Quelle Uniform_Limit.thy Sprache: Isabelle

(*  Title:      HOL/Analysis/Uniform_Limit.thy
    Author:     Christoph Traut, TU München
    Author:     Fabian Immler, TU München
*)

section \<open>Uniform Limit and Uniform Convergence\<close>

theory Uniform_Limit
imports Connected Summation_Tests Infinite_Sum
begin

subsection \<open>Definition\<close>

definition\<^marker>\<open>tag important\<close> uniformly_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> ('a \<Rightarrow> 'b) filter"
  where "uniformly_on S l = (INF e\{0 <..}. principal {f. \x\S. dist (f x) (l x) < e})"

abbreviation\<^marker>\<open>tag important\<close>
  "uniform_limit S f l \ filterlim f (uniformly_on S l)"

definition uniformly_convergent_on where
  "uniformly_convergent_on X f \ (\l. uniform_limit X f l sequentially)"

definition uniformly_Cauchy_on where
  "uniformly_Cauchy_on X f \ (\e>0. \M. \x\X. \(m::nat)\M. \n\M. dist (f m x) (f n x) < e)"

proposition uniform_limit_iff:
  "uniform_limit S f l F \ (\e>0. \\<^sub>F n in F. \x\S. dist (f n x) (l x) < e)"
  unfolding filterlim_iff uniformly_on_def
  by (subst eventually_INF_base)
    (fastforce
      simp: eventually_principal uniformly_on_def
      intro: bexI[where x="min a b" for a b]
      elim: eventually_mono)+

lemma uniform_limitD:
  "uniform_limit S f l F \ e > 0 \ \\<^sub>F n in F. \x\S. dist (f n x) (l x) < e"
  by (simp add: uniform_limit_iff)

lemma uniform_limitI:
  "(\e. e > 0 \ \\<^sub>F n in F. \x\S. dist (f n x) (l x) < e) \ uniform_limit S f l F"
  by (simp add: uniform_limit_iff)

lemma uniform_limit_on_subset:
  "uniform_limit J f g F \ I \ J \ uniform_limit I f g F"
  by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_mono)

lemma uniformly_convergent_on_subset:
  assumes "uniformly_convergent_on A f" "B \ A"
  shows   "uniformly_convergent_on B f"
  using assms by (meson uniform_limit_on_subset uniformly_convergent_on_def)

lemma uniform_limit_singleton [simp]: "uniform_limit {x} f g F \ ((\n. f n x) \ g x) F"
  by (simp add: uniform_limit_iff tendsto_iff)

lemma uniformly_convergent_on_singleton:
  "uniformly_convergent_on {x} f \ convergent (\n. f n x)"
  by (auto simp: uniformly_convergent_on_def convergent_def)

lemma uniform_limit_sequentially_iff:
  "uniform_limit S f l sequentially \ (\e>0. \N. \n\N. \x \ S. dist (f n x) (l x) < e)"
  unfolding uniform_limit_iff eventually_sequentially ..

lemma uniform_limit_at_iff:
  "uniform_limit S f l (at x) \
    (\<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))"
  unfolding uniform_limit_iff eventually_at by simp

lemma uniform_limit_at_le_iff:
  "uniform_limit S f l (at x) \
    (\<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))"
  unfolding uniform_limit_iff eventually_at
  by (fastforce dest: spec[where x = "e / 2" for e])

lemma uniform_limit_compose:
  assumes ul: "uniform_limit X g l F"
    and cont: "uniformly_continuous_on U f"
    and g: "\\<^sub>F n in F. g n ` X \ U" and l: "l ` X \ U"
  shows "uniform_limit X (\a b. f (g a b)) (f \ l) F"
proof (rule uniform_limitI)
  fix \<epsilon>::real
  assume "0 < \"
  then obtain \<delta> where "\<delta> > 0" and \<delta>: "\<And>u v. \<lbrakk>u\<in>U; v\<in>U; dist u v < \<delta>\<rbrakk> \<Longrightarrow> dist (f u) (f v) < \<epsilon>"
    by (metis cont uniformly_continuous_on_def)
  show "\\<^sub>F n in F. \x\X. dist (f (g n x)) ((f \ l) x) < \"
    using uniform_limitD [OF ul \<open>\<delta>>0\<close>] g unfolding o_def
    by eventually_elim (use \<delta> l in blast)
qed

lemma uniform_limit_compose':
  assumes "uniform_limit A f g F" and "h \ B \ A"
  shows   "uniform_limit B (\n x. f n (h x)) (\x. g (h x)) F"
  unfolding uniform_limit_iff
proof (intro strip)
  fix e :: real
  assume e: "e > 0"
  with assms(1) have "\\<^sub>F n in F. \x\A. dist (f n x) (g x) < e"
    by (auto simp: uniform_limit_iff)
  thus "\\<^sub>F n in F. \x\B. dist (f n (h x)) (g (h x)) < e"
    by eventually_elim (use assms(2) in blast)
qed

lemma metric_uniform_limit_imp_uniform_limit:
  assumes f: "uniform_limit S f a F"
  assumes le: "eventually (\x. \y\S. dist (g x y) (b y) \ dist (f x y) (a y)) F"
  shows "uniform_limit S g b F"
proof (rule uniform_limitI)
  fix e :: real
  assume "0 < e"
  from uniform_limitD[OF f this] le
  show "\\<^sub>F x in F. \y\S. dist (g x y) (b y) < e"
    by eventually_elim force
qed

subsection \<open>Exchange limits\<close>
proposition swap_uniform_limit':
  assumes f: "\\<^sub>F n in F. (f n \ g n) G"
  assumes g: "(g \ l) F"
  assumes uc: "uniform_limit S f h F"
  assumes ev: "\\<^sub>F x in G. x \ S"
  assumes "\trivial_limit F"
  shows "(h \ l) G"
