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