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.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 +