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)
```