src/HOL/Analysis/Uniform_Limit.thy
 author paulson Tue Feb 21 17:12:10 2017 +0000 (2017-02-21) changeset 65037 2cf841ff23be parent 65036 ab7e11730ad8 child 65204 d23eded35a33 permissions -rw-r--r--
some new material, also recasting some theorems using “obtains”
```     1 (*  Title:      HOL/Analysis/Uniform_Limit.thy
```
```     2     Author:     Christoph Traut, TU München
```
```     3     Author:     Fabian Immler, TU München
```
```     4 *)
```
```     5
```
```     6 section \<open>Uniform Limit and Uniform Convergence\<close>
```
```     7
```
```     8 theory Uniform_Limit
```
```     9 imports Topology_Euclidean_Space Summation_Tests
```
```    10 begin
```
```    11
```
```    12 definition uniformly_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> ('a \<Rightarrow> 'b) filter"
```
```    13   where "uniformly_on S l = (INF e:{0 <..}. principal {f. \<forall>x\<in>S. dist (f x) (l x) < e})"
```
```    14
```
```    15 abbreviation
```
```    16   "uniform_limit S f l \<equiv> filterlim f (uniformly_on S l)"
```
```    17
```
```    18 definition uniformly_convergent_on where
```
```    19   "uniformly_convergent_on X f \<longleftrightarrow> (\<exists>l. uniform_limit X f l sequentially)"
```
```    20
```
```    21 definition uniformly_Cauchy_on where
```
```    22   "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)"
```
```    23
```
```    24 lemma uniform_limit_iff:
```
```    25   "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)"
```
```    26   unfolding filterlim_iff uniformly_on_def
```
```    27   by (subst eventually_INF_base)
```
```    28     (fastforce
```
```    29       simp: eventually_principal uniformly_on_def
```
```    30       intro: bexI[where x="min a b" for a b]
```
```    31       elim: eventually_mono)+
```
```    32
```
```    33 lemma uniform_limitD:
```
```    34   "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"
```
```    35   by (simp add: uniform_limit_iff)
```
```    36
```
```    37 lemma uniform_limitI:
```
```    38   "(\<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"
```
```    39   by (simp add: uniform_limit_iff)
```
```    40
```
```    41 lemma uniform_limit_sequentially_iff:
```
```    42   "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)"
```
```    43   unfolding uniform_limit_iff eventually_sequentially ..
```
```    44
```
```    45 lemma uniform_limit_at_iff:
```
```    46   "uniform_limit S f l (at x) \<longleftrightarrow>
```
```    47     (\<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))"
```
```    48   unfolding uniform_limit_iff eventually_at by simp
```
```    49
```
```    50 lemma uniform_limit_at_le_iff:
```
```    51   "uniform_limit S f l (at x) \<longleftrightarrow>
```
```    52     (\<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))"
```
```    53   unfolding uniform_limit_iff eventually_at
```
```    54   by (fastforce dest: spec[where x = "e / 2" for e])
```
```    55
```
```    56 lemma metric_uniform_limit_imp_uniform_limit:
```
```    57   assumes f: "uniform_limit S f a F"
```
```    58   assumes le: "eventually (\<lambda>x. \<forall>y\<in>S. dist (g x y) (b y) \<le> dist (f x y) (a y)) F"
```
```    59   shows "uniform_limit S g b F"
```
```    60 proof (rule uniform_limitI)
```
```    61   fix e :: real assume "0 < e"
```
```    62   from uniform_limitD[OF f this] le
```
```    63   show "\<forall>\<^sub>F x in F. \<forall>y\<in>S. dist (g x y) (b y) < e"
```
```    64     by eventually_elim force
```
```    65 qed
```
```    66
```
```    67 lemma swap_uniform_limit:
```
```    68   assumes f: "\<forall>\<^sub>F n in F. (f n \<longlongrightarrow> g n) (at x within S)"
```
```    69   assumes g: "(g \<longlongrightarrow> l) F"
```
```    70   assumes uc: "uniform_limit S f h F"
```
```    71   assumes "\<not>trivial_limit F"
```
```    72   shows "(h \<longlongrightarrow> l) (at x within S)"
```
```    73 proof (rule tendstoI)
```
```    74   fix e :: real
```
```    75   define e' where "e' = e/3"
```
```    76   assume "0 < e"
```
```    77   then have "0 < e'" by (simp add: e'_def)
```
```    78   from uniform_limitD[OF uc \<open>0 < e'\<close>]
```
```    79   have "\<forall>\<^sub>F n in F. \<forall>x\<in>S. dist (h x) (f n x) < e'"
```
```    80     by (simp add: dist_commute)
```
```    81   moreover
```
```    82   from f
```
```    83   have "\<forall>\<^sub>F n in F. \<forall>\<^sub>F x in at x within S. dist (g n) (f n x) < e'"
```
```    84     by eventually_elim (auto dest!: tendstoD[OF _ \<open>0 < e'\<close>] simp: dist_commute)
```
```    85   moreover
```
```    86   from tendstoD[OF g \<open>0 < e'\<close>] have "\<forall>\<^sub>F x in F. dist l (g x) < e'"
```
```    87     by (simp add: dist_commute)
```
```    88   ultimately
```
```    89   have "\<forall>\<^sub>F _ in F. \<forall>\<^sub>F x in at x within S. dist (h x) l < e"
```
```    90   proof eventually_elim
```
```    91     case (elim n)
```
```    92     note fh = elim(1)
```
```    93     note gl = elim(3)
```
```    94     have "\<forall>\<^sub>F x in at x within S. x \<in> S"
```
```    95       by (auto simp: eventually_at_filter)
```
```    96     with elim(2)
```
```    97     show ?case
```
```    98     proof eventually_elim
```
```    99       case (elim x)
```
```   100       from fh[rule_format, OF \<open>x \<in> S\<close>] elim(1)
```
```   101       have "dist (h x) (g n) < e' + e'"
```
```   102         by (rule dist_triangle_lt[OF add_strict_mono])
```
```   103       from dist_triangle_lt[OF add_strict_mono, OF this gl]
```
```   104       show ?case by (simp add: e'_def)
```
```   105     qed
```
```   106   qed
```
```   107   thus "\<forall>\<^sub>F x in at x within S. dist (h x) l < e"
```
```   108     using eventually_happens by (metis \<open>\<not>trivial_limit F\<close>)
```
```   109 qed
```
```   110
```
```   111 lemma
```
```   112   tendsto_uniform_limitI:
```
```   113   assumes "uniform_limit S f l F"
```
```   114   assumes "x \<in> S"
```
```   115   shows "((\<lambda>y. f y x) \<longlongrightarrow> l x) F"
```
```   116   using assms
```
```   117   by (auto intro!: tendstoI simp: eventually_mono dest!: uniform_limitD)
```
```   118
```
```   119 lemma uniform_limit_theorem:
```
```   120   assumes c: "\<forall>\<^sub>F n in F. continuous_on A (f n)"
```
```   121   assumes ul: "uniform_limit A f l F"
```
```   122   assumes "\<not> trivial_limit F"
```
```   123   shows "continuous_on A l"
```
```   124   unfolding continuous_on_def
```
```   125 proof safe
```
```   126   fix x assume "x \<in> A"
```
```   127   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"
```
```   128     using c ul
```
```   129     by (auto simp: continuous_on_def eventually_mono tendsto_uniform_limitI)
```
```   130   then show "(l \<longlongrightarrow> l x) (at x within A)"
```
```   131     by (rule swap_uniform_limit) fact+
```
```   132 qed
```
```   133
```
```   134 lemma uniformly_Cauchy_onI:
```
```   135   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"
```
```   136   shows   "uniformly_Cauchy_on X f"
```
```   137   using assms unfolding uniformly_Cauchy_on_def by blast
```
```   138
```
```   139 lemma uniformly_Cauchy_onI':
```
```   140   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"
```
```   141   shows   "uniformly_Cauchy_on X f"
```
```   142 proof (rule uniformly_Cauchy_onI)
```
```   143   fix e :: real assume e: "e > 0"
```
```   144   from assms[OF this] obtain M
```
```   145     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
```
```   146   {
```
```   147     fix x m n assume x: "x \<in> X" and m: "m \<ge> M" and n: "n \<ge> M"
```
```   148     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"
```
```   149       by (cases m n rule: linorder_cases) (simp_all add: dist_commute)
```
```   150   }
```
```   151   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
```
```   152 qed
```
```   153
```
```   154 lemma uniformly_Cauchy_imp_Cauchy:
```
```   155   "uniformly_Cauchy_on X f \<Longrightarrow> x \<in> X \<Longrightarrow> Cauchy (\<lambda>n. f n x)"
```
```   156   unfolding Cauchy_def uniformly_Cauchy_on_def by fast
```
```   157
```
```   158 lemma uniform_limit_cong:
```
```   159   fixes f g :: "'a \<Rightarrow> 'b \<Rightarrow> ('c :: metric_space)" and h i :: "'b \<Rightarrow> 'c"
```
```   160   assumes "eventually (\<lambda>y. \<forall>x\<in>X. f y x = g y x) F"
```
```   161   assumes "\<And>x. x \<in> X \<Longrightarrow> h x = i x"
```
```   162   shows   "uniform_limit X f h F \<longleftrightarrow> uniform_limit X g i F"
```
```   163 proof -
```
```   164   {
```
```   165     fix f g :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" and h i :: "'b \<Rightarrow> 'c"
```
```   166     assume C: "uniform_limit X f h F" and A: "eventually (\<lambda>y. \<forall>x\<in>X. f y x = g y x) F"
```
```   167        and B: "\<And>x. x \<in> X \<Longrightarrow> h x = i x"
```
```   168     {
```
```   169       fix e ::real assume "e > 0"
```
```   170       with C have "eventually (\<lambda>y. \<forall>x\<in>X. dist (f y x) (h x) < e) F"
```
```   171         unfolding uniform_limit_iff by blast
```
```   172       with A have "eventually (\<lambda>y. \<forall>x\<in>X. dist (g y x) (i x) < e) F"
```
```   173         by eventually_elim (insert B, simp_all)
```
```   174     }
```
```   175     hence "uniform_limit X g i F" unfolding uniform_limit_iff by blast
```
```   176   } note A = this
```
```   177   show ?thesis by (rule iffI) (erule A; insert assms; simp add: eq_commute)+
```
```   178 qed
```
```   179
```
```   180 lemma uniform_limit_cong':
```
```   181   fixes f g :: "'a \<Rightarrow> 'b \<Rightarrow> ('c :: metric_space)" and h i :: "'b \<Rightarrow> 'c"
```
```   182   assumes "\<And>y x. x \<in> X \<Longrightarrow> f y x = g y x"
```
```   183   assumes "\<And>x. x \<in> X \<Longrightarrow> h x = i x"
```
```   184   shows   "uniform_limit X f h F \<longleftrightarrow> uniform_limit X g i F"
```
```   185   using assms by (intro uniform_limit_cong always_eventually) blast+
```
```   186
```
```   187 lemma uniformly_convergent_uniform_limit_iff:
```
```   188   "uniformly_convergent_on X f \<longleftrightarrow> uniform_limit X f (\<lambda>x. lim (\<lambda>n. f n x)) sequentially"
```
```   189 proof
```
```   190   assume "uniformly_convergent_on X f"
```
```   191   then obtain l where l: "uniform_limit X f l sequentially"
```
```   192     unfolding uniformly_convergent_on_def by blast
```
```   193   from l have "uniform_limit X f (\<lambda>x. lim (\<lambda>n. f n x)) sequentially \<longleftrightarrow>
```
```   194                       uniform_limit X f l sequentially"
```
```   195     by (intro uniform_limit_cong' limI tendsto_uniform_limitI[of f X l]) simp_all
```
```   196   also note l
```
```   197   finally show "uniform_limit X f (\<lambda>x. lim (\<lambda>n. f n x)) sequentially" .
```
```   198 qed (auto simp: uniformly_convergent_on_def)
```
```   199
```
```   200 lemma uniformly_convergentI: "uniform_limit X f l sequentially \<Longrightarrow> uniformly_convergent_on X f"
```
```   201   unfolding uniformly_convergent_on_def by blast
```
```   202
```
```   203 lemma uniformly_convergent_on_empty [iff]: "uniformly_convergent_on {} f"
```
```   204   by (simp add: uniformly_convergent_on_def uniform_limit_sequentially_iff)
```
```   205
```
```   206 lemma Cauchy_uniformly_convergent:
```
```   207   fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b :: complete_space"
```
```   208   assumes "uniformly_Cauchy_on X f"
```
```   209   shows   "uniformly_convergent_on X f"
```
```   210 unfolding uniformly_convergent_uniform_limit_iff uniform_limit_iff
```
```   211 proof safe
```
```   212   let ?f = "\<lambda>x. lim (\<lambda>n. f n x)"
```
```   213   fix e :: real assume e: "e > 0"
```
```   214   hence "e/2 > 0" by simp
```
```   215   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"
```
```   216     unfolding uniformly_Cauchy_on_def by fast
```
```   217   show "eventually (\<lambda>n. \<forall>x\<in>X. dist (f n x) (?f x) < e) sequentially"
```
```   218     using eventually_ge_at_top[of N]
```
```   219   proof eventually_elim
```
```   220     fix n assume n: "n \<ge> N"
```
```   221     show "\<forall>x\<in>X. dist (f n x) (?f x) < e"
```
```   222     proof
```
```   223       fix x assume x: "x \<in> X"
```
```   224       with assms have "(\<lambda>n. f n x) \<longlonglongrightarrow> ?f x"
```
```   225         by (auto dest!: Cauchy_convergent uniformly_Cauchy_imp_Cauchy simp: convergent_LIMSEQ_iff)
```
```   226       with \<open>e/2 > 0\<close> have "eventually (\<lambda>m. m \<ge> N \<and> dist (f m x) (?f x) < e/2) sequentially"
```
```   227         by (intro tendstoD eventually_conj eventually_ge_at_top)
```
```   228       then obtain m where m: "m \<ge> N" "dist (f m x) (?f x) < e/2"
```
```   229         unfolding eventually_at_top_linorder by blast
```
```   230       have "dist (f n x) (?f x) \<le> dist (f n x) (f m x) + dist (f m x) (?f x)"
```
```   231           by (rule dist_triangle)
```
```   232       also from x n have "... < e/2 + e/2" by (intro add_strict_mono N m)
```
```   233       finally show "dist (f n x) (?f x) < e" by simp
```
```   234     qed
```
```   235   qed
```
```   236 qed
```
```   237
```
```   238 lemma uniformly_convergent_imp_convergent:
```
```   239   "uniformly_convergent_on X f \<Longrightarrow> x \<in> X \<Longrightarrow> convergent (\<lambda>n. f n x)"
```
```   240   unfolding uniformly_convergent_on_def convergent_def
```
```   241   by (auto dest: tendsto_uniform_limitI)
```
```   242
```
```   243 lemma weierstrass_m_test_ev:
```
```   244 fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
```
```   245 assumes "eventually (\<lambda>n. \<forall>x\<in>A. norm (f n x) \<le> M n) sequentially"
```
```   246 assumes "summable M"
```
```   247 shows "uniform_limit A (\<lambda>n x. \<Sum>i<n. f i x) (\<lambda>x. suminf (\<lambda>i. f i x)) sequentially"
```
```   248 proof (rule uniform_limitI)
```
```   249   fix e :: real
```
```   250   assume "0 < e"
```
```   251   from suminf_exist_split[OF \<open>0 < e\<close> \<open>summable M\<close>]
```
```   252   have "\<forall>\<^sub>F k in sequentially. norm (\<Sum>i. M (i + k)) < e"
```
```   253     by (auto simp: eventually_sequentially)
```
```   254   with eventually_all_ge_at_top[OF assms(1)]
```
```   255     show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>A. dist (\<Sum>i<n. f i x) (\<Sum>i. f i x) < e"
```
```   256   proof eventually_elim
```
```   257     case (elim k)
```
```   258     show ?case
```
```   259     proof safe
```
```   260       fix x assume "x \<in> A"
```
```   261       have "\<exists>N. \<forall>n\<ge>N. norm (f n x) \<le> M n"
```
```   262         using assms(1) \<open>x \<in> A\<close> by (force simp: eventually_at_top_linorder)
```
```   263       hence summable_norm_f: "summable (\<lambda>n. norm (f n x))"
```
```   264         by(rule summable_norm_comparison_test[OF _ \<open>summable M\<close>])
```
```   265       have summable_f: "summable (\<lambda>n. f n x)"
```
```   266         using summable_norm_cancel[OF summable_norm_f] .
```
```   267       have summable_norm_f_plus_k: "summable (\<lambda>i. norm (f (i + k) x))"
```
```   268         using summable_ignore_initial_segment[OF summable_norm_f]
```
```   269         by auto
```
```   270       have summable_M_plus_k: "summable (\<lambda>i. M (i + k))"
```
```   271         using summable_ignore_initial_segment[OF \<open>summable M\<close>]
```
```   272         by auto
```
```   273
```
```   274       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))"
```
```   275         using dist_norm dist_commute by (subst dist_commute)
```
```   276       also have "... = norm (\<Sum>i. f (i + k) x)"
```
```   277         using suminf_minus_initial_segment[OF summable_f, where k=k] by simp
```
```   278       also have "... \<le> (\<Sum>i. norm (f (i + k) x))"
```
```   279         using summable_norm[OF summable_norm_f_plus_k] .
```
```   280       also have "... \<le> (\<Sum>i. M (i + k))"
```
```   281         by (rule suminf_le[OF _ summable_norm_f_plus_k summable_M_plus_k])
```
```   282            (insert elim(1) \<open>x \<in> A\<close>, simp)
```
```   283       finally show "dist (\<Sum>i<k. f i x) (\<Sum>i. f i x) < e"
```
```   284         using elim by auto
```
```   285     qed
```
```   286   qed
```
```   287 qed
```
```   288
```
```   289 text\<open>Alternative version, formulated as in HOL Light\<close>
```
```   290 corollary series_comparison_uniform:
```
```   291   fixes f :: "_ \<Rightarrow> nat \<Rightarrow> _ :: banach"
```
```   292   assumes g: "summable g" and le: "\<And>n x. N \<le> n \<and> x \<in> A \<Longrightarrow> norm(f x n) \<le> g n"
```
```   293     shows "\<exists>l. \<forall>e. 0 < e \<longrightarrow> (\<exists>N. \<forall>n x. N \<le> n \<and> x \<in> A \<longrightarrow> dist(sum (f x) {..<n}) (l x) < e)"
```
```   294 proof -
```
```   295   have 1: "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>A. norm (f x n) \<le> g n"
```
```   296     using le eventually_sequentially by auto
```
```   297   show ?thesis
```
```   298     apply (rule_tac x="(\<lambda>x. \<Sum>i. f x i)" in exI)
```
```   299     apply (metis (no_types, lifting) eventually_sequentially uniform_limitD [OF weierstrass_m_test_ev [OF 1 g]])
```
```   300     done
```
```   301 qed
```
```   302
```
```   303 corollary weierstrass_m_test:
```
```   304   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
```
```   305   assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> M n"
```
```   306   assumes "summable M"
```
```   307   shows "uniform_limit A (\<lambda>n x. \<Sum>i<n. f i x) (\<lambda>x. suminf (\<lambda>i. f i x)) sequentially"
```
```   308   using assms by (intro weierstrass_m_test_ev always_eventually) auto
```
```   309
```
```   310 corollary weierstrass_m_test'_ev:
```
```   311   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
```
```   312   assumes "eventually (\<lambda>n. \<forall>x\<in>A. norm (f n x) \<le> M n) sequentially" "summable M"
```
```   313   shows   "uniformly_convergent_on A (\<lambda>n x. \<Sum>i<n. f i x)"
```
```   314   unfolding uniformly_convergent_on_def by (rule exI, rule weierstrass_m_test_ev[OF assms])
```
```   315
```
```   316 corollary weierstrass_m_test':
```
```   317   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
```
```   318   assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> M n" "summable M"
```
```   319   shows   "uniformly_convergent_on A (\<lambda>n x. \<Sum>i<n. f i x)"
```
```   320   unfolding uniformly_convergent_on_def by (rule exI, rule weierstrass_m_test[OF assms])
```
```   321
```
```   322 lemma uniform_limit_eq_rhs: "uniform_limit X f l F \<Longrightarrow> l = m \<Longrightarrow> uniform_limit X f m F"
```
```   323   by simp
```
```   324
```
```   325 named_theorems uniform_limit_intros "introduction rules for uniform_limit"
```
```   326 setup \<open>
```
```   327   Global_Theory.add_thms_dynamic (@{binding uniform_limit_eq_intros},
```
```   328     fn context =>
```
```   329       Named_Theorems.get (Context.proof_of context) @{named_theorems uniform_limit_intros}
```
```   330       |> map_filter (try (fn thm => @{thm uniform_limit_eq_rhs} OF [thm])))
```
```   331 \<close>
```
```   332
```
```   333 lemma (in bounded_linear) uniform_limit[uniform_limit_intros]:
```
```   334   assumes "uniform_limit X g l F"
```
```   335   shows "uniform_limit X (\<lambda>a b. f (g a b)) (\<lambda>a. f (l a)) F"
```
```   336 proof (rule uniform_limitI)
```
```   337   fix e::real
```
```   338   from pos_bounded obtain K
```
```   339     where K: "\<And>x y. dist (f x) (f y) \<le> K * dist x y" "K > 0"
```
```   340     by (auto simp: ac_simps dist_norm diff[symmetric])
```
```   341   assume "0 < e" with \<open>K > 0\<close> have "e / K > 0" by simp
```
```   342   from uniform_limitD[OF assms this]
```
```   343   show "\<forall>\<^sub>F n in F. \<forall>x\<in>X. dist (f (g n x)) (f (l x)) < e"
```
```   344     by eventually_elim (metis le_less_trans mult.commute pos_less_divide_eq K)
```
```   345 qed
```
```   346
```
```   347 lemmas bounded_linear_uniform_limit_intros[uniform_limit_intros] =
```
```   348   bounded_linear.uniform_limit[OF bounded_linear_Im]
```
```   349   bounded_linear.uniform_limit[OF bounded_linear_Re]
```
```   350   bounded_linear.uniform_limit[OF bounded_linear_cnj]
```
```   351   bounded_linear.uniform_limit[OF bounded_linear_fst]
```
```   352   bounded_linear.uniform_limit[OF bounded_linear_snd]
```
```   353   bounded_linear.uniform_limit[OF bounded_linear_zero]
```
```   354   bounded_linear.uniform_limit[OF bounded_linear_of_real]
```
```   355   bounded_linear.uniform_limit[OF bounded_linear_inner_left]
```
```   356   bounded_linear.uniform_limit[OF bounded_linear_inner_right]
```
```   357   bounded_linear.uniform_limit[OF bounded_linear_divide]
```
```   358   bounded_linear.uniform_limit[OF bounded_linear_scaleR_right]
```
```   359   bounded_linear.uniform_limit[OF bounded_linear_mult_left]
```
```   360   bounded_linear.uniform_limit[OF bounded_linear_mult_right]
```
```   361   bounded_linear.uniform_limit[OF bounded_linear_scaleR_left]
```
```   362
```
```   363 lemmas uniform_limit_uminus[uniform_limit_intros] =
```
```   364   bounded_linear.uniform_limit[OF bounded_linear_minus[OF bounded_linear_ident]]
```
```   365
```
```   366 lemma uniform_limit_const[uniform_limit_intros]: "uniform_limit S (\<lambda>x y. c) (\<lambda>x. c) f"
```
```   367   by (auto intro!: uniform_limitI)
```
```   368
```
```   369 lemma uniform_limit_add[uniform_limit_intros]:
```
```   370   fixes f g::"'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_vector"
```
```   371   assumes "uniform_limit X f l F"
```
```   372   assumes "uniform_limit X g m F"
```
```   373   shows "uniform_limit X (\<lambda>a b. f a b + g a b) (\<lambda>a. l a + m a) F"
```
```   374 proof (rule uniform_limitI)
```
```   375   fix e::real
```
```   376   assume "0 < e"
```
```   377   hence "0 < e / 2" by simp
```
```   378   from
```
```   379     uniform_limitD[OF assms(1) this]
```
```   380     uniform_limitD[OF assms(2) this]
```
```   381   show "\<forall>\<^sub>F n in F. \<forall>x\<in>X. dist (f n x + g n x) (l x + m x) < e"
```
```   382     by eventually_elim (simp add: dist_triangle_add_half)
```
```   383 qed
```
```   384
```
```   385 lemma uniform_limit_minus[uniform_limit_intros]:
```
```   386   fixes f g::"'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_vector"
```
```   387   assumes "uniform_limit X f l F"
```
```   388   assumes "uniform_limit X g m F"
```
```   389   shows "uniform_limit X (\<lambda>a b. f a b - g a b) (\<lambda>a. l a - m a) F"
```
```   390   unfolding diff_conv_add_uminus
```
```   391   by (rule uniform_limit_intros assms)+
```
```   392
```
```   393 lemma uniform_limit_norm[uniform_limit_intros]:
```
```   394   assumes "uniform_limit S g l f"
```
```   395   shows "uniform_limit S (\<lambda>x y. norm (g x y)) (\<lambda>x. norm (l x)) f"
```
```   396   using assms
```
```   397   apply (rule metric_uniform_limit_imp_uniform_limit)
```
```   398   apply (rule eventuallyI)
```
```   399   by (metis dist_norm norm_triangle_ineq3 real_norm_def)
```
```   400
```
```   401 lemma (in bounded_bilinear) bounded_uniform_limit[uniform_limit_intros]:
```
```   402   assumes "uniform_limit X f l F"
```
```   403   assumes "uniform_limit X g m F"
```
```   404   assumes "bounded (m ` X)"
```
```   405   assumes "bounded (l ` X)"
```
```   406   shows "uniform_limit X (\<lambda>a b. prod (f a b) (g a b)) (\<lambda>a. prod (l a) (m a)) F"
```
```   407 proof (rule uniform_limitI)
```
```   408   fix e::real
```
```   409   from pos_bounded obtain K where K:
```
```   410     "0 < K" "\<And>a b. norm (prod a b) \<le> norm a * norm b * K"
```
```   411     by auto
```
```   412   hence "sqrt (K*4) > 0" by simp
```
```   413
```
```   414   from assms obtain Km Kl
```
```   415   where Km: "Km > 0" "\<And>x. x \<in> X \<Longrightarrow> norm (m x) \<le> Km"
```
```   416     and Kl: "Kl > 0" "\<And>x. x \<in> X \<Longrightarrow> norm (l x) \<le> Kl"
```
```   417     by (auto simp: bounded_pos)
```
```   418   hence "K * Km * 4 > 0" "K * Kl * 4 > 0"
```
```   419     using \<open>K > 0\<close>
```
```   420     by simp_all
```
```   421   assume "0 < e"
```
```   422
```
```   423   hence "sqrt e > 0" by simp
```
```   424   from uniform_limitD[OF assms(1) divide_pos_pos[OF this \<open>sqrt (K*4) > 0\<close>]]
```
```   425     uniform_limitD[OF assms(2) divide_pos_pos[OF this \<open>sqrt (K*4) > 0\<close>]]
```
```   426     uniform_limitD[OF assms(1) divide_pos_pos[OF \<open>e > 0\<close> \<open>K * Km * 4 > 0\<close>]]
```
```   427     uniform_limitD[OF assms(2) divide_pos_pos[OF \<open>e > 0\<close> \<open>K * Kl * 4 > 0\<close>]]
```
```   428   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"
```
```   429   proof eventually_elim
```
```   430     case (elim n)
```
```   431     show ?case
```
```   432     proof safe
```
```   433       fix x assume "x \<in> X"
```
```   434       have "dist (prod (f n x) (g n x)) (prod (l x) (m x)) \<le>
```
```   435         norm (prod (f n x - l x) (g n x - m x)) +
```
```   436         norm (prod (f n x - l x) (m x)) +
```
```   437         norm (prod (l x) (g n x - m x))"
```
```   438         by (auto simp: dist_norm prod_diff_prod intro: order_trans norm_triangle_ineq add_mono)
```
```   439       also note K(2)[of "f n x - l x" "g n x - m x"]
```
```   440       also from elim(1)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
```
```   441       have "norm (f n x - l x) \<le> sqrt e / sqrt (K * 4)"
```
```   442         by simp
```
```   443       also from elim(2)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
```
```   444       have "norm (g n x - m x) \<le> sqrt e / sqrt (K * 4)"
```
```   445         by simp
```
```   446       also have "sqrt e / sqrt (K * 4) * (sqrt e / sqrt (K * 4)) * K = e / 4"
```
```   447         using \<open>K > 0\<close> \<open>e > 0\<close> by auto
```
```   448       also note K(2)[of "f n x - l x" "m x"]
```
```   449       also note K(2)[of "l x" "g n x - m x"]
```
```   450       also from elim(3)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
```
```   451       have "norm (f n x - l x) \<le> e / (K * Km * 4)"
```
```   452         by simp
```
```   453       also from elim(4)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
```
```   454       have "norm (g n x - m x) \<le> e / (K * Kl * 4)"
```
```   455         by simp
```
```   456       also note Kl(2)[OF \<open>_ \<in> X\<close>]
```
```   457       also note Km(2)[OF \<open>_ \<in> X\<close>]
```
```   458       also have "e / (K * Km * 4) * Km * K = e / 4"
```
```   459         using \<open>K > 0\<close> \<open>Km > 0\<close> by simp
```
```   460       also have " Kl * (e / (K * Kl * 4)) * K = e / 4"
```
```   461         using \<open>K > 0\<close> \<open>Kl > 0\<close> by simp
```
```   462       also have "e / 4 + e / 4 + e / 4 < e" using \<open>e > 0\<close> by simp
```
```   463       finally show "dist (prod (f n x) (g n x)) (prod (l x) (m x)) < e"
```
```   464         using \<open>K > 0\<close> \<open>Kl > 0\<close> \<open>Km > 0\<close> \<open>e > 0\<close>
```
```   465         by (simp add: algebra_simps mult_right_mono divide_right_mono)
```
```   466     qed
```
```   467   qed
```
```   468 qed
```
```   469
```
```   470 lemmas bounded_bilinear_bounded_uniform_limit_intros[uniform_limit_intros] =
```
```   471   bounded_bilinear.bounded_uniform_limit[OF Inner_Product.bounded_bilinear_inner]
```
```   472   bounded_bilinear.bounded_uniform_limit[OF Real_Vector_Spaces.bounded_bilinear_mult]
```
```   473   bounded_bilinear.bounded_uniform_limit[OF Real_Vector_Spaces.bounded_bilinear_scaleR]
```
```   474
```
```   475 lemma uniform_lim_mult:
```
```   476   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_algebra"
```
```   477   assumes f: "uniform_limit S f l F"
```
```   478       and g: "uniform_limit S g m F"
```
```   479       and l: "bounded (l ` S)"
```
```   480       and m: "bounded (m ` S)"
```
```   481     shows "uniform_limit S (\<lambda>a b. f a b * g a b) (\<lambda>a. l a * m a) F"
```
```   482   by (intro bounded_bilinear_bounded_uniform_limit_intros assms)
```
```   483
```
```   484 lemma uniform_lim_inverse:
```
```   485   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_field"
```
```   486   assumes f: "uniform_limit S f l F"
```
```   487       and b: "\<And>x. x \<in> S \<Longrightarrow> b \<le> norm(l x)"
```
```   488       and "b > 0"
```
```   489     shows "uniform_limit S (\<lambda>x y. inverse (f x y)) (inverse \<circ> l) F"
```
```   490 proof (rule uniform_limitI)
```
```   491   fix e::real
```
```   492   assume "e > 0"
```
```   493   have lte: "dist (inverse (f x y)) ((inverse \<circ> l) y) < e"
```
```   494            if "b/2 \<le> norm (f x y)" "norm (f x y - l y) < e * b\<^sup>2 / 2" "y \<in> S"
```
```   495            for x y
```
```   496   proof -
```
```   497     have [simp]: "l y \<noteq> 0" "f x y \<noteq> 0"
```
```   498       using \<open>b > 0\<close> that b [OF \<open>y \<in> S\<close>] by fastforce+
```
```   499     have "norm (l y - f x y) <  e * b\<^sup>2 / 2"
```
```   500       by (metis norm_minus_commute that(2))
```
```   501     also have "... \<le> e * (norm (f x y) * norm (l y))"
```
```   502       using \<open>e > 0\<close> that b [OF \<open>y \<in> S\<close>] apply (simp add: power2_eq_square)
```
```   503       by (metis \<open>b > 0\<close> less_eq_real_def mult.left_commute mult_mono')
```
```   504     finally show ?thesis
```
```   505       by (auto simp: dist_norm divide_simps norm_mult norm_divide)
```
```   506   qed
```
```   507   have "\<forall>\<^sub>F n in F. \<forall>x\<in>S. dist (f n x) (l x) < b/2"
```
```   508     using uniform_limitD [OF f, of "b/2"] by (simp add: \<open>b > 0\<close>)
```
```   509   then have "\<forall>\<^sub>F x in F. \<forall>y\<in>S. b/2 \<le> norm (f x y)"
```
```   510     apply (rule eventually_mono)
```
```   511     using b apply (simp only: dist_norm)
```
```   512     by (metis (no_types, hide_lams) diff_zero dist_commute dist_norm norm_triangle_half_l not_less)
```
```   513   then have "\<forall>\<^sub>F x in F. \<forall>y\<in>S. b/2 \<le> norm (f x y) \<and> norm (f x y - l y) < e * b\<^sup>2 / 2"
```
```   514     apply (simp only: ball_conj_distrib dist_norm [symmetric])
```
```   515     apply (rule eventually_conj, assumption)
```
```   516       apply (rule uniform_limitD [OF f, of "e * b ^ 2 / 2"])
```
```   517     using \<open>b > 0\<close> \<open>e > 0\<close> by auto
```
```   518   then show "\<forall>\<^sub>F x in F. \<forall>y\<in>S. dist (inverse (f x y)) ((inverse \<circ> l) y) < e"
```
```   519     using lte by (force intro: eventually_mono)
```
```   520 qed
```
```   521
```
```   522 lemma uniform_lim_divide:
```
```   523   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_field"
```
```   524   assumes f: "uniform_limit S f l F"
```
```   525       and g: "uniform_limit S g m F"
```
```   526       and l: "bounded (l ` S)"
```
```   527       and b: "\<And>x. x \<in> S \<Longrightarrow> b \<le> norm(m x)"
```
```   528       and "b > 0"
```
```   529     shows "uniform_limit S (\<lambda>a b. f a b / g a b) (\<lambda>a. l a / m a) F"
```
```   530 proof -
```
```   531   have m: "bounded ((inverse \<circ> m) ` S)"
```
```   532     using b \<open>b > 0\<close>
```
```   533     apply (simp add: bounded_iff)
```
```   534     by (metis le_imp_inverse_le norm_inverse)
```
```   535   have "uniform_limit S (\<lambda>a b. f a b * inverse (g a b))
```
```   536          (\<lambda>a. l a * (inverse \<circ> m) a) F"
```
```   537     by (rule uniform_lim_mult [OF f uniform_lim_inverse [OF g b \<open>b > 0\<close>] l m])
```
```   538   then show ?thesis
```
```   539     by (simp add: field_class.field_divide_inverse)
```
```   540 qed
```
```   541
```
```   542 lemma uniform_limit_null_comparison:
```
```   543   assumes "\<forall>\<^sub>F x in F. \<forall>a\<in>S. norm (f x a) \<le> g x a"
```
```   544   assumes "uniform_limit S g (\<lambda>_. 0) F"
```
```   545   shows "uniform_limit S f (\<lambda>_. 0) F"
```
```   546   using assms(2)
```
```   547 proof (rule metric_uniform_limit_imp_uniform_limit)
```
```   548   show "\<forall>\<^sub>F x in F. \<forall>y\<in>S. dist (f x y) 0 \<le> dist (g x y) 0"
```
```   549     using assms(1) by (rule eventually_mono) (force simp add: dist_norm)
```
```   550 qed
```
```   551
```
```   552 lemma uniform_limit_on_Un:
```
```   553   "uniform_limit I f g F \<Longrightarrow> uniform_limit J f g F \<Longrightarrow> uniform_limit (I \<union> J) f g F"
```
```   554   by (auto intro!: uniform_limitI dest!: uniform_limitD elim: eventually_elim2)
```
```   555
```
```   556 lemma uniform_limit_on_empty [iff]:
```
```   557   "uniform_limit {} f g F"
```
```   558   by (auto intro!: uniform_limitI)
```
```   559
```
```   560 lemma uniform_limit_on_UNION:
```
```   561   assumes "finite S"
```
```   562   assumes "\<And>s. s \<in> S \<Longrightarrow> uniform_limit (h s) f g F"
```
```   563   shows "uniform_limit (UNION S h) f g F"
```
```   564   using assms
```
```   565   by induct (auto intro: uniform_limit_on_empty uniform_limit_on_Un)
```
```   566
```
```   567 lemma uniform_limit_on_Union:
```
```   568   assumes "finite I"
```
```   569   assumes "\<And>J. J \<in> I \<Longrightarrow> uniform_limit J f g F"
```
```   570   shows "uniform_limit (Union I) f g F"
```
```   571   by (metis SUP_identity_eq assms uniform_limit_on_UNION)
```
```   572
```
```   573 lemma uniform_limit_on_subset:
```
```   574   "uniform_limit J f g F \<Longrightarrow> I \<subseteq> J \<Longrightarrow> uniform_limit I f g F"
```
```   575   by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_mono)
```
```   576
```
```   577 lemma uniformly_convergent_add:
```
```   578   "uniformly_convergent_on A f \<Longrightarrow> uniformly_convergent_on A g\<Longrightarrow>
```
```   579       uniformly_convergent_on A (\<lambda>k x. f k x + g k x :: 'a :: {real_normed_algebra})"
```
```   580   unfolding uniformly_convergent_on_def by (blast dest: uniform_limit_add)
```
```   581
```
```   582 lemma uniformly_convergent_minus:
```
```   583   "uniformly_convergent_on A f \<Longrightarrow> uniformly_convergent_on A g\<Longrightarrow>
```
```   584       uniformly_convergent_on A (\<lambda>k x. f k x - g k x :: 'a :: {real_normed_algebra})"
```
```   585   unfolding uniformly_convergent_on_def by (blast dest: uniform_limit_minus)
```
```   586
```
```   587 lemma uniformly_convergent_mult:
```
```   588   "uniformly_convergent_on A f \<Longrightarrow>
```
```   589       uniformly_convergent_on A (\<lambda>k x. c * f k x :: 'a :: {real_normed_algebra})"
```
```   590   unfolding uniformly_convergent_on_def
```
```   591   by (blast dest: bounded_linear_uniform_limit_intros(13))
```
```   592
```
```   593 subsection\<open>Power series and uniform convergence\<close>
```
```   594
```
```   595 proposition powser_uniformly_convergent:
```
```   596   fixes a :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
```
```   597   assumes "r < conv_radius a"
```
```   598   shows "uniformly_convergent_on (cball \<xi> r) (\<lambda>n x. \<Sum>i<n. a i * (x - \<xi>) ^ i)"
```
```   599 proof (cases "0 \<le> r")
```
```   600   case True
```
```   601   then have *: "summable (\<lambda>n. norm (a n) * r ^ n)"
```
```   602     using abs_summable_in_conv_radius [of "of_real r" a] assms
```
```   603     by (simp add: norm_mult norm_power)
```
```   604   show ?thesis
```
```   605     by (simp add: weierstrass_m_test'_ev [OF _ *] norm_mult norm_power
```
```   606               mult_left_mono power_mono dist_norm norm_minus_commute)
```
```   607 next
```
```   608   case False then show ?thesis by (simp add: not_le)
```
```   609 qed
```
```   610
```
```   611 lemma powser_uniform_limit:
```
```   612   fixes a :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
```
```   613   assumes "r < conv_radius a"
```
```   614   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"
```
```   615 using powser_uniformly_convergent [OF assms]
```
```   616 by (simp add: Uniform_Limit.uniformly_convergent_uniform_limit_iff Series.suminf_eq_lim)
```
```   617
```
```   618 lemma powser_continuous_suminf:
```
```   619   fixes a :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
```
```   620   assumes "r < conv_radius a"
```
```   621   shows "continuous_on (cball \<xi> r) (\<lambda>x. suminf (\<lambda>i. a i * (x - \<xi>) ^ i))"
```
```   622 apply (rule uniform_limit_theorem [OF _ powser_uniform_limit])
```
```   623 apply (rule eventuallyI continuous_intros assms)+
```
```   624 apply (simp add:)
```
```   625 done
```
```   626
```
```   627 lemma powser_continuous_sums:
```
```   628   fixes a :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
```
```   629   assumes r: "r < conv_radius a"
```
```   630       and sm: "\<And>x. x \<in> cball \<xi> r \<Longrightarrow> (\<lambda>n. a n * (x - \<xi>) ^ n) sums (f x)"
```
```   631   shows "continuous_on (cball \<xi> r) f"
```
```   632 apply (rule continuous_on_cong [THEN iffD1, OF refl _ powser_continuous_suminf [OF r]])
```
```   633 using sm sums_unique by fastforce
```
```   634
```
```   635 end
```
```   636
```