added lemmas
authorimmler
Tue Apr 12 11:18:29 2016 +0200 (2016-04-12)
changeset 62951f59ef58f420b
parent 62950 c355b3223cbd
child 62961 8b85a554c5c4
added lemmas
src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Tue Apr 12 11:18:29 2016 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Tue Apr 12 11:18:29 2016 +0200
     1.3 @@ -484,6 +484,12 @@
     1.4    apply (simp add: blinfun.bilinear_simps)
     1.5    done
     1.6  
     1.7 +lemma Blinfun_eq_matrix: "bounded_linear f \<Longrightarrow> Blinfun f = blinfun_of_matrix (\<lambda>i j. f j \<bullet> i)"
     1.8 +  by (intro blinfun_euclidean_eqI)
     1.9 +     (auto simp: blinfun_of_matrix_apply bounded_linear_Blinfun_apply inner_Basis if_distrib
    1.10 +      cond_application_beta setsum.delta' euclidean_representation
    1.11 +      cong: if_cong)
    1.12 +
    1.13  text \<open>TODO: generalize (via @{thm compact_cball})?\<close>
    1.14  instance blinfun :: (euclidean_space, euclidean_space) heine_borel
    1.15  proof
    1.16 @@ -627,6 +633,11 @@
    1.17    by unfold_locales
    1.18      (auto intro!: blinfun_eqI exI[where x=1] simp: blinfun.bilinear_simps norm_blinfun_compose)
    1.19  
    1.20 +lemma blinfun_compose_zero[simp]:
    1.21 +  "blinfun_compose 0 = (\<lambda>_. 0)"
    1.22 +  "blinfun_compose x 0 = 0"
    1.23 +  by (auto simp: blinfun.bilinear_simps intro!: blinfun_eqI)
    1.24 +
    1.25  
    1.26  lift_definition blinfun_inner_right::"'a::real_inner \<Rightarrow> 'a \<Rightarrow>\<^sub>L real" is "op \<bullet>"
    1.27    by (rule bounded_linear_inner_right)