proof (rule tendstoI)
  fix e :: real
  define e' where "e' = e/3"
  assume "0 < e"
  then have "0 < e'" by (simp add: e'_def)
  from uniform_limitD[OF uc \<open>0 < e'\<close>]
  have "\\<^sub>F n in F. \x\S. dist (h x) (f n x) < e'"
    by (simp add: dist_commute)
  moreover
  from f
  have "\\<^sub>F n in F. \\<^sub>F x in G. dist (g n) (f n x) < e'"
    by eventually_elim (auto dest!: tendstoD[OF _ \<open>0 < e'\<close>] simp: dist_commute)
  moreover
  from tendstoD[OF g \<open>0 < e'\<close>] have "\<forall>\<^sub>F x in F. dist l (g x) < e'"
    by (simp add: dist_commute)
  ultimately
  have "\\<^sub>F _ in F. \\<^sub>F x in G. dist (h x) l < e"
  proof eventually_elim
    case (elim n)
    note fh = elim(1)
    note gl = elim(3)
    show ?case
      using elim(2) ev
    proof eventually_elim
      case (elim x)
      from fh[rule_format, OF \<open>x \<in> S\<close>] elim(1)
      have "dist (h x) (g n) < e' + e'"
        by (rule dist_triangle_lt[OF add_strict_mono])
      from dist_triangle_lt[OF add_strict_mono, OF this gl]
      show ?case by (simp add: e'_def)
    qed
  qed
  thus "\\<^sub>F x in G. dist (h x) l < e"
    using eventually_happens by (metis \<open>\<not>trivial_limit F\<close>)
qed

corollary swap_uniform_limit:
  assumes "\\<^sub>F n in F. (f n \ g n) (at x within S)"
  assumes "(g \ l) F" "uniform_limit S f h F" "\trivial_limit F"
  shows "(h \ l) (at x within S)"
  using swap_uniform_limit' eventually_at_topological assms
  by blast

subsection \<open>Uniform limit theorem\<close>

lemma tendsto_uniform_limitI:
  assumes "uniform_limit S f l F"
  assumes "x \ S"
  shows "((\y. f y x) \ l x) F"
  using assms
  by (auto intro!: tendstoI simp: eventually_mono dest!: uniform_limitD)

theorem uniform_limit_theorem:
  assumes c: "\\<^sub>F n in F. continuous_on A (f n)"
  assumes ul: "uniform_limit A f l F"
  assumes "\ trivial_limit F"
  shows "continuous_on A l"
  unfolding continuous_on_def
proof safe
  fix x assume "x \ A"
  then have "\\<^sub>F n in F. (f n \ f n x) (at x within A)" "((\n. f n x) \ l x) F"
    using c ul
    by (auto simp: continuous_on_def eventually_mono tendsto_uniform_limitI)
  then show "(l \ l x) (at x within A)"
    by (rule swap_uniform_limit) fact+
qed

lemma uniformly_Cauchy_onI:
  assumes "\e. e > 0 \ \M. \x\X. \m\M. \n\M. dist (f m x) (f n x) < e"
  shows   "uniformly_Cauchy_on X f"
  using assms unfolding uniformly_Cauchy_on_def by blast

lemma uniformly_Cauchy_onI':
  assumes "\e. e > 0 \ \M. \x\X. \m\M. \n>m. dist (f m x) (f n x) < e"
  shows   "uniformly_Cauchy_on X f"
proof (rule uniformly_Cauchy_onI)
  fix e :: real assume e: "e > 0"
  from assms[OF this] obtain M
    where M: "\x m n. x \ X \ m \ M \ n > m \ dist (f m x) (f n x) < e" by fast
  {
    fix x m n assume x: "x \ X" and m: "m \ M" and n: "n \ M"
    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"
      by (cases m n rule: linorder_cases) (simp_all add: dist_commute)
  }
  thus "\M. \x\X. \m\M. \n\M. dist (f m x) (f n x) < e" by fast
qed

lemma uniformly_Cauchy_imp_Cauchy:
  "uniformly_Cauchy_on X f \ x \ X \ Cauchy (\n. f n x)"
  unfolding Cauchy_def uniformly_Cauchy_on_def by fast

lemma uniform_limit_cong:
  fixes f g :: "'a \ 'b \ ('c :: metric_space)" and h i :: "'b \ 'c"
  assumes "eventually (\y. \x\X. f y x = g y x) F"
  assumes "\x. x \ X \ h x = i x"
  shows   "uniform_limit X f h F \ uniform_limit X g i F"
proof -
  {
    fix f g :: "'a \ 'b \ 'c" and h i :: "'b \ 'c"
    assume C: "uniform_limit X f h F" and A: "eventually (\y. \x\X. f y x = g y x) F"
       and B: "\x. x \ X \ h x = i x"
    {
      fix e ::real assume "e > 0"
      with C have "eventually (\y. \x\X. dist (f y x) (h x) < e) F"
        unfolding uniform_limit_iff by blast
      with A have "eventually (\y. \x\X. dist (g y x) (i x) < e) F"
        by eventually_elim (insert B, simp_all)
    }
    hence "uniform_limit X g i F" unfolding uniform_limit_iff by blast
  } note A = this
  show ?thesis by (rule iffI) (erule A; insert assms; simp add: eq_commute)+
qed

lemma uniform_limit_cong':
  fixes f g :: "'a \ 'b \ ('c :: metric_space)" and h i :: "'b \ 'c"
  assumes "\y x. x \ X \ f y x = g y x"
  assumes "\x. x \ X \ h x = i x"
  shows   "uniform_limit X f h F \ uniform_limit X g i F"
  using assms by (intro uniform_limit_cong always_eventually) blast+

lemma uniformly_convergent_cong:
  assumes "eventually (\x. \y\A. f x y = g x y) sequentially" "A = B"
  shows "uniformly_convergent_on A f \ uniformly_convergent_on B g"
  unfolding uniformly_convergent_on_def assms(2) [symmetric]
  by (intro iff_exI uniform_limit_cong eventually_mono [OF assms(1)]) auto

lemma uniformly_convergent_on_compose:
  assumes "uniformly_convergent_on A f"
  assumes "filterlim g sequentially sequentially"
  shows   "uniformly_convergent_on A (\n. f (g n))"
proof -
  from assms(1) obtain f' where "uniform_limit A f f' sequentially"
    by (auto simp: uniformly_convergent_on_def)
  hence "uniform_limit A (\n. f (g n)) f' sequentially"
    by (rule filterlim_compose) fact
  thus ?thesis
    by (auto simp: uniformly_convergent_on_def)
qed

lemma uniformly_convergent_uniform_limit_iff:
  "uniformly_convergent_on X f \ uniform_limit X f (\x. lim (\n. f n x)) sequentially"
proof
  assume "uniformly_convergent_on X f"
  then obtain l where l: "uniform_limit X f l sequentially"
    unfolding uniformly_convergent_on_def by blast
  from l have "uniform_limit X f (\x. lim (\n. f n x)) sequentially \
                      uniform_limit X f l sequentially"
    by (intro uniform_limit_cong' limI tendsto_uniform_limitI[of f X l]) simp_all
  also note l
  finally show "uniform_limit X f (\x. lim (\n. f n x)) sequentially" .
qed (auto simp: uniformly_convergent_on_def)

lemma uniformly_convergentI: "uniform_limit X f l sequentially \ uniformly_convergent_on X f"
  unfolding uniformly_convergent_on_def by blast

lemma uniformly_convergent_on_empty [iff]: "uniformly_convergent_on {} f"
  by (simp add: uniformly_convergent_on_def uniform_limit_sequentially_iff)

lemma uniformly_convergent_on_const [simp,intro]:
  "uniformly_convergent_on A (\_. c)"
  by (auto simp: uniformly_convergent_on_def uniform_limit_iff intro!: exI[of _ c])

text\<open>Cauchy-type criteria for uniform convergence.\<close>

lemma Cauchy_uniformly_convergent:
  fixes f :: "nat \ 'a \ 'b :: complete_space"
  assumes "uniformly_Cauchy_on X f"
  shows   "uniformly_convergent_on X f"
unfolding uniformly_convergent_uniform_limit_iff uniform_limit_iff
proof safe
  let ?f = "\x. lim (\n. f n x)"
  fix e :: real assume e: "e > 0"
  hence "e/2 > 0" by simp
  with assms obtain N where N: "\x m n. x \ X \ m \ N \ n \ N \ dist (f m x) (f n x) < e/2"
    unfolding uniformly_Cauchy_on_def by fast
  show "eventually (\n. \x\X. dist (f n x) (?f x) < e) sequentially"
    using eventually_ge_at_top[of N]
  proof eventually_elim
    fix n assume n: "n \ N"
    show "\x\X. dist (f n x) (?f x) < e"
    proof
      fix x assume x: "x \ X"
      with assms have "(\n. f n x) \ ?f x"
        by (auto dest!: Cauchy_convergent uniformly_Cauchy_imp_Cauchy simp: convergent_LIMSEQ_iff)
      with \<open>e/2 > 0\<close> have "eventually (\<lambda>m. m \<ge> N \<and> dist (f m x) (?f x) < e/2) sequentially"
        by (intro tendstoD eventually_conj eventually_ge_at_top)
      then obtain m where m: "m \ N" "dist (f m x) (?f x) < e/2"
        unfolding eventually_at_top_linorder by blast
      have "dist (f n x) (?f x) \ dist (f n x) (f m x) + dist (f m x) (?f x)"
          by (rule dist_triangle)
      also from x n have "... < e/2 + e/2" by (intro add_strict_mono N m)
      finally show "dist (f n x) (?f x) < e" by simp
    qed
  qed
qed

lemma uniformly_convergent_Cauchy:
  assumes "uniformly_convergent_on X f"
  shows "uniformly_Cauchy_on X f"
proof (rule uniformly_Cauchy_onI)
  fix e::real assume "e > 0"
  then have "0 < e / 2" by simp
  with assms[unfolded uniformly_convergent_on_def uniform_limit_sequentially_iff]
  obtain l N where l:"x \ X \ n \ N \ dist (f n x) (l x) < e / 2" for n x
    by metis
  from l l have "x \ X \ n \ N \ m \ N \ dist (f n x) (f m x) < e" for n m x
    by (rule dist_triangle_half_l)
  then show "\M. \x\X. \m\M. \n\M. dist (f m x) (f n x) < e" by blast
qed

lemma uniformly_convergent_eq_Cauchy:
  "uniformly_convergent_on X f = uniformly_Cauchy_on X f" for f::"nat \ 'b \ 'a::complete_space"
  using Cauchy_uniformly_convergent uniformly_convergent_Cauchy by blast

lemma uniformly_convergent_eq_cauchy:
  fixes s::"nat \ 'b \ 'a::complete_space"
  shows
    "(\l. \e>0. \N. \n x. N \ n \ P x \ dist(s n x)(l x) < e) \
      (\<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)"
proof -
  have *: "(\n\N. \x. Q x \ R n x) \ (\n x. N \ n \ Q x \ R n x)"
    "(\x. Q x \ (\m\N. \n\N. S n m x)) \ (\m n x. N \ m \ N \ n \ Q x \ S n m x)"
    for N::nat and Q::"'b \ bool" and R S
    by blast+
  show ?thesis
    using uniformly_convergent_eq_Cauchy[of "Collect P" s]
    unfolding uniformly_convergent_on_def uniformly_Cauchy_on_def uniform_limit_sequentially_iff
    by (simp add: *)
qed

lemma uniformly_cauchy_imp_uniformly_convergent:
  fixes s :: "nat \ 'a \ 'b::complete_space"
  assumes "\e>0.\N. \m (n::nat) x. N \ m \ N \ n \ P x --> dist(s m x)(s n x) < e"
    and "\x. P x --> (\e>0. \N. \n. N \ n \ dist(s n x)(l x) < e)"
  shows "\e>0. \N. \n x. N \ n \ P x \ dist(s n x)(l x) < e"
proof -
  obtain l' where l:"\e>0. \N. \n x. N \ n \ P x \ dist (s n x) (l' x) < e"
    using assms(1) unfolding uniformly_convergent_eq_cauchy[symmetric] by auto
  moreover
  {
    fix x
    assume "P x"
    then have "l x = l' x"
      using tendsto_unique[OF trivial_limit_sequentially, of "\n. s n x" "l x" "l' x"]
      using l and assms(2) unfolding lim_sequentially by blast
  }
  ultimately show ?thesis by auto
qed

lemma uniformly_convergent_on_sum_E:
  fixes \<epsilon>::real and f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_space,real_normed_vector}"
  assumes uconv: "uniformly_convergent_on K (\n z. \k>0"
  obtains N where "\m n z. \N \ m; m \ n; z\K\ \ norm(\k=m.."
proof -
  obtain N where N: "\m n z. \N \ m; N \ n; z\K\ \ dist (\kk"
    using uconv \<open>\<epsilon>>0\<close> unfolding uniformly_Cauchy_on_def uniformly_convergent_eq_Cauchy by meson
  show thesis
  proof
    fix m n z
    assume "N \ m" "m \ n" "z \ K"
    moreover have "(\k = m..kk
      by (metis atLeast0LessThan le0 sum_diff_nat_ivl \<open>m \<le> n\<close>)
    ultimately show "norm(\k = m.."
      using N  by (simp add: dist_norm)
  qed
qed

lemma uniformly_convergent_on_sum_iff:
  fixes f :: "nat \ 'a \ 'b::{complete_space,real_normed_vector}"
  shows "uniformly_convergent_on K (\n z. \k
     \<longleftrightarrow> (\<forall>\<epsilon>>0. \<exists>N. \<forall>m n z. N\<le>m \<longrightarrow> m\<le>n \<longrightarrow> z\<in>K \<longrightarrow> norm (\<Sum>k=m..<n. f k z) < \<epsilon>)" (is "?lhs=?rhs")
proof
  assume R: ?rhs
  show ?lhs
    unfolding uniformly_Cauchy_on_def uniformly_convergent_eq_Cauchy
  proof (intro strip)
    fix \<epsilon>::real
    assume "\>0"
    then obtain N where "\m n z. \N \ m; m \ n; z\K\ \ norm(\k = m.."
      using R by blast
    then have "\x\K. \m\N. \n\m. norm ((\kk"
      by (metis atLeast0LessThan le0 sum_diff_nat_ivl norm_minus_commute)
    then have "\x\K. \m\N. \n\N. norm ((\kk"
      by (metis linorder_le_cases norm_minus_commute)
    then show "\M. \x\K. \m\M. \n\M. dist (\kk"
      by (metis dist_norm)
  qed
qed (metis uniformly_convergent_on_sum_E)

lemma uniform_limit_suminf:
  fixes f:: "nat \ 'a :: topological_space \ 'b::{metric_space, comm_monoid_add}"
  assumes "uniformly_convergent_on X (\n x. \k
  shows "uniform_limit X (\n x. \kx. \k. f k x) sequentially"
proof -
  obtain S where S: "uniform_limit X (\n x. \k
    using assms uniformly_convergent_on_def by blast
  then have "(\k. f k x) = S x" if "x \ X" for x
    using that sums_iff sums_def by (blast intro: tendsto_uniform_limitI [OF S])
  with S show ?thesis
    by (simp cong: uniform_limit_cong')
qed

text \<open>TODO: remove explicit formulations
  @{thm uniformly_convergent_eq_cauchy uniformly_cauchy_imp_uniformly_convergent}?!\<close>

lemma uniformly_convergent_imp_convergent:
  "uniformly_convergent_on X f \ x \ X \ convergent (\n. f n x)"
  unfolding uniformly_convergent_on_def convergent_def
  by (auto dest: tendsto_uniform_limitI)

subsection \<open>Comparison Test\<close>

lemma uniformly_summable_comparison_test:
  fixes f :: "nat \ 'a \ 'b :: banach"
  assumes "uniformly_convergent_on A (\N x. \n
  assumes "\n x. x \ A \ norm (f n x) \ g n x"
  shows   "uniformly_convergent_on A (\N x. \n
proof -
  have "uniformly_Cauchy_on A (\N x. \n
  proof (rule uniformly_Cauchy_onI')
    fix e :: real assume e: "e > 0"
    obtain M where M: "\x m n. x \ A \ m \ M \ n \ M \ dist (\kk
      using assms(1) e unfolding uniformly_convergent_eq_Cauchy uniformly_Cauchy_on_def by metis
    show "\M. \x\A. \m\M. \n>m. dist (\kk
    proof (rule exI[of _ M], safe)
      fix x m n assume xmn: "x \ A" "m \ M" "m < n"
      have nonneg: "g k x \ 0" for k
        by (rule order.trans[OF _ assms(2)]) (use xmn in auto)
      have "dist (\kkk\{..
        using xmn by (subst sum_diff) (auto simp: dist_norm norm_minus_commute)
      also have "{..
        by auto
      also have "norm (\k\{m.. (\k\{m..
        using norm_sum by blast
      also have "\ \ (\k\{m..
        by (intro sum_mono assms xmn)
      also have "\ = \\k\{m.."
        by (subst abs_of_nonneg) (auto simp: nonneg intro!: sum_nonneg)
      also have "{m..
        by auto
      also have "\\k\\. g k x\ = dist (\kk
        using xmn by (subst sum_diff) (auto simp: abs_minus_commute dist_norm)
      also have "\ < e"
        by (rule M) (use xmn in auto)
      finally show "dist (\kk
    qed
  qed
  thus ?thesis
    unfolding uniformly_convergent_eq_Cauchy .
qed

lemma uniform_limit_compose_uniformly_continuous_on:
  fixes f :: "'a :: metric_space \ 'b :: metric_space"
  assumes lim: "uniform_limit A g g' F"
  assumes cont: "uniformly_continuous_on B f"
  assumes ev: "eventually (\x. \y\A. g x y \ B) F" and "closed B"
  shows   "uniform_limit A (\x y. f (g x y)) (\y. f (g' y)) F"
proof (cases "F = bot")
  case [simp]: False
  show ?thesis
    unfolding uniform_limit_iff
  proof safe
    fix e :: real assume e: "e > 0"

    have g'_in_B: "g' y \<in> B" if "y \<in> A" for y
    proof (rule Lim_in_closed_set)
      show "eventually (\x. g x y \ B) F"
        using ev by eventually_elim (use that in auto)
      show "((\x. g x y) \ g' y) F"
        using lim that by (metis tendsto_uniform_limitI)
    qed (use \<open>closed B\<close> in auto)

    obtain d where d: "d > 0" "\x y. x \ B \ y \ B \ dist x y < d \ dist (f x) (f y) < e"
      using e cont unfolding uniformly_continuous_on_def by metis
    from lim have "eventually (\x. \y\A. dist (g x y) (g' y) < d) F"
      unfolding uniform_limit_iff using \<open>d > 0\<close>  by meson
    thus "eventually (\x. \y\A. dist (f (g x y)) (f (g' y)) < e) F"
      using assms(3)
    proof eventually_elim
      case (elim x)
      show "\y\A. dist (f (g x y)) (f (g' y)) < e"
      proof safe
        fix y assume y: "y \ A"
        show "dist (f (g x y)) (f (g' y)) < e"
        proof (rule d)
          show "dist (g x y) (g' y) < d"
            using elim y by blast
        qed (use y elim g'_in_B in auto)
      qed
    qed
  qed
qed (auto simp: filterlim_def)

lemma uniformly_convergent_on_compose_uniformly_continuous_on:
  fixes f :: "'a :: metric_space \ 'b :: metric_space"
  assumes lim: "uniformly_convergent_on A g"
  assumes cont: "uniformly_continuous_on B f"
  assumes ev: "eventually (\x. \y\A. g x y \ B) sequentially" and "closed B"
  shows   "uniformly_convergent_on A (\x y. f (g x y))"
proof -
  from lim obtain g' where g': "uniform_limit A g g' sequentially"
    by (auto simp: uniformly_convergent_on_def)
  thus ?thesis
    using uniform_limit_compose_uniformly_continuous_on[OF g' cont ev \closed B\]
    by (auto simp: uniformly_convergent_on_def)
qed

subsection \<open>Weierstrass M-Test\<close>

proposition Weierstrass_m_test_ev:
fixes f :: "_ \ _ \ _ :: banach"
assumes "eventually (\n. \x\A. norm (f n x) \ M n) sequentially"
assumes "summable M"
shows "uniform_limit A (\n x. \ix. suminf (\i. f i x)) sequentially"
proof (rule uniform_limitI)
  fix e :: real
  assume "0 < e"
  from suminf_exist_split[OF \<open>0 < e\<close> \<open>summable M\<close>]
  have "\\<^sub>F k in sequentially. norm (\i. M (i + k)) < e"
    by (auto simp: eventually_sequentially)
  with eventually_all_ge_at_top[OF assms(1)]
    show "\\<^sub>F n in sequentially. \x\A. dist (\ii. f i x) < e"
  proof eventually_elim
    case (elim k)
    show ?case
    proof safe
      fix x assume "x \ A"
      have "\N. \n\N. norm (f n x) \ M n"
        using assms(1) \<open>x \<in> A\<close> by (force simp: eventually_at_top_linorder)
      hence summable_norm_f: "summable (\n. norm (f n x))"
        by(rule summable_norm_comparison_test[OF _ \<open>summable M\<close>])
      have summable_f: "summable (\n. f n x)"
        using summable_norm_cancel[OF summable_norm_f] .
      have summable_norm_f_plus_k: "summable (\i. norm (f (i + k) x))"
        using summable_ignore_initial_segment[OF summable_norm_f]
        by auto
      have summable_M_plus_k: "summable (\i. M (i + k))"
        using summable_ignore_initial_segment[OF \<open>summable M\<close>]
        by auto

      have "dist (\ii. f i x) = norm ((\i. f i x) - (\i
        using dist_norm dist_commute by (subst dist_commute)
      also have "... = norm (\i. f (i + k) x)"
        using suminf_minus_initial_segment[OF summable_f, where k=k] by simp
      also have "... \ (\i. norm (f (i + k) x))"
        using summable_norm[OF summable_norm_f_plus_k] .
      also have "... \ (\i. M (i + k))"
        by (rule suminf_le[OF _ summable_norm_f_plus_k summable_M_plus_k])
           (insert elim(1) \<open>x \<in> A\<close>, simp)
      finally show "dist (\ii. f i x) < e"
        using elim by auto
    qed
  qed
qed

text\<open>Alternative version, formulated as in HOL Light\<close>
corollary\<^marker>\<open>tag unimportant\<close> series_comparison_uniform:
  fixes f :: "_ \ nat \ _ :: banach"
  assumes g: "summable g" and le: "\n x. N \ n \ x \ A \ norm(f x n) \ g n"
    shows "\l. \e. 0 < e \ (\N. \n x. N \ n \ x \ A \ dist(sum (f x) {..
proof -
  have 1: "\\<^sub>F n in sequentially. \x\A. norm (f x n) \ g n"
    using le eventually_sequentially by auto
  show ?thesis
    apply (rule_tac x="(\x. \i. f x i)" in exI)
    apply (metis (no_types, lifting) eventually_sequentially uniform_limitD [OF Weierstrass_m_test_ev [OF 1 g]])
    done
qed

corollary\<^marker>\<open>tag unimportant\<close> Weierstrass_m_test:
  fixes f :: "_ \ _ \ _ :: banach"
  assumes "\n x. x \ A \ norm (f n x) \ M n"
  assumes "summable M"
  shows "uniform_limit A (\n x. \ix. suminf (\i. f i x)) sequentially"
  using assms by (intro Weierstrass_m_test_ev always_eventually) auto

corollary\<^marker>\<open>tag unimportant\<close> Weierstrass_m_test'_ev:
  fixes f :: "_ \ _ \ _ :: banach"
  assumes "eventually (\n. \x\A. norm (f n x) \ M n) sequentially" "summable M"
  shows   "uniformly_convergent_on A (\n x. \i
  unfolding uniformly_convergent_on_def by (rule exI, rule Weierstrass_m_test_ev[OF assms])

corollary\<^marker>\<open>tag unimportant\<close> Weierstrass_m_test':
  fixes f :: "_ \ _ \ _ :: banach"
  assumes "\n x. x \ A \ norm (f n x) \ M n" "summable M"
  shows   "uniformly_convergent_on A (\n x. \i
  unfolding uniformly_convergent_on_def by (rule exI, rule Weierstrass_m_test[OF assms])

lemma Weierstrass_m_test_general:
  fixes f :: "'a \ 'b \ 'c :: banach"
  fixes M :: "'a \ real"
  assumes norm_le:  "\x y. x \ X \ y \ Y \ norm (f x y) \ M x"
  assumes summable: "M summable_on X"
  shows "uniform_limit Y (\X y. \x\X. f x y) (\y. \\<^sub>\x\X. f x y) (finite_subsets_at_top X)"
proof (rule uniform_limitI)
  fix \<epsilon> :: real
  assume "\ > 0"
  define S where "S = (\y. \\<^sub>\x\X. f x y)"
  have S: "((\x. f x y) has_sum S y) X" if y: "y \ Y" for y
    unfolding S_def
  proof (rule has_sum_infsum)
    have "(\x. norm (f x y)) summable_on X"
      by (rule abs_summable_on_comparison_test'[OF summable norm_le]) (use y in auto)
    thus "(\x. f x y) summable_on X"
      by (metis abs_summable_summable)
  qed

  define T where "T = (\\<^sub>\x\X. M x)"
  have T: "(M has_sum T) X"
    unfolding T_def by (simp add: local.summable)
  have M_summable: "M summable_on X'" if "X' \ X" for X'
    using local.summable summable_on_subset_banach that by blast

  have f_summable: "(\x. f x y) summable_on X'" if "X' \ X" "y \ Y" for X' y
    using S summable_on_def summable_on_subset_banach that by blast
  have "eventually (\X'. dist (\x\X'. M x) T < \) (finite_subsets_at_top X)"
    using T \<open>\<epsilon> > 0\<close> unfolding T_def has_sum_def tendsto_iff by blast
  moreover have "eventually (\X'. finite X' \ X' \ X) (finite_subsets_at_top X)"
    by (simp add: eventually_finite_subsets_at_top_weakI)
  ultimately show "\\<^sub>F X' in finite_subsets_at_top X. \y\Y. dist (\x\X'. f x y) (\\<^sub>\x\X. f x y) < \"
  proof eventually_elim
    case X': (elim X')
    show "\y\Y. dist (\x\X'. f x y) (\\<^sub>\x\X. f x y) < \"
    proof
      fix y assume y: "y \ Y"
      have 1: "((\x. f x y) has_sum (S y - (\x\X'. f x y))) (X - X')"
        using X' y by (intro has_sum_Diff S has_sum_finite[of X'] f_summable) auto
      have 2: "(M has_sum (T - (\x\X'. M x))) (X - X')"
        using X' y by (intro has_sum_Diff T has_sum_finite[of X'] M_summable) auto
      have "dist (\x\X'. f x y) (\\<^sub>\x\X. f x y) = norm (S y - (\x\X'. f x y))"
        by (simp add: dist_norm norm_minus_commute S_def)
      also have "norm (S y - (\x\X'. f x y)) \ (\\<^sub>\x\X-X'. M x)"
        using 2 y by (intro norm_infsum_le[OF 1 _ norm_le]) (auto simp: infsumI)
      also have "\ = T - (\x\X'. M x)"
        using 2 by (auto simp: infsumI)
      also have "\ < \"
        using X' by (simp add: dist_norm)
      finally show "dist (\x\X'. f x y) (\\<^sub>\x\X. f x y) < \" .
    qed
  qed
qed

lemma Weierstrass_m_test_general':
  fixes f :: "'a \ 'b \ 'c :: banach"
  fixes M :: "'a \ real"
  assumes norm_le:  "\x y. x \ X \ y \ Y \ norm (f x y) \ M x"
  assumes has_sum: "\y. y \ Y \ ((\x. f x y) has_sum S y) X"
  assumes summable: "M summable_on X"
  shows "uniform_limit Y (\X y. \x\X. f x y) S (finite_subsets_at_top X)"
proof -
  have "uniform_limit Y (\X y. \x\X. f x y) (\y. \\<^sub>\x\X. f x y) (finite_subsets_at_top X)"
    using norm_le summable by (rule Weierstrass_m_test_general)
  also have "?this \ ?thesis"
    by (intro uniform_limit_cong refl always_eventually allI ballI)
       (use has_sum in \<open>auto simp: has_sum_iff\<close>)
  finally show ?thesis .
qed

subsection\<^marker>\<open>tag unimportant\<close> \<open>Structural introduction rules\<close>

lemma uniform_limit_eq_rhs: "uniform_limit X f l F \ l = m \ uniform_limit X f m F"
  by simp

named_theorems uniform_limit_intros "introduction rules for uniform_limit"
setup \<open>
  Global_Theory.add_thms_dynamic (\<^binding>\<open>uniform_limit_eq_intros\<close>,
    fn context =>
      Named_Theorems.get (Context.proof_of context) \<^named_theorems>\<open>uniform_limit_intros\<close>
      |> map_filter (try (fn thm => @{thm uniform_limit_eq_rhs} OF [thm])))
\<close>

lemma (in bounded_linear) uniform_limit[uniform_limit_intros]:
  assumes "uniform_limit X g l F"
  shows "uniform_limit X (\a b. f (g a b)) (\a. f (l a)) F"
proof (rule uniform_limitI)
  fix e::real
  from pos_bounded obtain K
    where K: "\x y. dist (f x) (f y) \ K * dist x y" "K > 0"
    by (auto simp: ac_simps dist_norm diff[symmetric])
  assume "0 < e" with \<open>K > 0\<close> have "e / K > 0" by simp
  from uniform_limitD[OF assms this]
  show "\\<^sub>F n in F. \x\X. dist (f (g n x)) (f (l x)) < e"
    by eventually_elim (metis le_less_trans mult.commute pos_less_divide_eq K)
qed

lemma (in bounded_linear) uniformly_convergent_on:
  assumes "uniformly_convergent_on A g"
  shows   "uniformly_convergent_on A (\x y. f (g x y))"
proof -
  from assms obtain l where "uniform_limit A g l sequentially"
    unfolding uniformly_convergent_on_def by blast
  hence "uniform_limit A (\x y. f (g x y)) (\x. f (l x)) sequentially"
    by (rule uniform_limit)
  thus ?thesis unfolding uniformly_convergent_on_def by blast
qed

lemmas bounded_linear_uniform_limit_intros[uniform_limit_intros] =
  bounded_linear.uniform_limit[OF bounded_linear_Im]
  bounded_linear.uniform_limit[OF bounded_linear_Re]
  bounded_linear.uniform_limit[OF bounded_linear_cnj]
  bounded_linear.uniform_limit[OF bounded_linear_fst]
  bounded_linear.uniform_limit[OF bounded_linear_snd]
  bounded_linear.uniform_limit[OF bounded_linear_zero]
  bounded_linear.uniform_limit[OF bounded_linear_of_real]
  bounded_linear.uniform_limit[OF bounded_linear_inner_left]
  bounded_linear.uniform_limit[OF bounded_linear_inner_right]
  bounded_linear.uniform_limit[OF bounded_linear_divide]
  bounded_linear.uniform_limit[OF bounded_linear_scaleR_right]
  bounded_linear.uniform_limit[OF bounded_linear_mult_left]
  bounded_linear.uniform_limit[OF bounded_linear_mult_right]
  bounded_linear.uniform_limit[OF bounded_linear_scaleR_left]

lemmas uniform_limit_uminus[uniform_limit_intros] =
  bounded_linear.uniform_limit[OF bounded_linear_minus[OF bounded_linear_ident]]

lemma uniform_limit_const[uniform_limit_intros]: "uniform_limit S (\x. c) c f"
  by (auto intro!: uniform_limitI)

lemma uniform_limit_add[uniform_limit_intros]:
  fixes f g::"'a \ 'b \ 'c::real_normed_vector"
  assumes "uniform_limit X f l F"
  assumes "uniform_limit X g m F"
  shows "uniform_limit X (\a b. f a b + g a b) (\a. l a + m a) F"
proof (rule uniform_limitI)
  fix e::real
  assume "0 < e"
  hence "0 < e / 2" by simp
  from
    uniform_limitD[OF assms(1) this]
    uniform_limitD[OF assms(2) this]
  show "\\<^sub>F n in F. \x\X. dist (f n x + g n x) (l x + m x) < e"
    by eventually_elim (simp add: dist_triangle_add_half)
qed

lemma uniform_limit_minus[uniform_limit_intros]:
  fixes f g::"'a \ 'b \ 'c::real_normed_vector"
  assumes "uniform_limit X f l F"
  assumes "uniform_limit X g m F"
  shows "uniform_limit X (\a b. f a b - g a b) (\a. l a - m a) F"
  unfolding diff_conv_add_uminus
  by (rule uniform_limit_intros assms)+

lemma uniform_limit_norm[uniform_limit_intros]:
  assumes "uniform_limit S g l f"
  shows "uniform_limit S (\x y. norm (g x y)) (\x. norm (l x)) f"
  using assms
  apply (rule metric_uniform_limit_imp_uniform_limit)
  apply (rule eventuallyI)
  by (metis dist_norm norm_triangle_ineq3 real_norm_def)

lemma (in bounded_bilinear) bounded_uniform_limit[uniform_limit_intros]:
  assumes "uniform_limit X f l F"
  assumes "uniform_limit X g m F"
  assumes "bounded (m ` X)"
  assumes "bounded (l ` X)"
  shows "uniform_limit X (\a b. prod (f a b) (g a b)) (\a. prod (l a) (m a)) F"
proof (rule uniform_limitI)
  fix e::real
  from pos_bounded obtain K where K:
    "0 < K" "\a b. norm (prod a b) \ norm a * norm b * K"
    by auto
  hence "sqrt (K*4) > 0" by simp

  from assms obtain Km Kl
  where Km: "Km > 0" "\x. x \ X \ norm (m x) \ Km"
    and Kl: "Kl > 0" "\x. x \ X \ norm (l x) \ Kl"
    by (auto simp: bounded_pos)
  hence "K * Km * 4 > 0" "K * Kl * 4 > 0"
    using \<open>K > 0\<close>
    by simp_all
  assume "0 < e"

  hence "sqrt e > 0" by simp
  from uniform_limitD[OF assms(1) divide_pos_pos[OF this \<open>sqrt (K*4) > 0\<close>]]
    uniform_limitD[OF assms(2) divide_pos_pos[OF this \<open>sqrt (K*4) > 0\<close>]]
    uniform_limitD[OF assms(1) divide_pos_pos[OF \<open>e > 0\<close> \<open>K * Km * 4 > 0\<close>]]
    uniform_limitD[OF assms(2) divide_pos_pos[OF \<open>e > 0\<close> \<open>K * Kl * 4 > 0\<close>]]
  show "\\<^sub>F n in F. \x\X. dist (prod (f n x) (g n x)) (prod (l x) (m x)) < e"
  proof eventually_elim
    case (elim n)
    show ?case
    proof safe
      fix x assume "x \ X"
      have "dist (prod (f n x) (g n x)) (prod (l x) (m x)) \
        norm (prod (f n x - l x) (g n x - m x)) +
        norm (prod (f n x - l x) (m x)) +
        norm (prod (l x) (g n x - m x))"
        by (auto simp: dist_norm prod_diff_prod intro: order_trans norm_triangle_ineq add_mono)
      also note K(2)[of "f n x - l x" "g n x - m x"]
      also from elim(1)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
      have "norm (f n x - l x) \ sqrt e / sqrt (K * 4)"
        by simp
      also from elim(2)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
      have "norm (g n x - m x) \ sqrt e / sqrt (K * 4)"
        by simp
      also have "sqrt e / sqrt (K * 4) * (sqrt e / sqrt (K * 4)) * K = e / 4"
        using \<open>K > 0\<close> \<open>e > 0\<close> by auto
      also note K(2)[of "f n x - l x" "m x"]
      also note K(2)[of "l x" "g n x - m x"]
      also from elim(3)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
      have "norm (f n x - l x) \ e / (K * Km * 4)"
        by simp
      also from elim(4)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
      have "norm (g n x - m x) \ e / (K * Kl * 4)"
        by simp
      also note Kl(2)[OF \<open>_ \<in> X\<close>]
      also note Km(2)[OF \<open>_ \<in> X\<close>]
      also have "e / (K * Km * 4) * Km * K = e / 4"
        using \<open>K > 0\<close> \<open>Km > 0\<close> by simp
      also have " Kl * (e / (K * Kl * 4)) * K = e / 4"
        using \<open>K > 0\<close> \<open>Kl > 0\<close> by simp
      also have "e / 4 + e / 4 + e / 4 < e" using \<open>e > 0\<close> by simp
      finally show "dist (prod (f n x) (g n x)) (prod (l x) (m x)) < e"
        using \<open>K > 0\<close> \<open>Kl > 0\<close> \<open>Km > 0\<close> \<open>e > 0\<close>
        by (simp add: algebra_simps mult_right_mono divide_right_mono)
    qed
  qed
qed

lemmas bounded_bilinear_bounded_uniform_limit_intros[uniform_limit_intros] =
  bounded_bilinear.bounded_uniform_limit[OF Inner_Product.bounded_bilinear_inner]
  bounded_bilinear.bounded_uniform_limit[OF Real_Vector_Spaces.bounded_bilinear_mult]
  bounded_bilinear.bounded_uniform_limit[OF Real_Vector_Spaces.bounded_bilinear_scaleR]

lemma uniform_lim_mult:
  fixes f :: "'a \ 'b \ 'c::real_normed_algebra"
  assumes f: "uniform_limit S f l F"
      and g: "uniform_limit S g m F"
      and l: "bounded (l ` S)"
      and m: "bounded (m ` S)"
    shows "uniform_limit S (\a b. f a b * g a b) (\a. l a * m a) F"
  by (intro bounded_bilinear_bounded_uniform_limit_intros assms)

lemma uniform_lim_inverse:
  fixes f :: "'a \ 'b \ 'c::real_normed_field"
  assumes f: "uniform_limit S f l F"
      and b: "\x. x \ S \ b \ norm(l x)"
      and "b > 0"
    shows "uniform_limit S (\x y. inverse (f x y)) (inverse \ l) F"
proof (rule uniform_limitI)
  fix e::real
  assume "e > 0"
  have lte: "dist (inverse (f x y)) ((inverse \ l) y) < e"
           if "b/2 \ norm (f x y)" "norm (f x y - l y) < e * b\<^sup>2 / 2" "y \ S"
           for x y
  proof -
    have [simp]: "l y \ 0" "f x y \ 0"
      using \<open>b > 0\<close> that b [OF \<open>y \<in> S\<close>] by fastforce+
    have "norm (l y - f x y) < e * b\<^sup>2 / 2"
      by (metis norm_minus_commute that(2))
    also have "... \ e * (norm (f x y) * norm (l y))"
      using \<open>e > 0\<close> that b [OF \<open>y \<in> S\<close>] apply (simp add: power2_eq_square)
      by (metis \<open>b > 0\<close> less_eq_real_def mult.left_commute mult_mono')
    finally show ?thesis
      by (auto simp: dist_norm field_split_simps norm_mult norm_divide)
  qed
  have "\\<^sub>F n in F. \x\S. dist (f n x) (l x) < b/2"
    using uniform_limitD [OF f, of "b/2"] by (simp add: \<open>b > 0\<close>)
  then have "\\<^sub>F x in F. \y\S. b/2 \ norm (f x y)"
    apply (rule eventually_mono)
    using b apply (simp only: dist_norm)
    by (metis (no_types, opaque_lifting) diff_zero dist_commute dist_norm norm_triangle_half_l not_less)
  then have "\\<^sub>F x in F. \y\S. b/2 \ norm (f x y) \ norm (f x y - l y) < e * b\<^sup>2 / 2"
    apply (simp only: ball_conj_distrib dist_norm [symmetric])
    apply (rule eventually_conj, assumption)
      apply (rule uniform_limitD [OF f, of "e * b ^ 2 / 2"])
    using \<open>b > 0\<close> \<open>e > 0\<close> by auto
  then show "\\<^sub>F x in F. \y\S. dist (inverse (f x y)) ((inverse \ l) y) < e"
    using lte by (force intro: eventually_mono)
qed

lemma uniform_lim_divide:
  fixes f :: "'a \ 'b \ 'c::real_normed_field"
  assumes f: "uniform_limit S f l F"
      and g: "uniform_limit S g m F"
      and l: "bounded (l ` S)"
      and b: "\x. x \ S \ b \ norm(m x)"
      and "b > 0"
    shows "uniform_limit S (\a b. f a b / g a b) (\a. l a / m a) F"
proof -
  have m: "bounded ((inverse \ m) ` S)"
    using b \<open>b > 0\<close>
    apply (simp add: bounded_iff)
    by (metis le_imp_inverse_le norm_inverse)
  have "uniform_limit S (\a b. f a b * inverse (g a b))
         (\<lambda>a. l a * (inverse \<circ> m) a) F"
    by (rule uniform_lim_mult [OF f uniform_lim_inverse [OF g b \<open>b > 0\<close>] l m])
  then show ?thesis
    by (simp add: field_class.field_divide_inverse)
qed

lemma uniform_limit_null_comparison:
  assumes "\\<^sub>F x in F. \a\S. norm (f x a) \ g x a"
  assumes "uniform_limit S g (\_. 0) F"
  shows "uniform_limit S f (\_. 0) F"
  using assms(2)
proof (rule metric_uniform_limit_imp_uniform_limit)
  show "\\<^sub>F x in F. \y\S. dist (f x y) 0 \ dist (g x y) 0"
    using assms(1) by (rule eventually_mono) (force simp add: dist_norm)
qed

lemma uniform_limit_on_Un:
  "uniform_limit I f g F \ uniform_limit J f g F \ uniform_limit (I \ J) f g F"
  by (auto intro!: uniform_limitI dest!: uniform_limitD elim: eventually_elim2)

lemma uniform_limit_on_empty [iff]:
  "uniform_limit {} f g F"
  by (auto intro!: uniform_limitI)

lemma uniform_limit_on_UNION:
  assumes "finite S"
  assumes "\s. s \ S \ uniform_limit (h s) f g F"
  shows "uniform_limit (\(h ` S)) f g F"
  using assms
  by induct (auto intro: uniform_limit_on_empty uniform_limit_on_Un)

lemma uniform_limit_on_Union:
  assumes "finite I"
  assumes "\J. J \ I \ uniform_limit J f g F"
  shows "uniform_limit (Union I) f g F"
  by (metis SUP_identity_eq assms uniform_limit_on_UNION)

lemma uniform_limit_bounded:
  fixes f::"'i \ 'a::topological_space \ 'b::metric_space"
  assumes l: "uniform_limit S f l F"
  assumes bnd: "\\<^sub>F i in F. bounded (f i ` S)"
  assumes "F \ bot"
  shows "bounded (l ` S)"
proof -
  from l have "\\<^sub>F n in F. \x\S. dist (l x) (f n x) < 1"
    by (auto simp: uniform_limit_iff dist_commute dest!: spec[where x=1])
  with bnd
  have "\\<^sub>F n in F. \M. \x\S. dist undefined (l x) \ M + 1"
    by eventually_elim
      (auto intro!: order_trans[OF dist_triangle2 add_mono] intro: less_imp_le
        simp: bounded_any_center[where a=undefined])
  then show ?thesis using assms
    by (auto simp: bounded_any_center[where a=undefined] dest!: eventually_happens)
qed

lemma uniformly_convergent_add:
  "uniformly_convergent_on A f \ uniformly_convergent_on A g\
      uniformly_convergent_on A (\<lambda>k x. f k x + g k x :: 'a :: {real_normed_algebra})"
  unfolding uniformly_convergent_on_def by (blast dest: uniform_limit_add)

lemma uniformly_convergent_minus:
  "uniformly_convergent_on A f \ uniformly_convergent_on A g\
      uniformly_convergent_on A (\<lambda>k x. f k x - g k x :: 'a :: {real_normed_algebra})"
  unfolding uniformly_convergent_on_def by (blast dest: uniform_limit_minus)

lemma uniformly_convergent_mult:
  "uniformly_convergent_on A f \
      uniformly_convergent_on A (\<lambda>k x. c * f k x :: 'a :: {real_normed_algebra})"
  unfolding uniformly_convergent_on_def
  by (blast dest: bounded_linear_uniform_limit_intros(13))

subsection\<open>Power series and uniform convergence\<close>

proposition powser_uniformly_convergent:
  fixes a :: "nat \ 'a::{real_normed_div_algebra,banach}"
  assumes "r < conv_radius a"
  shows "uniformly_convergent_on (cball \ r) (\n x. \i) ^ i)"
proof (cases "0 \ r")
  case True
  then have *: "summable (\n. norm (a n) * r ^ n)"
    using abs_summable_in_conv_radius [of "of_real r" a] assms
    by (simp add: norm_mult norm_power)
  show ?thesis
    by (simp add: Weierstrass_m_test'_ev [OF _ *] norm_mult norm_power
              mult_left_mono power_mono dist_norm norm_minus_commute)
next
  case False then show ?thesis by (simp add: not_le)
qed

lemma powser_uniform_limit:
  fixes a :: "nat \ 'a::{real_normed_div_algebra,banach}"
  assumes "r < conv_radius a"
  shows "uniform_limit (cball \ r) (\n x. \i) ^ i) (\x. suminf (\i. a i * (x - \) ^ i)) sequentially"
  using powser_uniformly_convergent [OF assms]
  by (simp add: Uniform_Limit.uniformly_convergent_uniform_limit_iff Series.suminf_eq_lim)

lemma powser_continuous_suminf:
  fixes a :: "nat \ 'a::{real_normed_div_algebra,banach}"
  assumes "r < conv_radius a"
  shows "continuous_on (cball \ r) (\x. suminf (\i. a i * (x - \) ^ i))"
  apply (rule uniform_limit_theorem [OF _ powser_uniform_limit])
    apply (rule eventuallyI continuous_intros assms)+
  apply auto
  done

lemma powser_continuous_sums:
  fixes a :: "nat \ 'a::{real_normed_div_algebra,banach}"
  assumes r: "r < conv_radius a"
    and sm: "\x. x \ cball \ r \ (\n. a n * (x - \) ^ n) sums (f x)"
  shows "continuous_on (cball \ r) f"
  apply (rule continuous_on_cong [THEN iffD1, OF refl _ powser_continuous_suminf [OF r]])
  using sm sums_unique by fastforce

lemmas uniform_limit_subset_union = uniform_limit_on_subset[OF uniform_limit_on_Union]

subsection \<open>Tannery's Theorem\<close>

text \<open>
  Tannery's Theorem proves that, under certain boundedness conditions:
  \[ \lim_{x\to\bar x} \sum_{k=0}^\infty f(k,n) = \sum_{k=0}^\infty \lim_{x\to\bar x} f(k,n) \]
\<close>
lemma tannerys_theorem:
  fixes a :: "nat \ _ \ 'a :: {real_normed_algebra, banach}"
  assumes limit: "\k. ((\n. a k n) \ b k) F"
  assumes bound: "eventually (\(k,n). norm (a k n) \ M k) (at_top \\<^sub>F F)"
  assumes "summable M"
  assumes [simp]: "F \ bot"
  shows   "eventually (\n. summable (\k. norm (a k n))) F \
           summable (\<lambda>n. norm (b n)) \<and>
           ((\<lambda>n. suminf (\<lambda>k. a k n)) \<longlongrightarrow> suminf b) F"
proof (intro conjI allI)
  show "eventually (\n. summable (\k. norm (a k n))) F"
  proof -
    have "eventually (\n. eventually (\k. norm (a k n) \ M k) at_top) F"
      using eventually_eventually_prod_filter2[OF bound] by simp
    thus ?thesis
    proof eventually_elim
      case (elim n)
      show "summable (\k. norm (a k n))"
      proof (rule summable_comparison_test_ev)
        show "eventually (\k. norm (norm (a k n)) \ M k) at_top"
          using elim by auto
      qed fact
    qed
  qed

  have bound': "eventually (\k. norm (b k) \ M k) at_top"
  proof -
    have "eventually (\k. eventually (\n. norm (a k n) \ M k) F) at_top"
      using eventually_eventually_prod_filter1[OF bound] by simp
    thus ?thesis
    proof eventually_elim
      case (elim k)
      show "norm (b k) \ M k"
      proof (rule tendsto_upperbound)
        show "((\n. norm (a k n)) \ norm (b k)) F"
          by (intro tendsto_intros limit)
      qed (use elim in auto)
    qed
  qed
  show "summable (\n. norm (b n))"
    by (rule summable_comparison_test_ev[OF _ \<open>summable M\<close>]) (use bound' in auto)

  from bound obtain Pf Pg where
    *: "eventually Pf at_top" "eventually Pg F" "\k n. Pf k \ Pg n \ norm (a k n) \ M k"
    unfolding eventually_prod_filter by auto

  show "((\n. \k. a k n) \ (\k. b k)) F"
  proof (rule swap_uniform_limit')
    show "(\K. (\k (\k. b k)"
      using \<open>summable (\<lambda>n. norm (b n))\<close>
      by (intro summable_LIMSEQ) (auto dest: summable_norm_cancel)
    show "\\<^sub>F K in sequentially. ((\n. \k (\k
      by (intro tendsto_intros always_eventually allI limit)
    show "\\<^sub>F x in F. x \ {n. Pg n}"
      using *(2) by simp
    show "uniform_limit {n. Pg n} (\K n. \kn. \k. a k n) sequentially"
    proof (rule Weierstrass_m_test_ev)
      show "\\<^sub>F k in at_top. \n\{n. Pg n}. norm (a k n) \ M k"
        using *(1) by eventually_elim (use *(3) in auto)
      show "summable M"
        by fact
    qed
  qed auto
qed

end

quality95%

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.