src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy
 changeset 61973 0c7e865fa7cb parent 61969 e01015e49041 child 61975 b4b11391c676
```     1.1 --- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Tue Dec 29 23:50:44 2015 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Wed Dec 30 11:21:54 2015 +0100
1.3 @@ -355,8 +355,8 @@
1.4  lemma tendsto_componentwise1:
1.5    fixes a::"'a::euclidean_space \<Rightarrow>\<^sub>L 'b::real_normed_vector"
1.6      and b::"'c \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
1.7 -  assumes "(\<And>j. j \<in> Basis \<Longrightarrow> ((\<lambda>n. b n j) ---> a j) F)"
1.8 -  shows "(b ---> a) F"
1.9 +  assumes "(\<And>j. j \<in> Basis \<Longrightarrow> ((\<lambda>n. b n j) \<longlongrightarrow> a j) F)"
1.10 +  shows "(b \<longlongrightarrow> a) F"
1.11  proof -
1.12    have "\<And>j. j \<in> Basis \<Longrightarrow> Zfun (\<lambda>x. norm (b x j - a j)) F"
1.13      using assms unfolding tendsto_Zfun_iff Zfun_norm_iff .
1.14 @@ -408,8 +408,8 @@
1.15    done
1.16
1.17  lemma tendsto_blinfun_of_matrix:
1.18 -  assumes "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> ((\<lambda>n. b n i j) ---> a i j) F"
1.19 -  shows "((\<lambda>n. blinfun_of_matrix (b n)) ---> blinfun_of_matrix a) F"
1.20 +  assumes "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> ((\<lambda>n. b n i j) \<longlongrightarrow> a i j) F"
1.21 +  shows "((\<lambda>n. blinfun_of_matrix (b n)) \<longlongrightarrow> blinfun_of_matrix a) F"
1.22  proof -
1.23    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.24      using assms unfolding tendsto_Zfun_iff Zfun_norm_iff .
1.25 @@ -423,7 +423,7 @@
1.26  lemma tendsto_componentwise:
1.27    fixes a::"'a::euclidean_space \<Rightarrow>\<^sub>L 'b::euclidean_space"
1.28      and b::"'c \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
1.29 -  shows "(\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> ((\<lambda>n. b n j \<bullet> i) ---> a j \<bullet> i) F) \<Longrightarrow> (b ---> a) F"
1.30 +  shows "(\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> ((\<lambda>n. b n j \<bullet> i) \<longlongrightarrow> a j \<bullet> i) F) \<Longrightarrow> (b \<longlongrightarrow> a) F"
1.31    apply (subst blinfun_of_matrix_works[of a, symmetric])
1.32    apply (subst blinfun_of_matrix_works[of "b x" for x, symmetric, abs_def])
1.33    by (rule tendsto_blinfun_of_matrix)
1.34 @@ -495,7 +495,7 @@
1.35        by (metis (lifting) bounded_subset f' image_subsetI s')
1.36      then obtain l2 r2
1.37        where r2: "subseq r2"
1.38 -      and lr2: "((\<lambda>i. f (r1 (r2 i)) k) ---> l2) sequentially"
1.39 +      and lr2: "((\<lambda>i. f (r1 (r2 i)) k) \<longlongrightarrow> l2) sequentially"
1.40        using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) k"]
1.41        by (auto simp: o_def)
1.42      def r \<equiv> "r1 \<circ> r2"
1.43 @@ -585,9 +585,9 @@
1.44      ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
1.45        using eventually_elim2 by force
1.46    }
1.47 -  then have *: "((f \<circ> r) ---> l) sequentially"
1.48 +  then have *: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
1.49      unfolding o_def tendsto_iff by simp
1.50 -  with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
1.51 +  with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
1.52      by auto
1.53  qed
1.54
```