src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy
changeset 61945 1135b8de26c3
parent 61916 7950ae6d3266
child 61969 e01015e49041
     1.1 --- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Mon Dec 28 01:26:34 2015 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Mon Dec 28 01:28:28 2015 +0100
     1.3 @@ -398,7 +398,7 @@
     1.4    by transfer (auto simp: algebra_simps setsum_subtractf)
     1.5  
     1.6  lemma norm_blinfun_of_matrix:
     1.7 -  "norm (blinfun_of_matrix a) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. abs (a i j))"
     1.8 +  "norm (blinfun_of_matrix a) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. \<bar>a i j\<bar>)"
     1.9    apply (rule norm_blinfun_bound)
    1.10     apply (simp add: setsum_nonneg)
    1.11    apply (simp only: blinfun_of_matrix_apply setsum_left_distrib)
    1.12 @@ -413,7 +413,7 @@
    1.13  proof -
    1.14    have "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> Zfun (\<lambda>x. norm (b x i j - a i j)) F"
    1.15      using assms unfolding tendsto_Zfun_iff Zfun_norm_iff .
    1.16 -  hence "Zfun (\<lambda>x. (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. abs (b x i j - a i j))) F"
    1.17 +  hence "Zfun (\<lambda>x. (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. \<bar>b x i j - a i j\<bar>)) F"
    1.18      by (auto intro!: Zfun_setsum)
    1.19    thus ?thesis
    1.20      unfolding tendsto_Zfun_iff blinfun_of_matrix_minus