src/HOL/Analysis/Uniform_Limit.thy
changeset 65204 d23eded35a33
parent 65037 2cf841ff23be
child 66827 c94531b5007d
     1.1 --- a/src/HOL/Analysis/Uniform_Limit.thy	Sun Mar 12 19:06:10 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Uniform_Limit.thy	Fri Mar 10 23:16:40 2017 +0100
     1.3 @@ -203,6 +203,8 @@
     1.4  lemma uniformly_convergent_on_empty [iff]: "uniformly_convergent_on {} f"
     1.5    by (simp add: uniformly_convergent_on_def uniform_limit_sequentially_iff)
     1.6  
     1.7 +text\<open>Cauchy-type criteria for uniform convergence.\<close>
     1.8 +
     1.9  lemma Cauchy_uniformly_convergent:
    1.10    fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b :: complete_space"
    1.11    assumes "uniformly_Cauchy_on X f"
    1.12 @@ -235,6 +237,62 @@
    1.13    qed
    1.14  qed
    1.15  
    1.16 +lemma uniformly_convergent_Cauchy:
    1.17 +  assumes "uniformly_convergent_on X f"
    1.18 +  shows "uniformly_Cauchy_on X f"
    1.19 +proof (rule uniformly_Cauchy_onI)
    1.20 +  fix e::real assume "e > 0"
    1.21 +  then have "0 < e / 2" by simp
    1.22 +  with assms[unfolded uniformly_convergent_on_def uniform_limit_sequentially_iff]
    1.23 +  obtain l N where l:"x \<in> X \<Longrightarrow> n \<ge> N \<Longrightarrow> dist (f n x) (l x) < e / 2" for n x
    1.24 +    by metis
    1.25 +  from l l have "x \<in> X \<Longrightarrow> n \<ge> N \<Longrightarrow> m \<ge> N \<Longrightarrow> dist (f n x) (f m x) < e" for n m x
    1.26 +    by (rule dist_triangle_half_l)
    1.27 +  then show "\<exists>M. \<forall>x\<in>X. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e" by blast
    1.28 +qed
    1.29 +
    1.30 +lemma uniformly_convergent_eq_Cauchy:
    1.31 +  "uniformly_convergent_on X f = uniformly_Cauchy_on X f" for f::"nat \<Rightarrow> 'b \<Rightarrow> 'a::complete_space"
    1.32 +  using Cauchy_uniformly_convergent uniformly_convergent_Cauchy by blast
    1.33 +
    1.34 +lemma uniformly_convergent_eq_cauchy:
    1.35 +  fixes s::"nat \<Rightarrow> 'b \<Rightarrow> 'a::complete_space"
    1.36 +  shows
    1.37 +    "(\<exists>l. \<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e) \<longleftrightarrow>
    1.38 +      (\<forall>e>0. \<exists>N. \<forall>m n x. N \<le> m \<and> N \<le> n \<and> P x  \<longrightarrow> dist (s m x) (s n x) < e)"
    1.39 +proof -
    1.40 +  have *: "(\<forall>n\<ge>N. \<forall>x. Q x \<longrightarrow> R n x) \<longleftrightarrow> (\<forall>n x. N \<le> n \<and> Q x \<longrightarrow> R n x)"
    1.41 +    "(\<forall>x. Q x \<longrightarrow> (\<forall>m\<ge>N. \<forall>n\<ge>N. S n m x)) \<longleftrightarrow> (\<forall>m n x. N \<le> m \<and> N \<le> n \<and> Q x \<longrightarrow> S n m x)"
    1.42 +    for N::nat and Q::"'b \<Rightarrow> bool" and R S
    1.43 +    by blast+
    1.44 +  show ?thesis
    1.45 +    using uniformly_convergent_eq_Cauchy[of "Collect P" s]
    1.46 +    unfolding uniformly_convergent_on_def uniformly_Cauchy_on_def uniform_limit_sequentially_iff
    1.47 +    by (simp add: *)
    1.48 +qed
    1.49 +
    1.50 +lemma uniformly_cauchy_imp_uniformly_convergent:
    1.51 +  fixes s :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::complete_space"
    1.52 +  assumes "\<forall>e>0.\<exists>N. \<forall>m (n::nat) x. N \<le> m \<and> N \<le> n \<and> P x --> dist(s m x)(s n x) < e"
    1.53 +    and "\<forall>x. P x --> (\<forall>e>0. \<exists>N. \<forall>n. N \<le> n \<longrightarrow> dist(s n x)(l x) < e)"
    1.54 +  shows "\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e"
    1.55 +proof -
    1.56 +  obtain l' where l:"\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist (s n x) (l' x) < e"
    1.57 +    using assms(1) unfolding uniformly_convergent_eq_cauchy[symmetric] by auto
    1.58 +  moreover
    1.59 +  {
    1.60 +    fix x
    1.61 +    assume "P x"
    1.62 +    then have "l x = l' x"
    1.63 +      using tendsto_unique[OF trivial_limit_sequentially, of "\<lambda>n. s n x" "l x" "l' x"]
    1.64 +      using l and assms(2) unfolding lim_sequentially by blast
    1.65 +  }
    1.66 +  ultimately show ?thesis by auto
    1.67 +qed
    1.68 +
    1.69 +text \<open>TODO: remove explicit formulations
    1.70 +  @{thm uniformly_convergent_eq_cauchy uniformly_cauchy_imp_uniformly_convergent}?!\<close>
    1.71 +
    1.72  lemma uniformly_convergent_imp_convergent:
    1.73    "uniformly_convergent_on X f \<Longrightarrow> x \<in> X \<Longrightarrow> convergent (\<lambda>n. f n x)"
    1.74    unfolding uniformly_convergent_on_def convergent_def
    1.75 @@ -363,7 +421,7 @@
    1.76  lemmas uniform_limit_uminus[uniform_limit_intros] =
    1.77    bounded_linear.uniform_limit[OF bounded_linear_minus[OF bounded_linear_ident]]
    1.78  
    1.79 -lemma uniform_limit_const[uniform_limit_intros]: "uniform_limit S (\<lambda>x y. c) (\<lambda>x. c) f"
    1.80 +lemma uniform_limit_const[uniform_limit_intros]: "uniform_limit S (\<lambda>x. c) c f"
    1.81    by (auto intro!: uniform_limitI)
    1.82  
    1.83  lemma uniform_limit_add[uniform_limit_intros]:
    1.84 @@ -574,6 +632,24 @@
    1.85    "uniform_limit J f g F \<Longrightarrow> I \<subseteq> J \<Longrightarrow> uniform_limit I f g F"
    1.86    by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_mono)
    1.87  
    1.88 +lemma uniform_limit_bounded:
    1.89 +  fixes f::"'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::metric_space"
    1.90 +  assumes l: "uniform_limit S f l F"
    1.91 +  assumes bnd: "\<forall>\<^sub>F i in F. bounded (f i ` S)"
    1.92 +  assumes "F \<noteq> bot"
    1.93 +  shows "bounded (l ` S)"
    1.94 +proof -
    1.95 +  from l have "\<forall>\<^sub>F n in F. \<forall>x\<in>S. dist (l x) (f n x) < 1"
    1.96 +    by (auto simp: uniform_limit_iff dist_commute dest!: spec[where x=1])
    1.97 +  with bnd
    1.98 +  have "\<forall>\<^sub>F n in F. \<exists>M. \<forall>x\<in>S. dist undefined (l x) \<le> M + 1"
    1.99 +    by eventually_elim
   1.100 +      (auto intro!: order_trans[OF dist_triangle2 add_mono] intro: less_imp_le
   1.101 +        simp: bounded_any_center[where a=undefined])
   1.102 +  then show ?thesis using assms
   1.103 +    by (auto simp: bounded_any_center[where a=undefined] dest!: eventually_happens)
   1.104 +qed
   1.105 +
   1.106  lemma uniformly_convergent_add:
   1.107    "uniformly_convergent_on A f \<Longrightarrow> uniformly_convergent_on A g\<Longrightarrow>
   1.108        uniformly_convergent_on A (\<lambda>k x. f k x + g k x :: 'a :: {real_normed_algebra})"