src/HOL/Analysis/Linear_Algebra.thy
changeset 64773 223b2ebdda79
parent 64267 b9a1486e79be
child 65680 378a2f11bec9
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Tue Jan 03 23:21:09 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Wed Jan 04 16:18:50 2017 +0000
     1.3 @@ -1482,14 +1482,14 @@
     1.4  
     1.5  lemma sum_norm_le:
     1.6    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
     1.7 -  assumes fg: "\<forall>x \<in> S. norm (f x) \<le> g x"
     1.8 +  assumes fg: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> g x"
     1.9    shows "norm (sum f S) \<le> sum g S"
    1.10    by (rule order_trans [OF norm_sum sum_mono]) (simp add: fg)
    1.11  
    1.12  lemma sum_norm_bound:
    1.13    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
    1.14 -  assumes K: "\<forall>x \<in> S. norm (f x) \<le> K"
    1.15 -  shows "norm (sum f S) \<le> of_nat (card S) * K"
    1.16 +  assumes K: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> K"
    1.17 +  shows "norm (sum f S) \<le> of_nat (card S)*K"
    1.18    using sum_norm_le[OF K] sum_constant[symmetric]
    1.19    by simp
    1.20  
    1.21 @@ -1946,11 +1946,9 @@
    1.22      also have "\<dots> = norm (sum ?g Basis)"
    1.23        by (simp add: linear_sum [OF lf] linear_cmul [OF lf])
    1.24      finally have th0: "norm (f x) = norm (sum ?g Basis)" .
    1.25 -    have th: "\<forall>b\<in>Basis. norm (?g b) \<le> norm (f b) * norm x"
    1.26 -    proof
    1.27 -      fix i :: 'a
    1.28 -      assume i: "i \<in> Basis"
    1.29 -      from Basis_le_norm[OF i, of x]
    1.30 +    have th: "norm (?g i) \<le> norm (f i) * norm x" if "i \<in> Basis" for i
    1.31 +    proof -
    1.32 +      from Basis_le_norm[OF that, of x]
    1.33        show "norm (?g i) \<le> norm (f i) * norm x"
    1.34          unfolding norm_scaleR
    1.35          apply (subst mult.commute)
    1.36 @@ -2023,7 +2021,6 @@
    1.37    show "norm (h x y) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. norm (h i j)) * norm x * norm y"
    1.38      apply (auto simp add: sum_distrib_right th sum.cartesian_product)
    1.39      apply (rule sum_norm_le)
    1.40 -    apply simp
    1.41      apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh]
    1.42        field_simps simp del: scaleR_scaleR)
    1.43      apply (rule mult_mono)