Theory Uniform_Limit

theory Uniform_Limit
imports Topology_Euclidean_Space Summation
(*  Title:      HOL/Multivariate_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 Topology_Euclidean_Space Summation
begin

definition 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
  "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)"
  
lemma uniform_limit_iff:
  "uniform_limit S f l F ⟷ (∀e>0. ∀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 ⟹ ∀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 ⟹ ∀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_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 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 "∀F x in F. ∀y∈S. dist (g x y) (b y) < e"
    by eventually_elim force
qed

lemma swap_uniform_limit:
  assumes f: "∀F n in F. (f n ⤏ g n) (at x within S)"
  assumes g: "(g ⤏ l) F"
  assumes uc: "uniform_limit S f h F"
  assumes "¬trivial_limit F"
  shows "(h ⤏ l) (at x within S)"
proof (rule tendstoI)
  fix e :: real
  def e'  "e/3"
  assume "0 < e"
  then have "0 < e'" by (simp add: e'_def)
  from uniform_limitD[OF uc ‹0 < e'›]
  have "∀F n in F. ∀x∈S. dist (h x) (f n x) < e'"
    by (simp add: dist_commute)
  moreover
  from f
  have "∀F n in F. ∀F x in at x within S. 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 "∀F x in F. dist l (g x) < e'"
    by (simp add: dist_commute)
  ultimately
  have "∀F _ in F. ∀F x in at x within S. dist (h x) l < e"
  proof eventually_elim
    case (elim n)
    note fh = elim(1)
    note gl = elim(3)
    have "∀F x in at x within S. x ∈ S"
      by (auto simp: eventually_at_filter)
    with elim(2)
    show ?case
    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 "∀F x in at x within S. dist (h x) l < e"
    using eventually_happens by (metis ‹¬trivial_limit F›)
qed

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)

lemma uniform_limit_theorem:
  assumes c: "∀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 "∀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_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 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_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)

lemma 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. ∑i<n. f i x) (λx. 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 "∀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 "∀F n in sequentially. ∀x∈A. dist (∑i<n. f i x) (∑i. 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 (∑i<k. f i x) (∑i. f i x) = norm ((∑i. f i x) - (∑i<k. f i x))"
        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 (∑i<k. f i x) (∑i. f i x) < e"
        using elim by auto
    qed
  qed
qed

text‹Alternative version, formulated as in HOL Light›
corollary 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(setsum (f x) {..<n}) (l x) < e)"
proof -
  have 1: "∀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 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. ∑i<n. f i x) (λx. suminf (λi. f i x)) sequentially"
  using assms by (intro weierstrass_m_test_ev always_eventually) auto
    
corollary 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<n. f i x)"
  unfolding uniformly_convergent_on_def by (rule exI, rule weierstrass_m_test_ev[OF assms])

corollary 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<n. f i x)"
  unfolding uniformly_convergent_on_def by (rule exI, rule weierstrass_m_test[OF assms])

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 (@{binding uniform_limit_eq_intros},
    fn context =>
      Named_Theorems.get (Context.proof_of context) @{named_theorems 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 "∀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

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 y. c) (λx. 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 "∀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 "∀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_limit_null_comparison:
  assumes "∀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 "∀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_union:
  "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 (UNION S h) f g F"
  using assms
  by induct (auto intro: uniform_limit_on_empty uniform_limit_on_union)

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_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_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<n. a i * (x - ξ) ^ 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<n. a i * (x - ξ) ^ 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 (simp add:)
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

end