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