--- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy Tue Apr 12 11:18:29 2016 +0200
@@ -484,6 +484,12 @@
apply (simp add: blinfun.bilinear_simps)
done
+lemma Blinfun_eq_matrix: "bounded_linear f \<Longrightarrow> Blinfun f = blinfun_of_matrix (\<lambda>i j. f j \<bullet> i)"
+ by (intro blinfun_euclidean_eqI)
+ (auto simp: blinfun_of_matrix_apply bounded_linear_Blinfun_apply inner_Basis if_distrib
+ cond_application_beta setsum.delta' euclidean_representation
+ cong: if_cong)
+
text \<open>TODO: generalize (via @{thm compact_cball})?\<close>
instance blinfun :: (euclidean_space, euclidean_space) heine_borel
proof
@@ -627,6 +633,11 @@
by unfold_locales
(auto intro!: blinfun_eqI exI[where x=1] simp: blinfun.bilinear_simps norm_blinfun_compose)
+lemma blinfun_compose_zero[simp]:
+ "blinfun_compose 0 = (\<lambda>_. 0)"
+ "blinfun_compose x 0 = 0"
+ by (auto simp: blinfun.bilinear_simps intro!: blinfun_eqI)
+
lift_definition blinfun_inner_right::"'a::real_inner \<Rightarrow> 'a \<Rightarrow>\<^sub>L real" is "op \<bullet>"
by (rule bounded_linear_inner_right)