src/HOL/Analysis/Uniform_Limit.thy
changeset 63627 6ddb43c6b711
parent 63594 bd218a9320b5
child 64267 b9a1486e79be
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Analysis/Uniform_Limit.thy	Mon Aug 08 14:13:14 2016 +0200
     1.3 @@ -0,0 +1,570 @@
     1.4 +(*  Title:      HOL/Analysis/Uniform_Limit.thy
     1.5 +    Author:     Christoph Traut, TU München
     1.6 +    Author:     Fabian Immler, TU München
     1.7 +*)
     1.8 +
     1.9 +section \<open>Uniform Limit and Uniform Convergence\<close>
    1.10 +
    1.11 +theory Uniform_Limit
    1.12 +imports Topology_Euclidean_Space Summation_Tests
    1.13 +begin
    1.14 +
    1.15 +definition uniformly_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> ('a \<Rightarrow> 'b) filter"
    1.16 +  where "uniformly_on S l = (INF e:{0 <..}. principal {f. \<forall>x\<in>S. dist (f x) (l x) < e})"
    1.17 +
    1.18 +abbreviation
    1.19 +  "uniform_limit S f l \<equiv> filterlim f (uniformly_on S l)"
    1.20 +
    1.21 +definition uniformly_convergent_on where
    1.22 +  "uniformly_convergent_on X f \<longleftrightarrow> (\<exists>l. uniform_limit X f l sequentially)"
    1.23 +
    1.24 +definition uniformly_Cauchy_on where
    1.25 +  "uniformly_Cauchy_on X f \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>x\<in>X. \<forall>(m::nat)\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e)"
    1.26 +
    1.27 +lemma uniform_limit_iff:
    1.28 +  "uniform_limit S f l F \<longleftrightarrow> (\<forall>e>0. \<forall>\<^sub>F n in F. \<forall>x\<in>S. dist (f n x) (l x) < e)"
    1.29 +  unfolding filterlim_iff uniformly_on_def
    1.30 +  by (subst eventually_INF_base)
    1.31 +    (fastforce
    1.32 +      simp: eventually_principal uniformly_on_def
    1.33 +      intro: bexI[where x="min a b" for a b]
    1.34 +      elim: eventually_mono)+
    1.35 +
    1.36 +lemma uniform_limitD:
    1.37 +  "uniform_limit S f l F \<Longrightarrow> e > 0 \<Longrightarrow> \<forall>\<^sub>F n in F. \<forall>x\<in>S. dist (f n x) (l x) < e"
    1.38 +  by (simp add: uniform_limit_iff)
    1.39 +
    1.40 +lemma uniform_limitI:
    1.41 +  "(\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F n in F. \<forall>x\<in>S. dist (f n x) (l x) < e) \<Longrightarrow> uniform_limit S f l F"
    1.42 +  by (simp add: uniform_limit_iff)
    1.43 +
    1.44 +lemma uniform_limit_sequentially_iff:
    1.45 +  "uniform_limit S f l sequentially \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> S. dist (f n x) (l x) < e)"
    1.46 +  unfolding uniform_limit_iff eventually_sequentially ..
    1.47 +
    1.48 +lemma uniform_limit_at_iff:
    1.49 +  "uniform_limit S f l (at x) \<longleftrightarrow>
    1.50 +    (\<forall>e>0. \<exists>d>0. \<forall>z. 0 < dist z x \<and> dist z x < d \<longrightarrow> (\<forall>x\<in>S. dist (f z x) (l x) < e))"
    1.51 +  unfolding uniform_limit_iff eventually_at by simp
    1.52 +
    1.53 +lemma uniform_limit_at_le_iff:
    1.54 +  "uniform_limit S f l (at x) \<longleftrightarrow>
    1.55 +    (\<forall>e>0. \<exists>d>0. \<forall>z. 0 < dist z x \<and> dist z x < d \<longrightarrow> (\<forall>x\<in>S. dist (f z x) (l x) \<le> e))"
    1.56 +  unfolding uniform_limit_iff eventually_at
    1.57 +  by (fastforce dest: spec[where x = "e / 2" for e])
    1.58 +
    1.59 +lemma metric_uniform_limit_imp_uniform_limit:
    1.60 +  assumes f: "uniform_limit S f a F"
    1.61 +  assumes le: "eventually (\<lambda>x. \<forall>y\<in>S. dist (g x y) (b y) \<le> dist (f x y) (a y)) F"
    1.62 +  shows "uniform_limit S g b F"
    1.63 +proof (rule uniform_limitI)
    1.64 +  fix e :: real assume "0 < e"
    1.65 +  from uniform_limitD[OF f this] le
    1.66 +  show "\<forall>\<^sub>F x in F. \<forall>y\<in>S. dist (g x y) (b y) < e"
    1.67 +    by eventually_elim force
    1.68 +qed
    1.69 +
    1.70 +lemma swap_uniform_limit:
    1.71 +  assumes f: "\<forall>\<^sub>F n in F. (f n \<longlongrightarrow> g n) (at x within S)"
    1.72 +  assumes g: "(g \<longlongrightarrow> l) F"
    1.73 +  assumes uc: "uniform_limit S f h F"
    1.74 +  assumes "\<not>trivial_limit F"
    1.75 +  shows "(h \<longlongrightarrow> l) (at x within S)"
    1.76 +proof (rule tendstoI)
    1.77 +  fix e :: real
    1.78 +  define e' where "e' = e/3"
    1.79 +  assume "0 < e"
    1.80 +  then have "0 < e'" by (simp add: e'_def)
    1.81 +  from uniform_limitD[OF uc \<open>0 < e'\<close>]
    1.82 +  have "\<forall>\<^sub>F n in F. \<forall>x\<in>S. dist (h x) (f n x) < e'"
    1.83 +    by (simp add: dist_commute)
    1.84 +  moreover
    1.85 +  from f
    1.86 +  have "\<forall>\<^sub>F n in F. \<forall>\<^sub>F x in at x within S. dist (g n) (f n x) < e'"
    1.87 +    by eventually_elim (auto dest!: tendstoD[OF _ \<open>0 < e'\<close>] simp: dist_commute)
    1.88 +  moreover
    1.89 +  from tendstoD[OF g \<open>0 < e'\<close>] have "\<forall>\<^sub>F x in F. dist l (g x) < e'"
    1.90 +    by (simp add: dist_commute)
    1.91 +  ultimately
    1.92 +  have "\<forall>\<^sub>F _ in F. \<forall>\<^sub>F x in at x within S. dist (h x) l < e"
    1.93 +  proof eventually_elim
    1.94 +    case (elim n)
    1.95 +    note fh = elim(1)
    1.96 +    note gl = elim(3)
    1.97 +    have "\<forall>\<^sub>F x in at x within S. x \<in> S"
    1.98 +      by (auto simp: eventually_at_filter)
    1.99 +    with elim(2)
   1.100 +    show ?case
   1.101 +    proof eventually_elim
   1.102 +      case (elim x)
   1.103 +      from fh[rule_format, OF \<open>x \<in> S\<close>] elim(1)
   1.104 +      have "dist (h x) (g n) < e' + e'"
   1.105 +        by (rule dist_triangle_lt[OF add_strict_mono])
   1.106 +      from dist_triangle_lt[OF add_strict_mono, OF this gl]
   1.107 +      show ?case by (simp add: e'_def)
   1.108 +    qed
   1.109 +  qed
   1.110 +  thus "\<forall>\<^sub>F x in at x within S. dist (h x) l < e"
   1.111 +    using eventually_happens by (metis \<open>\<not>trivial_limit F\<close>)
   1.112 +qed
   1.113 +
   1.114 +lemma
   1.115 +  tendsto_uniform_limitI:
   1.116 +  assumes "uniform_limit S f l F"
   1.117 +  assumes "x \<in> S"
   1.118 +  shows "((\<lambda>y. f y x) \<longlongrightarrow> l x) F"
   1.119 +  using assms
   1.120 +  by (auto intro!: tendstoI simp: eventually_mono dest!: uniform_limitD)
   1.121 +
   1.122 +lemma uniform_limit_theorem:
   1.123 +  assumes c: "\<forall>\<^sub>F n in F. continuous_on A (f n)"
   1.124 +  assumes ul: "uniform_limit A f l F"
   1.125 +  assumes "\<not> trivial_limit F"
   1.126 +  shows "continuous_on A l"
   1.127 +  unfolding continuous_on_def
   1.128 +proof safe
   1.129 +  fix x assume "x \<in> A"
   1.130 +  then have "\<forall>\<^sub>F n in F. (f n \<longlongrightarrow> f n x) (at x within A)" "((\<lambda>n. f n x) \<longlongrightarrow> l x) F"
   1.131 +    using c ul
   1.132 +    by (auto simp: continuous_on_def eventually_mono tendsto_uniform_limitI)
   1.133 +  then show "(l \<longlongrightarrow> l x) (at x within A)"
   1.134 +    by (rule swap_uniform_limit) fact+
   1.135 +qed
   1.136 +
   1.137 +lemma uniformly_Cauchy_onI:
   1.138 +  assumes "\<And>e. e > 0 \<Longrightarrow> \<exists>M. \<forall>x\<in>X. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e"
   1.139 +  shows   "uniformly_Cauchy_on X f"
   1.140 +  using assms unfolding uniformly_Cauchy_on_def by blast
   1.141 +
   1.142 +lemma uniformly_Cauchy_onI':
   1.143 +  assumes "\<And>e. e > 0 \<Longrightarrow> \<exists>M. \<forall>x\<in>X. \<forall>m\<ge>M. \<forall>n>m. dist (f m x) (f n x) < e"
   1.144 +  shows   "uniformly_Cauchy_on X f"
   1.145 +proof (rule uniformly_Cauchy_onI)
   1.146 +  fix e :: real assume e: "e > 0"
   1.147 +  from assms[OF this] obtain M
   1.148 +    where M: "\<And>x m n. x \<in> X \<Longrightarrow> m \<ge> M \<Longrightarrow> n > m \<Longrightarrow> dist (f m x) (f n x) < e" by fast
   1.149 +  {
   1.150 +    fix x m n assume x: "x \<in> X" and m: "m \<ge> M" and n: "n \<ge> M"
   1.151 +    with M[OF this(1,2), of n] M[OF this(1,3), of m] e have "dist (f m x) (f n x) < e"
   1.152 +      by (cases m n rule: linorder_cases) (simp_all add: dist_commute)
   1.153 +  }
   1.154 +  thus "\<exists>M. \<forall>x\<in>X. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e" by fast
   1.155 +qed
   1.156 +
   1.157 +lemma uniformly_Cauchy_imp_Cauchy:
   1.158 +  "uniformly_Cauchy_on X f \<Longrightarrow> x \<in> X \<Longrightarrow> Cauchy (\<lambda>n. f n x)"
   1.159 +  unfolding Cauchy_def uniformly_Cauchy_on_def by fast
   1.160 +
   1.161 +lemma uniform_limit_cong:
   1.162 +  fixes f g :: "'a \<Rightarrow> 'b \<Rightarrow> ('c :: metric_space)" and h i :: "'b \<Rightarrow> 'c"
   1.163 +  assumes "eventually (\<lambda>y. \<forall>x\<in>X. f y x = g y x) F"
   1.164 +  assumes "\<And>x. x \<in> X \<Longrightarrow> h x = i x"
   1.165 +  shows   "uniform_limit X f h F \<longleftrightarrow> uniform_limit X g i F"
   1.166 +proof -
   1.167 +  {
   1.168 +    fix f g :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" and h i :: "'b \<Rightarrow> 'c"
   1.169 +    assume C: "uniform_limit X f h F" and A: "eventually (\<lambda>y. \<forall>x\<in>X. f y x = g y x) F"
   1.170 +       and B: "\<And>x. x \<in> X \<Longrightarrow> h x = i x"
   1.171 +    {
   1.172 +      fix e ::real assume "e > 0"
   1.173 +      with C have "eventually (\<lambda>y. \<forall>x\<in>X. dist (f y x) (h x) < e) F"
   1.174 +        unfolding uniform_limit_iff by blast
   1.175 +      with A have "eventually (\<lambda>y. \<forall>x\<in>X. dist (g y x) (i x) < e) F"
   1.176 +        by eventually_elim (insert B, simp_all)
   1.177 +    }
   1.178 +    hence "uniform_limit X g i F" unfolding uniform_limit_iff by blast
   1.179 +  } note A = this
   1.180 +  show ?thesis by (rule iffI) (erule A; insert assms; simp add: eq_commute)+
   1.181 +qed
   1.182 +
   1.183 +lemma uniform_limit_cong':
   1.184 +  fixes f g :: "'a \<Rightarrow> 'b \<Rightarrow> ('c :: metric_space)" and h i :: "'b \<Rightarrow> 'c"
   1.185 +  assumes "\<And>y x. x \<in> X \<Longrightarrow> f y x = g y x"
   1.186 +  assumes "\<And>x. x \<in> X \<Longrightarrow> h x = i x"
   1.187 +  shows   "uniform_limit X f h F \<longleftrightarrow> uniform_limit X g i F"
   1.188 +  using assms by (intro uniform_limit_cong always_eventually) blast+
   1.189 +
   1.190 +lemma uniformly_convergent_uniform_limit_iff:
   1.191 +  "uniformly_convergent_on X f \<longleftrightarrow> uniform_limit X f (\<lambda>x. lim (\<lambda>n. f n x)) sequentially"
   1.192 +proof
   1.193 +  assume "uniformly_convergent_on X f"
   1.194 +  then obtain l where l: "uniform_limit X f l sequentially"
   1.195 +    unfolding uniformly_convergent_on_def by blast
   1.196 +  from l have "uniform_limit X f (\<lambda>x. lim (\<lambda>n. f n x)) sequentially \<longleftrightarrow>
   1.197 +                      uniform_limit X f l sequentially"
   1.198 +    by (intro uniform_limit_cong' limI tendsto_uniform_limitI[of f X l]) simp_all
   1.199 +  also note l
   1.200 +  finally show "uniform_limit X f (\<lambda>x. lim (\<lambda>n. f n x)) sequentially" .
   1.201 +qed (auto simp: uniformly_convergent_on_def)
   1.202 +
   1.203 +lemma uniformly_convergentI: "uniform_limit X f l sequentially \<Longrightarrow> uniformly_convergent_on X f"
   1.204 +  unfolding uniformly_convergent_on_def by blast
   1.205 +
   1.206 +lemma uniformly_convergent_on_empty [iff]: "uniformly_convergent_on {} f"
   1.207 +  by (simp add: uniformly_convergent_on_def uniform_limit_sequentially_iff)
   1.208 +
   1.209 +lemma Cauchy_uniformly_convergent:
   1.210 +  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b :: complete_space"
   1.211 +  assumes "uniformly_Cauchy_on X f"
   1.212 +  shows   "uniformly_convergent_on X f"
   1.213 +unfolding uniformly_convergent_uniform_limit_iff uniform_limit_iff
   1.214 +proof safe
   1.215 +  let ?f = "\<lambda>x. lim (\<lambda>n. f n x)"
   1.216 +  fix e :: real assume e: "e > 0"
   1.217 +  hence "e/2 > 0" by simp
   1.218 +  with assms obtain N where N: "\<And>x m n. x \<in> X \<Longrightarrow> m \<ge> N \<Longrightarrow> n \<ge> N \<Longrightarrow> dist (f m x) (f n x) < e/2"
   1.219 +    unfolding uniformly_Cauchy_on_def by fast
   1.220 +  show "eventually (\<lambda>n. \<forall>x\<in>X. dist (f n x) (?f x) < e) sequentially"
   1.221 +    using eventually_ge_at_top[of N]
   1.222 +  proof eventually_elim
   1.223 +    fix n assume n: "n \<ge> N"
   1.224 +    show "\<forall>x\<in>X. dist (f n x) (?f x) < e"
   1.225 +    proof
   1.226 +      fix x assume x: "x \<in> X"
   1.227 +      with assms have "(\<lambda>n. f n x) \<longlonglongrightarrow> ?f x"
   1.228 +        by (auto dest!: Cauchy_convergent uniformly_Cauchy_imp_Cauchy simp: convergent_LIMSEQ_iff)
   1.229 +      with \<open>e/2 > 0\<close> have "eventually (\<lambda>m. m \<ge> N \<and> dist (f m x) (?f x) < e/2) sequentially"
   1.230 +        by (intro tendstoD eventually_conj eventually_ge_at_top)
   1.231 +      then obtain m where m: "m \<ge> N" "dist (f m x) (?f x) < e/2"
   1.232 +        unfolding eventually_at_top_linorder by blast
   1.233 +      have "dist (f n x) (?f x) \<le> dist (f n x) (f m x) + dist (f m x) (?f x)"
   1.234 +          by (rule dist_triangle)
   1.235 +      also from x n have "... < e/2 + e/2" by (intro add_strict_mono N m)
   1.236 +      finally show "dist (f n x) (?f x) < e" by simp
   1.237 +    qed
   1.238 +  qed
   1.239 +qed
   1.240 +
   1.241 +lemma uniformly_convergent_imp_convergent:
   1.242 +  "uniformly_convergent_on X f \<Longrightarrow> x \<in> X \<Longrightarrow> convergent (\<lambda>n. f n x)"
   1.243 +  unfolding uniformly_convergent_on_def convergent_def
   1.244 +  by (auto dest: tendsto_uniform_limitI)
   1.245 +
   1.246 +lemma weierstrass_m_test_ev:
   1.247 +fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
   1.248 +assumes "eventually (\<lambda>n. \<forall>x\<in>A. norm (f n x) \<le> M n) sequentially"
   1.249 +assumes "summable M"
   1.250 +shows "uniform_limit A (\<lambda>n x. \<Sum>i<n. f i x) (\<lambda>x. suminf (\<lambda>i. f i x)) sequentially"
   1.251 +proof (rule uniform_limitI)
   1.252 +  fix e :: real
   1.253 +  assume "0 < e"
   1.254 +  from suminf_exist_split[OF \<open>0 < e\<close> \<open>summable M\<close>]
   1.255 +  have "\<forall>\<^sub>F k in sequentially. norm (\<Sum>i. M (i + k)) < e"
   1.256 +    by (auto simp: eventually_sequentially)
   1.257 +  with eventually_all_ge_at_top[OF assms(1)]
   1.258 +    show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>A. dist (\<Sum>i<n. f i x) (\<Sum>i. f i x) < e"
   1.259 +  proof eventually_elim
   1.260 +    case (elim k)
   1.261 +    show ?case
   1.262 +    proof safe
   1.263 +      fix x assume "x \<in> A"
   1.264 +      have "\<exists>N. \<forall>n\<ge>N. norm (f n x) \<le> M n"
   1.265 +        using assms(1) \<open>x \<in> A\<close> by (force simp: eventually_at_top_linorder)
   1.266 +      hence summable_norm_f: "summable (\<lambda>n. norm (f n x))"
   1.267 +        by(rule summable_norm_comparison_test[OF _ \<open>summable M\<close>])
   1.268 +      have summable_f: "summable (\<lambda>n. f n x)"
   1.269 +        using summable_norm_cancel[OF summable_norm_f] .
   1.270 +      have summable_norm_f_plus_k: "summable (\<lambda>i. norm (f (i + k) x))"
   1.271 +        using summable_ignore_initial_segment[OF summable_norm_f]
   1.272 +        by auto
   1.273 +      have summable_M_plus_k: "summable (\<lambda>i. M (i + k))"
   1.274 +        using summable_ignore_initial_segment[OF \<open>summable M\<close>]
   1.275 +        by auto
   1.276 +
   1.277 +      have "dist (\<Sum>i<k. f i x) (\<Sum>i. f i x) = norm ((\<Sum>i. f i x) - (\<Sum>i<k. f i x))"
   1.278 +        using dist_norm dist_commute by (subst dist_commute)
   1.279 +      also have "... = norm (\<Sum>i. f (i + k) x)"
   1.280 +        using suminf_minus_initial_segment[OF summable_f, where k=k] by simp
   1.281 +      also have "... \<le> (\<Sum>i. norm (f (i + k) x))"
   1.282 +        using summable_norm[OF summable_norm_f_plus_k] .
   1.283 +      also have "... \<le> (\<Sum>i. M (i + k))"
   1.284 +        by (rule suminf_le[OF _ summable_norm_f_plus_k summable_M_plus_k])
   1.285 +           (insert elim(1) \<open>x \<in> A\<close>, simp)
   1.286 +      finally show "dist (\<Sum>i<k. f i x) (\<Sum>i. f i x) < e"
   1.287 +        using elim by auto
   1.288 +    qed
   1.289 +  qed
   1.290 +qed
   1.291 +
   1.292 +text\<open>Alternative version, formulated as in HOL Light\<close>
   1.293 +corollary series_comparison_uniform:
   1.294 +  fixes f :: "_ \<Rightarrow> nat \<Rightarrow> _ :: banach"
   1.295 +  assumes g: "summable g" and le: "\<And>n x. N \<le> n \<and> x \<in> A \<Longrightarrow> norm(f x n) \<le> g n"
   1.296 +    shows "\<exists>l. \<forall>e. 0 < e \<longrightarrow> (\<exists>N. \<forall>n x. N \<le> n \<and> x \<in> A \<longrightarrow> dist(setsum (f x) {..<n}) (l x) < e)"
   1.297 +proof -
   1.298 +  have 1: "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>A. norm (f x n) \<le> g n"
   1.299 +    using le eventually_sequentially by auto
   1.300 +  show ?thesis
   1.301 +    apply (rule_tac x="(\<lambda>x. \<Sum>i. f x i)" in exI)
   1.302 +    apply (metis (no_types, lifting) eventually_sequentially uniform_limitD [OF weierstrass_m_test_ev [OF 1 g]])
   1.303 +    done
   1.304 +qed
   1.305 +
   1.306 +corollary weierstrass_m_test:
   1.307 +  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
   1.308 +  assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> M n"
   1.309 +  assumes "summable M"
   1.310 +  shows "uniform_limit A (\<lambda>n x. \<Sum>i<n. f i x) (\<lambda>x. suminf (\<lambda>i. f i x)) sequentially"
   1.311 +  using assms by (intro weierstrass_m_test_ev always_eventually) auto
   1.312 +
   1.313 +corollary weierstrass_m_test'_ev:
   1.314 +  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
   1.315 +  assumes "eventually (\<lambda>n. \<forall>x\<in>A. norm (f n x) \<le> M n) sequentially" "summable M"
   1.316 +  shows   "uniformly_convergent_on A (\<lambda>n x. \<Sum>i<n. f i x)"
   1.317 +  unfolding uniformly_convergent_on_def by (rule exI, rule weierstrass_m_test_ev[OF assms])
   1.318 +
   1.319 +corollary weierstrass_m_test':
   1.320 +  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
   1.321 +  assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> M n" "summable M"
   1.322 +  shows   "uniformly_convergent_on A (\<lambda>n x. \<Sum>i<n. f i x)"
   1.323 +  unfolding uniformly_convergent_on_def by (rule exI, rule weierstrass_m_test[OF assms])
   1.324 +
   1.325 +lemma uniform_limit_eq_rhs: "uniform_limit X f l F \<Longrightarrow> l = m \<Longrightarrow> uniform_limit X f m F"
   1.326 +  by simp
   1.327 +
   1.328 +named_theorems uniform_limit_intros "introduction rules for uniform_limit"
   1.329 +setup \<open>
   1.330 +  Global_Theory.add_thms_dynamic (@{binding uniform_limit_eq_intros},
   1.331 +    fn context =>
   1.332 +      Named_Theorems.get (Context.proof_of context) @{named_theorems uniform_limit_intros}
   1.333 +      |> map_filter (try (fn thm => @{thm uniform_limit_eq_rhs} OF [thm])))
   1.334 +\<close>
   1.335 +
   1.336 +lemma (in bounded_linear) uniform_limit[uniform_limit_intros]:
   1.337 +  assumes "uniform_limit X g l F"
   1.338 +  shows "uniform_limit X (\<lambda>a b. f (g a b)) (\<lambda>a. f (l a)) F"
   1.339 +proof (rule uniform_limitI)
   1.340 +  fix e::real
   1.341 +  from pos_bounded obtain K
   1.342 +    where K: "\<And>x y. dist (f x) (f y) \<le> K * dist x y" "K > 0"
   1.343 +    by (auto simp: ac_simps dist_norm diff[symmetric])
   1.344 +  assume "0 < e" with \<open>K > 0\<close> have "e / K > 0" by simp
   1.345 +  from uniform_limitD[OF assms this]
   1.346 +  show "\<forall>\<^sub>F n in F. \<forall>x\<in>X. dist (f (g n x)) (f (l x)) < e"
   1.347 +    by eventually_elim (metis le_less_trans mult.commute pos_less_divide_eq K)
   1.348 +qed
   1.349 +
   1.350 +lemmas bounded_linear_uniform_limit_intros[uniform_limit_intros] =
   1.351 +  bounded_linear.uniform_limit[OF bounded_linear_Im]
   1.352 +  bounded_linear.uniform_limit[OF bounded_linear_Re]
   1.353 +  bounded_linear.uniform_limit[OF bounded_linear_cnj]
   1.354 +  bounded_linear.uniform_limit[OF bounded_linear_fst]
   1.355 +  bounded_linear.uniform_limit[OF bounded_linear_snd]
   1.356 +  bounded_linear.uniform_limit[OF bounded_linear_zero]
   1.357 +  bounded_linear.uniform_limit[OF bounded_linear_of_real]
   1.358 +  bounded_linear.uniform_limit[OF bounded_linear_inner_left]
   1.359 +  bounded_linear.uniform_limit[OF bounded_linear_inner_right]
   1.360 +  bounded_linear.uniform_limit[OF bounded_linear_divide]
   1.361 +  bounded_linear.uniform_limit[OF bounded_linear_scaleR_right]
   1.362 +  bounded_linear.uniform_limit[OF bounded_linear_mult_left]
   1.363 +  bounded_linear.uniform_limit[OF bounded_linear_mult_right]
   1.364 +  bounded_linear.uniform_limit[OF bounded_linear_scaleR_left]
   1.365 +
   1.366 +lemmas uniform_limit_uminus[uniform_limit_intros] =
   1.367 +  bounded_linear.uniform_limit[OF bounded_linear_minus[OF bounded_linear_ident]]
   1.368 +
   1.369 +lemma uniform_limit_const[uniform_limit_intros]: "uniform_limit S (\<lambda>x y. c) (\<lambda>x. c) f"
   1.370 +  by (auto intro!: uniform_limitI)
   1.371 +
   1.372 +lemma uniform_limit_add[uniform_limit_intros]:
   1.373 +  fixes f g::"'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_vector"
   1.374 +  assumes "uniform_limit X f l F"
   1.375 +  assumes "uniform_limit X g m F"
   1.376 +  shows "uniform_limit X (\<lambda>a b. f a b + g a b) (\<lambda>a. l a + m a) F"
   1.377 +proof (rule uniform_limitI)
   1.378 +  fix e::real
   1.379 +  assume "0 < e"
   1.380 +  hence "0 < e / 2" by simp
   1.381 +  from
   1.382 +    uniform_limitD[OF assms(1) this]
   1.383 +    uniform_limitD[OF assms(2) this]
   1.384 +  show "\<forall>\<^sub>F n in F. \<forall>x\<in>X. dist (f n x + g n x) (l x + m x) < e"
   1.385 +    by eventually_elim (simp add: dist_triangle_add_half)
   1.386 +qed
   1.387 +
   1.388 +lemma uniform_limit_minus[uniform_limit_intros]:
   1.389 +  fixes f g::"'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_vector"
   1.390 +  assumes "uniform_limit X f l F"
   1.391 +  assumes "uniform_limit X g m F"
   1.392 +  shows "uniform_limit X (\<lambda>a b. f a b - g a b) (\<lambda>a. l a - m a) F"
   1.393 +  unfolding diff_conv_add_uminus
   1.394 +  by (rule uniform_limit_intros assms)+
   1.395 +
   1.396 +lemma uniform_limit_norm[uniform_limit_intros]:
   1.397 +  assumes "uniform_limit S g l f"
   1.398 +  shows "uniform_limit S (\<lambda>x y. norm (g x y)) (\<lambda>x. norm (l x)) f"
   1.399 +  using assms
   1.400 +  apply (rule metric_uniform_limit_imp_uniform_limit)
   1.401 +  apply (rule eventuallyI)
   1.402 +  by (metis dist_norm norm_triangle_ineq3 real_norm_def)
   1.403 +
   1.404 +lemma (in bounded_bilinear) bounded_uniform_limit[uniform_limit_intros]:
   1.405 +  assumes "uniform_limit X f l F"
   1.406 +  assumes "uniform_limit X g m F"
   1.407 +  assumes "bounded (m ` X)"
   1.408 +  assumes "bounded (l ` X)"
   1.409 +  shows "uniform_limit X (\<lambda>a b. prod (f a b) (g a b)) (\<lambda>a. prod (l a) (m a)) F"
   1.410 +proof (rule uniform_limitI)
   1.411 +  fix e::real
   1.412 +  from pos_bounded obtain K where K:
   1.413 +    "0 < K" "\<And>a b. norm (prod a b) \<le> norm a * norm b * K"
   1.414 +    by auto
   1.415 +  hence "sqrt (K*4) > 0" by simp
   1.416 +
   1.417 +  from assms obtain Km Kl
   1.418 +  where Km: "Km > 0" "\<And>x. x \<in> X \<Longrightarrow> norm (m x) \<le> Km"
   1.419 +    and Kl: "Kl > 0" "\<And>x. x \<in> X \<Longrightarrow> norm (l x) \<le> Kl"
   1.420 +    by (auto simp: bounded_pos)
   1.421 +  hence "K * Km * 4 > 0" "K * Kl * 4 > 0"
   1.422 +    using \<open>K > 0\<close>
   1.423 +    by simp_all
   1.424 +  assume "0 < e"
   1.425 +
   1.426 +  hence "sqrt e > 0" by simp
   1.427 +  from uniform_limitD[OF assms(1) divide_pos_pos[OF this \<open>sqrt (K*4) > 0\<close>]]
   1.428 +    uniform_limitD[OF assms(2) divide_pos_pos[OF this \<open>sqrt (K*4) > 0\<close>]]
   1.429 +    uniform_limitD[OF assms(1) divide_pos_pos[OF \<open>e > 0\<close> \<open>K * Km * 4 > 0\<close>]]
   1.430 +    uniform_limitD[OF assms(2) divide_pos_pos[OF \<open>e > 0\<close> \<open>K * Kl * 4 > 0\<close>]]
   1.431 +  show "\<forall>\<^sub>F n in F. \<forall>x\<in>X. dist (prod (f n x) (g n x)) (prod (l x) (m x)) < e"
   1.432 +  proof eventually_elim
   1.433 +    case (elim n)
   1.434 +    show ?case
   1.435 +    proof safe
   1.436 +      fix x assume "x \<in> X"
   1.437 +      have "dist (prod (f n x) (g n x)) (prod (l x) (m x)) \<le>
   1.438 +        norm (prod (f n x - l x) (g n x - m x)) +
   1.439 +        norm (prod (f n x - l x) (m x)) +
   1.440 +        norm (prod (l x) (g n x - m x))"
   1.441 +        by (auto simp: dist_norm prod_diff_prod intro: order_trans norm_triangle_ineq add_mono)
   1.442 +      also note K(2)[of "f n x - l x" "g n x - m x"]
   1.443 +      also from elim(1)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
   1.444 +      have "norm (f n x - l x) \<le> sqrt e / sqrt (K * 4)"
   1.445 +        by simp
   1.446 +      also from elim(2)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
   1.447 +      have "norm (g n x - m x) \<le> sqrt e / sqrt (K * 4)"
   1.448 +        by simp
   1.449 +      also have "sqrt e / sqrt (K * 4) * (sqrt e / sqrt (K * 4)) * K = e / 4"
   1.450 +        using \<open>K > 0\<close> \<open>e > 0\<close> by auto
   1.451 +      also note K(2)[of "f n x - l x" "m x"]
   1.452 +      also note K(2)[of "l x" "g n x - m x"]
   1.453 +      also from elim(3)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
   1.454 +      have "norm (f n x - l x) \<le> e / (K * Km * 4)"
   1.455 +        by simp
   1.456 +      also from elim(4)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
   1.457 +      have "norm (g n x - m x) \<le> e / (K * Kl * 4)"
   1.458 +        by simp
   1.459 +      also note Kl(2)[OF \<open>_ \<in> X\<close>]
   1.460 +      also note Km(2)[OF \<open>_ \<in> X\<close>]
   1.461 +      also have "e / (K * Km * 4) * Km * K = e / 4"
   1.462 +        using \<open>K > 0\<close> \<open>Km > 0\<close> by simp
   1.463 +      also have " Kl * (e / (K * Kl * 4)) * K = e / 4"
   1.464 +        using \<open>K > 0\<close> \<open>Kl > 0\<close> by simp
   1.465 +      also have "e / 4 + e / 4 + e / 4 < e" using \<open>e > 0\<close> by simp
   1.466 +      finally show "dist (prod (f n x) (g n x)) (prod (l x) (m x)) < e"
   1.467 +        using \<open>K > 0\<close> \<open>Kl > 0\<close> \<open>Km > 0\<close> \<open>e > 0\<close>
   1.468 +        by (simp add: algebra_simps mult_right_mono divide_right_mono)
   1.469 +    qed
   1.470 +  qed
   1.471 +qed
   1.472 +
   1.473 +lemmas bounded_bilinear_bounded_uniform_limit_intros[uniform_limit_intros] =
   1.474 +  bounded_bilinear.bounded_uniform_limit[OF Inner_Product.bounded_bilinear_inner]
   1.475 +  bounded_bilinear.bounded_uniform_limit[OF Real_Vector_Spaces.bounded_bilinear_mult]
   1.476 +  bounded_bilinear.bounded_uniform_limit[OF Real_Vector_Spaces.bounded_bilinear_scaleR]
   1.477 +
   1.478 +lemma uniform_limit_null_comparison:
   1.479 +  assumes "\<forall>\<^sub>F x in F. \<forall>a\<in>S. norm (f x a) \<le> g x a"
   1.480 +  assumes "uniform_limit S g (\<lambda>_. 0) F"
   1.481 +  shows "uniform_limit S f (\<lambda>_. 0) F"
   1.482 +  using assms(2)
   1.483 +proof (rule metric_uniform_limit_imp_uniform_limit)
   1.484 +  show "\<forall>\<^sub>F x in F. \<forall>y\<in>S. dist (f x y) 0 \<le> dist (g x y) 0"
   1.485 +    using assms(1) by (rule eventually_mono) (force simp add: dist_norm)
   1.486 +qed
   1.487 +
   1.488 +lemma uniform_limit_on_union:
   1.489 +  "uniform_limit I f g F \<Longrightarrow> uniform_limit J f g F \<Longrightarrow> uniform_limit (I \<union> J) f g F"
   1.490 +  by (auto intro!: uniform_limitI dest!: uniform_limitD elim: eventually_elim2)
   1.491 +
   1.492 +lemma uniform_limit_on_empty [iff]:
   1.493 +  "uniform_limit {} f g F"
   1.494 +  by (auto intro!: uniform_limitI)
   1.495 +
   1.496 +lemma uniform_limit_on_UNION:
   1.497 +  assumes "finite S"
   1.498 +  assumes "\<And>s. s \<in> S \<Longrightarrow> uniform_limit (h s) f g F"
   1.499 +  shows "uniform_limit (UNION S h) f g F"
   1.500 +  using assms
   1.501 +  by induct (auto intro: uniform_limit_on_empty uniform_limit_on_union)
   1.502 +
   1.503 +lemma uniform_limit_on_Union:
   1.504 +  assumes "finite I"
   1.505 +  assumes "\<And>J. J \<in> I \<Longrightarrow> uniform_limit J f g F"
   1.506 +  shows "uniform_limit (Union I) f g F"
   1.507 +  by (metis SUP_identity_eq assms uniform_limit_on_UNION)
   1.508 +
   1.509 +lemma uniform_limit_on_subset:
   1.510 +  "uniform_limit J f g F \<Longrightarrow> I \<subseteq> J \<Longrightarrow> uniform_limit I f g F"
   1.511 +  by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_mono)
   1.512 +
   1.513 +lemma uniformly_convergent_add:
   1.514 +  "uniformly_convergent_on A f \<Longrightarrow> uniformly_convergent_on A g\<Longrightarrow>
   1.515 +      uniformly_convergent_on A (\<lambda>k x. f k x + g k x :: 'a :: {real_normed_algebra})"
   1.516 +  unfolding uniformly_convergent_on_def by (blast dest: uniform_limit_add)
   1.517 +
   1.518 +lemma uniformly_convergent_minus:
   1.519 +  "uniformly_convergent_on A f \<Longrightarrow> uniformly_convergent_on A g\<Longrightarrow>
   1.520 +      uniformly_convergent_on A (\<lambda>k x. f k x - g k x :: 'a :: {real_normed_algebra})"
   1.521 +  unfolding uniformly_convergent_on_def by (blast dest: uniform_limit_minus)
   1.522 +
   1.523 +lemma uniformly_convergent_mult:
   1.524 +  "uniformly_convergent_on A f \<Longrightarrow>
   1.525 +      uniformly_convergent_on A (\<lambda>k x. c * f k x :: 'a :: {real_normed_algebra})"
   1.526 +  unfolding uniformly_convergent_on_def
   1.527 +  by (blast dest: bounded_linear_uniform_limit_intros(13))
   1.528 +
   1.529 +
   1.530 +subsection\<open>Power series and uniform convergence\<close>
   1.531 +
   1.532 +proposition powser_uniformly_convergent:
   1.533 +  fixes a :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
   1.534 +  assumes "r < conv_radius a"
   1.535 +  shows "uniformly_convergent_on (cball \<xi> r) (\<lambda>n x. \<Sum>i<n. a i * (x - \<xi>) ^ i)"
   1.536 +proof (cases "0 \<le> r")
   1.537 +  case True
   1.538 +  then have *: "summable (\<lambda>n. norm (a n) * r ^ n)"
   1.539 +    using abs_summable_in_conv_radius [of "of_real r" a] assms
   1.540 +    by (simp add: norm_mult norm_power)
   1.541 +  show ?thesis
   1.542 +    by (simp add: weierstrass_m_test'_ev [OF _ *] norm_mult norm_power
   1.543 +              mult_left_mono power_mono dist_norm norm_minus_commute)
   1.544 +next
   1.545 +  case False then show ?thesis by (simp add: not_le)
   1.546 +qed
   1.547 +
   1.548 +lemma powser_uniform_limit:
   1.549 +  fixes a :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
   1.550 +  assumes "r < conv_radius a"
   1.551 +  shows "uniform_limit (cball \<xi> r) (\<lambda>n x. \<Sum>i<n. a i * (x - \<xi>) ^ i) (\<lambda>x. suminf (\<lambda>i. a i * (x - \<xi>) ^ i)) sequentially"
   1.552 +using powser_uniformly_convergent [OF assms]
   1.553 +by (simp add: Uniform_Limit.uniformly_convergent_uniform_limit_iff Series.suminf_eq_lim)
   1.554 +
   1.555 +lemma powser_continuous_suminf:
   1.556 +  fixes a :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
   1.557 +  assumes "r < conv_radius a"
   1.558 +  shows "continuous_on (cball \<xi> r) (\<lambda>x. suminf (\<lambda>i. a i * (x - \<xi>) ^ i))"
   1.559 +apply (rule uniform_limit_theorem [OF _ powser_uniform_limit])
   1.560 +apply (rule eventuallyI continuous_intros assms)+
   1.561 +apply (simp add:)
   1.562 +done
   1.563 +
   1.564 +lemma powser_continuous_sums:
   1.565 +  fixes a :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
   1.566 +  assumes r: "r < conv_radius a"
   1.567 +      and sm: "\<And>x. x \<in> cball \<xi> r \<Longrightarrow> (\<lambda>n. a n * (x - \<xi>) ^ n) sums (f x)"
   1.568 +  shows "continuous_on (cball \<xi> r) f"
   1.569 +apply (rule continuous_on_cong [THEN iffD1, OF refl _ powser_continuous_suminf [OF r]])
   1.570 +using sm sums_unique by fastforce
   1.571 +
   1.572 +end
   1.573 +