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