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 ‹Uniform Limit and Uniform Convergence›

theory Uniform_Limit
imports Connected Summation_Tests Infinite_Sum
begin


subsection ‹Definition›

definition🍋‹tag important› uniformly_on :: "'a set \ ('a \ 'b::metric_space) \ ('a \ 'b) filter"
  where "uniformly_on S l = (INF e\{0 <..}. principal {f. \x\S. dist (f x) (l x) < e})"

abbreviation🍋‹tag important›
  "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) \
    (∀e>0. ∃d>0. ∀z. 0 < dist z x ∧ dist z x < d ⟶ (∀x∈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) \
    (∀e>0. ∃d>0. ∀z. 0 < dist z x ∧ dist z x < d ⟶ (∀x∈S. dist (f z x) (l x) ≤ 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 ε::real
  assume "0 < \" 
  then obtain δ where "\ > 0" and δ: "\u v. \u\U; v\U; dist u v < \\ \ dist (f u) (f v) < \"
    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 ‹δ>0›] g unfolding o_def
    by eventually_elim (use δ 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 ‹Exchange limits›
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 ‹0 < e'\]
  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 _ ‹0 < e'\] simp: dist_commute)
  moreover
  from tendstoD[OF g ‹0 < e'\] have "\\<^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 ‹x ∈ S›] 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 ‹¬trivial_limit F›)
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 ‹Uniform limit theorem›

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‹Cauchy-type criteria for uniform convergence.›

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 ‹e/2 > 0› have "eventually (\m. m \ N \ 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) \
      (∀e>0. ∃N. ∀m n x. N ≤ m ∧ N ≤ n ∧ P x  ⟶ 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 ε::real and f :: "nat \ 'a \ 'b::{complete_space,real_normed_vector}"
  assumes uconv: "uniformly_convergent_on K (\n z. \k and "\>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 ‹ε>0› 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 ‹m ≤ n›)
    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
     ⟷ (∀ε>0. ∃N. ∀m n z. N≤m ⟶ m≤n ⟶ z∈K ⟶ norm (∑k=m..<n. f k z) < ε)" (is "?lhs=?rhs")
proof
  assume R: ?rhs
  show ?lhs
    unfolding uniformly_Cauchy_on_def uniformly_convergent_eq_Cauchy
  proof (intro strip)
    fix ε::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 ‹TODO: remove explicit formulations
  @{thm uniformly_convergent_eq_cauchy uniformly_cauchy_imp_uniformly_convergent}?!›

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 ‹Comparison Test›

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 ∈ B" if "y ∈ 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 ‹closed B› 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 ‹d > 0›  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 ‹Weierstrass M-Test›

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 ‹0 < e› ‹summable M›]
  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) ‹x ∈ A› by (force simp: eventually_at_top_linorder)
      hence summable_norm_f: "summable (\n. norm (f n x))"
        by(rule summable_norm_comparison_test[OF _ ‹summable M›])
      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 ‹summable M›]
        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) ‹x ∈ A›, simp)
      finally show "dist (\ii. f i x) < e"
        using elim by auto
    qed
  qed
qed

text‹Alternative version, formulated as in HOL Light›
corollary🍋‹tag unimportant› 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🍋‹tag unimportant› 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🍋‹tag unimportant› 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🍋‹tag unimportant› 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 ε :: 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 ‹ε > 0› 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 ‹auto simp: has_sum_iff›)
  finally show ?thesis .
qed


subsection🍋‹tag unimportant› ‹Structural introduction rules›

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 ‹
  Global_Theory.add_thms_dynamic (🍋‹uniform_limit_eq_intros›,
    fn context =>
      Named_Theorems.get (Context.proof_of context) 🍋‹uniform_limit_intros›
      |> map_filter (try (fn thm => @{thm uniform_limit_eq_rhs} OF [thm])))
›

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 ‹K > 0› 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 ‹K > 0›
    by simp_all
  assume "0 < e"

  hence "sqrt e > 0" by simp
  from uniform_limitD[OF assms(1) divide_pos_pos[OF this ‹sqrt (K*4) > 0›]]
    uniform_limitD[OF assms(2) divide_pos_pos[OF this ‹sqrt (K*4) > 0›]]
    uniform_limitD[OF assms(1) divide_pos_pos[OF ‹e > 0› ‹K * Km * 4 > 0›]]
    uniform_limitD[OF assms(2) divide_pos_pos[OF ‹e > 0› ‹K * Kl * 4 > 0›]]
  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 ‹_ ∈ X›, unfolded dist_norm]
      have "norm (f n x - l x) \ sqrt e / sqrt (K * 4)"
        by simp
      also from elim(2)[THEN bspec, OF ‹_ ∈ X›, 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 ‹K > 0› ‹e > 0› 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 ‹_ ∈ X›, unfolded dist_norm]
      have "norm (f n x - l x) \ e / (K * Km * 4)"
        by simp
      also from elim(4)[THEN bspec, OF ‹_ ∈ X›, unfolded dist_norm]
      have "norm (g n x - m x) \ e / (K * Kl * 4)"
        by simp
      also note Kl(2)[OF ‹_ ∈ X›]
      also note Km(2)[OF ‹_ ∈ X›]
      also have "e / (K * Km * 4) * Km * K = e / 4"
        using ‹K > 0› ‹Km > 0› by simp
      also have " Kl * (e / (K * Kl * 4)) * K = e / 4"
        using ‹K > 0› ‹Kl > 0› by simp
      also have "e / 4 + e / 4 + e / 4 < e" using ‹e > 0› by simp
      finally show "dist (prod (f n x) (g n x)) (prod (l x) (m x)) < e"
        using ‹K > 0› ‹Kl > 0› ‹Km > 0› ‹e > 0›
        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 ‹b > 0› that b [OF ‹y ∈ S›] 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 ‹e > 0› that b [OF ‹y ∈ S›] apply (simp add: power2_eq_square)
      by (metis ‹b > 0› 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: ‹b > 0›)
  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 ‹b > 0› ‹e > 0› 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 ‹b > 0›
    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))
         (λa. l a * (inverse ∘ m) a) F"
    by (rule uniform_lim_mult [OF f uniform_lim_inverse [OF g b ‹b > 0›] 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 (λ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 (λ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 (λ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‹Power series and uniform convergence›

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 ‹Tannery's Theorem\

text ‹
  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) \]
›
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 (λn. norm (b n)) ∧
           ((λn. suminf (λk. a k n)) ---> 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 _ ‹summable M›]) (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 ‹summable (λn. norm (b n))›
      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