author immler Tue, 12 Apr 2016 11:18:29 +0200 changeset 62951 f59ef58f420b parent 62950 c355b3223cbd child 62961 8b85a554c5c4
--- 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 @@
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)