Quelle  Summation_Tests.thy

(*  Title:    HOL/Analysis/Summation_Tests.thy
  Author: Manuel Eberl, TU München
*)

section ‹Radius of Convergence and Summation Tests›

theory Summation_Tests
imports
  Complex_Main
  "HOL-Library.Discrete_Functions"
  "HOL-Library.Extended_Real"
  "HOL-Library.Liminf_Limsup"
  Extended_Real_Limits
begin

text ‹
  The definition of the radius of convergence of a power series,
  various summability tests, lemmas to compute the radius of convergence etc.
 ›

subsection ‹Convergence tests for infinite sums›

subsubsection ‹Root test›

lemma limsup_root_powser:
  fixes f :: "nat ==> 'a :: {banach, real_normed_div_algebra}"
  shows "limsup (λn. ereal (root n (norm (f n * z ^ n)))) =
             limsup (λn. ereal (root n (norm (f n)))) * ereal (norm z)"
proof -
  have A: "(λn. ereal (root n (norm (f n * z ^ n)))) =
              (λn. ereal (root n (norm (f n))) * ereal (norm z))" (is "?g = ?h")
  proof
    fix n show "?g n = ?h n"
    by (cases "n = 0") (simp_all add: norm_mult real_root_mult real_root_pos2 norm_power)
  qed
  show ?thesis by (subst A, subst limsup_ereal_mult_right) simp_all
qed

lemma limsup_root_limit:
  assumes "(λn. ereal (root n (norm (f n)))) <---- l" (is "?g <---- _")
  shows   "limsup (λn. ereal (root n (norm (f n)))) = l"
proof -
  from assms have "convergent ?g" "lim ?g = l"
    unfolding convergent_def by (blast intro: limI)+
  with convergent_limsup_cl show ?thesis by force
qed

lemma limsup_root_limit':
  assumes "(λn. root n (norm (f n))) <---- l"
  shows   "limsup (λn. ereal (root n (norm (f n)))) = ereal l"
  by (intro limsup_root_limit tendsto_ereal assms)

theorem root_test_convergence':
  fixes f :: "nat ==> 'a :: banach"
  defines "l ≡ limsup (λn. ereal (root n (norm (f n))))"
  assumes l: "l < 1"
  shows   "summable f"
proof -
  have "0 = limsup (λn. 0)" by (simp add: Limsup_const)
  also have "... ≤ l" unfolding l_def by (intro Limsup_mono) (simp_all add: real_root_ge_zero)
  finally have "l ≥ 0" by simp
  with l obtain l' where l': "l = ereal l'" by (cases l) simp_all

  define c where "c = (1 - l') / 2"
  from l and ‹l ≥ 0› have c: "l + c > l" "l' + c ≥ 0" "l' + c < 1" unfolding c_def
    by (simp_all add: field_simps l')
  have "∀C>l. eventually (λn. ereal (root n (norm (f n))) < C) sequentially"
    by (subst Limsup_le_iff[symmetric]) (simp add: l_def)
  with c have "eventually (λn. ereal (root n (norm (f n))) < l + ereal c) sequentially" by simp
  with eventually_gt_at_top[of "0::nat"]
    have "eventually (λn. norm (f n) ≤ (l' + c) ^ n) sequentially"
  proof eventually_elim
    fix n :: nat assume n: "n > 0"
    assume "ereal (root n (norm (f n))) < l + ereal c"
    hence "root n (norm (f n)) ≤ l' + c" by (simp add: l')
    with c n have "root n (norm (f n)) ^ n ≤ (l' + c) ^ n"
      by (intro power_mono) (simp_all add: real_root_ge_zero)
    also from n have "root n (norm (f n)) ^ n = norm (f n)" by simp
    finally show "norm (f n) ≤ (l' + c) ^ n" by simp
  qed
  thus ?thesis
    by (rule summable_comparison_test_ev[OF _ summable_geometric]) (simp add: c)
qed

theorem root_test_divergence:
  fixes f :: "nat ==> 'a :: banach"
  defines "l ≡ limsup (λn. ereal (root n (norm (f n))))"
  assumes l: "l > 1"
  shows   "¬summable f"
proof
  assume "summable f"
  hence bounded: "Bseq f" by (simp add: summable_imp_Bseq)

  have "0 = limsup (λn. 0)" by (simp add: Limsup_const)
  also have "... ≤ l" unfolding l_def by (intro Limsup_mono) (simp_all add: real_root_ge_zero)
  finally have l_nonneg: "l ≥ 0" by simp

  define c where "c = (if l = ∞ then 2 else 1 + (real_of_ereal l - 1) / 2)"
  from l l_nonneg consider "l = ∞" | "∃l'. l = ereal l'" by (cases l) simp_all
  hence c: "c > 1 ∧ ereal c < l" by cases (insert l, auto simp: c_def field_simps)

  have unbounded: "¬bdd_above {n. root n (norm (f n)) > c}"
  proof
    assume "bdd_above {n. root n (norm (f n)) > c}"
    then obtain N where "∀n. root n (norm (f n)) > c ⟶ n ≤ N" unfolding bdd_above_def by blast
    hence "∃N. ∀n≥N. root n (norm (f n)) ≤ c"
      by (intro exI[of _ "N + 1"]) (force simp: not_less_eq_eq[symmetric])
    hence "eventually (λn. root n (norm (f n)) ≤ c) sequentially"
      by (auto simp: eventually_at_top_linorder)
    hence "l ≤ c" unfolding l_def by (intro Limsup_bounded) simp_all
    with c show False by auto
  qed

  from bounded obtain K where K: "K > 0" "∧n. norm (f n) ≤ K" using BseqE by blast
  define n where "n = nat ⌈log c K⌉"
  from unbounded have "∃m>n. c < root m (norm (f m))" unfolding bdd_above_def
    by (auto simp: not_le)
  then obtain m where m: "n < m" "c < root m (norm (f m))" by auto
  from c K have "K = c powr log c K" by (simp add: powr_def log_def)
  also from c have "c powr log c K ≤ c powr real n" unfolding n_def
    by (intro powr_mono, linarith, simp)
  finally have "K ≤ c ^ n" using c by (simp add: powr_realpow)
  also from c m have "c ^ n < c ^ m" by simp
  also from c m have "c ^ m < root m (norm (f m)) ^ m" by (intro power_strict_mono) simp_all
  also from m have "... = norm (f m)" by simp
  finally show False using K(2)[of m]  by simp
qed


subsubsection ‹Cauchy's condensation test›

context
fixes f :: "nat ==> real"
begin

private lemma condensation_inequality:
  assumes mono: "∧m n. 0 < m ==> m ≤ n ==> f n ≤ f m"
  shows   "(∑k=1..≥ (∑k=1.. (is "?thesis1")
          "(∑k=1..≤ (∑k=1.. (is "?thesis2")
  by (intro sum_mono mono floor_log_exp2_ge floor_log_exp2_le, simp, simp)+

private lemma condensation_condense1: "(∑k=1..<2^n. f (2 ^ floor_log k)) = (∑k
proof (induction n)
  case (Suc n)
  have "{1..<2^Suc n} = {1..<2^n} ∪ {2^n..<(2^Suc n :: nat)}" by auto
  also have "(∑k∈…. f (2 ^ floor_log k)) =
                 (∑k∑k = 2^n..<2^Suc n. f (2^floor_log k))"
    by (subst sum.union_disjoint) (insert Suc, auto)
  also have "floor_log k = n" if "k ∈ {2^n..<2^Suc n}" for k using that by (intro floor_log_eqI) simp_all
  hence "(∑k = 2^n..<2^Suc n. f (2^floor_log k)) = (∑(_::nat) = 2^n..<2^Suc n. f (2^n))"
    by (intro sum.cong) simp_all
  also have "… = 2^n * f (2^n)" by (simp)
  finally show ?case by simp
qed simp

private lemma condensation_condense2: "(∑k=1..<2^n. f (2 * 2 ^ floor_log k)) = (∑k
proof (induction n)
  case (Suc n)
  have "{1..<2^Suc n} = {1..<2^n} ∪ {2^n..<(2^Suc n :: nat)}" by auto
  also have "(∑k∈…. f (2 * 2 ^ floor_log k)) =
                 (∑k∑k = 2^n..<2^Suc n. f (2 * 2^floor_log k))"
    by (subst sum.union_disjoint) (insert Suc, auto)
  also have "floor_log k = n" if "k ∈ {2^n..<2^Suc n}" for k using that by (intro floor_log_eqI) simp_all
  hence "(∑k = 2^n..<2^Suc n. f (2*2^floor_log k)) = (∑(_::nat) = 2^n..<2^Suc n. f (2^Suc n))"
    by (intro sum.cong) simp_all
  also have "… = 2^n * f (2^Suc n)" by (simp)
  finally show ?case by simp
qed simp

theorem condensation_test:
  assumes mono: "∧m. 0 < m ==> f (Suc m) ≤ f m"
  assumes nonneg: "∧n. f n ≥ 0"
  shows "summable f ⟷ summable (λn. 2^n * f (2^n))"
proof -
  define f' where "f' n = (if n = 0 then 0 else f n)" for n
  from mono have mono': "decseq (λn. f (Suc n))" by (intro decseq_SucI) simp
  hence mono': "f n ≤ f m" if "m ≤ n" "m > 0" for m n
    using that decseqD[OF mono', of "m - 1" "n - 1"] by simp

  have "(λn. f (Suc n)) = (λn. f' (Suc n))" by (intro ext) (simp add: f'_def)
  hence "summable f ⟷ summable f'"
    by (subst (1 2) summable_Suc_iff [symmetric]) (simp only:)
  also have "… ⟷ convergent (λn. ∑k unfolding summable_iff_convergent ..
  also have "monoseq (λn. ∑k unfolding f'_def
    by (intro mono_SucI1) (auto intro!: mult_nonneg_nonneg nonneg)
  hence "convergent (λn. ∑k⟷ Bseq (λn. ∑k
    by (rule monoseq_imp_convergent_iff_Bseq)
  also have "… ⟷ Bseq (λn. ∑k=1.. unfolding One_nat_def
    by (subst sum_shift_lb_Suc0_0_upt) (simp_all add: f'_def atLeast0LessThan)
  also have "… ⟷ Bseq (λn. ∑k=1.. unfolding f'_def by simp
  also have "… ⟷ Bseq (λn. ∑k=1..<2^n. f k)"
    by (rule nonneg_incseq_Bseq_subseq_iff[symmetric])
       (auto intro!: sum_nonneg incseq_SucI nonneg simp: strict_mono_def)
  also have "… ⟷ Bseq (λn. ∑k
  proof (intro iffI)
    assume A: "Bseq (λn. ∑k=1..<2^n. f k)"
    have "eventually (λn. norm (∑k≤ norm (∑k=1..<2^n. f k)) sequentially"
    proof (intro always_eventually allI)
      fix n :: nat
      have "norm (∑k∑k unfolding real_norm_def
        by (intro abs_of_nonneg sum_nonneg ballI mult_nonneg_nonneg nonneg) simp_all
      also have "… ≤ (∑k=1..<2^n. f k)"
        by (subst condensation_condense2 [symmetric]) (intro condensation_inequality mono')
      also have "… = norm …" unfolding real_norm_def
        by (intro abs_of_nonneg[symmetric] sum_nonneg ballI mult_nonneg_nonneg nonneg)
      finally show "norm (∑k≤ norm (∑k=1..<2^n. f k)" .
    qed
    from this and A have "Bseq (λn. ∑k by (rule Bseq_eventually_mono)
    from Bseq_mult[OF Bfun_const[of 2] this] have "Bseq (λn. ∑k
      by (simp add: sum_distrib_left sum_distrib_right mult_ac)
    hence "Bseq (λn. (∑k=Suc 0..
      by (intro Bseq_add, subst sum.shift_bounds_Suc_ivl) (simp add: atLeast0LessThan)
    hence "Bseq (λn. (∑k=0..
      by (subst sum.atLeast_Suc_lessThan) (simp_all add: add_ac)
    thus "Bseq (λn. (∑k
      by (subst (asm) Bseq_Suc_iff) (simp add: atLeast0LessThan)
  next
    assume A: "Bseq (λn. (∑k
    have "eventually (λn. norm (∑k=1..<2^n. f k) ≤ norm (∑k
    proof (intro always_eventually allI)
      fix n :: nat
      have "norm (∑k=1..<2^n. f k) = (∑k=1..<2^n. f k)" unfolding real_norm_def
        by (intro abs_of_nonneg sum_nonneg ballI mult_nonneg_nonneg nonneg)
      also have "… ≤ (∑k
        by (subst condensation_condense1 [symmetric]) (intro condensation_inequality mono')
      also have "… = norm …" unfolding real_norm_def
        by (intro abs_of_nonneg [symmetric] sum_nonneg ballI mult_nonneg_nonneg nonneg) simp_all
      finally show "norm (∑k=1..<2^n. f k) ≤ norm (∑k .
    qed
    from this and A show "Bseq (λn. ∑k=1..<2^n. f k)" by (rule Bseq_eventually_mono)
  qed
  also have "monoseq (λn. (∑k
    by (intro mono_SucI1) (auto intro!: mult_nonneg_nonneg nonneg)
  hence "Bseq (λn. (∑k⟷ convergent (λn. (∑k
    by (rule monoseq_imp_convergent_iff_Bseq [symmetric])
  also have "… ⟷ summable (λk. 2^k * f (2^k))" by (simp only: summable_iff_convergent)
  finally show ?thesis .
qed

end


subsubsection ‹Summability of powers›

lemma abs_summable_complex_powr_iff:
    "summable (λn. norm (exp (of_real (ln (of_nat n)) * s))) ⟷ Re s < -1"
proof (cases "Re s ≤ 0")
  let ?l = "λn. complex_of_real (ln (of_nat n))"
  case False
  have "eventually (λn. norm (1 :: real) ≤ norm (exp (?l n * s))) sequentially"
    apply (rule eventually_mono [OF eventually_gt_at_top[of "0::nat"]])
    using False ge_one_powr_ge_zero by auto
  from summable_comparison_test_ev[OF this] False show ?thesis by (auto simp: summable_const_iff)
next
  let ?l = "λn. complex_of_real (ln (of_nat n))"
  case True
  hence "summable (λn. norm (exp (?l n * s))) ⟷ summable (λn. 2^n * norm (exp (?l (2^n) * s)))"
    by (intro condensation_test) (auto intro!: mult_right_mono_neg)
  also have "(λn. 2^n * norm (exp (?l (2^n) * s))) = (λn. (2 powr (Re s + 1)) ^ n)"
  proof
    fix n :: nat
    have "2^n * norm (exp (?l (2^n) * s)) = exp (real n * ln 2) * exp (real n * ln 2 * Re s)"
      using True by (subst exp_of_nat_mult) (simp add: ln_realpow algebra_simps)
    also have "… = exp (real n * (ln 2 * (Re s + 1)))"
      by (simp add: algebra_simps exp_add)
    also have "… = exp (ln 2 * (Re s + 1)) ^ n" by (subst exp_of_nat_mult) simp
    also have "exp (ln 2 * (Re s + 1)) = 2 powr (Re s + 1)" by (simp add: powr_def)
    finally show "2^n * norm (exp (?l (2^n) * s)) = (2 powr (Re s + 1)) ^ n" .
  qed
  also have "summable … ⟷ 2 powr (Re s + 1) < 2 powr 0"
    by (subst summable_geometric_iff) simp
  also have "… ⟷ Re s < -1" by (subst powr_less_cancel_iff) (simp, linarith)
  finally show ?thesis .
qed

theorem summable_complex_powr_iff:
  assumes "Re s < -1"
  shows   "summable (λn. exp (of_real (ln (of_nat n)) * s))"
  by (rule summable_norm_cancel, subst abs_summable_complex_powr_iff) fact

lemma summable_real_powr_iff: "summable (λn. of_nat n powr s :: real) ⟷ s < -1"
proof -
  from eventually_gt_at_top[of "0::nat"]
    have "summable (λn. of_nat n powr s) ⟷ summable (λn. exp (ln (of_nat n) * s))"
    by (intro summable_cong) (auto elim!: eventually_mono simp: powr_def)
  also have "… ⟷ s < -1" using abs_summable_complex_powr_iff[of "of_real s"] by simp
  finally show ?thesis .
qed

lemma summable_power_int_real_iff:
  "summable (λn. real n powi c) ⟷ c < -1"
proof -
  have "summable (λn. real n powi c) ⟷ summable (λn. real (Suc n) powi c)"
    by (subst summable_Suc_iff) auto
  also have "(λn. real (Suc n) powi c) = (λn. real (Suc n) powr of_int c)"
    by (subst powr_real_of_int') auto
  also have "summable … ⟷ summable (λn. real n powr of_int c)"
    by (subst summable_Suc_iff) auto
  also have "… ⟷ c < -1"
    by (subst summable_real_powr_iff) auto
  finally show ?thesis .
qed

lemma inverse_power_summable:
  assumes s: "s ≥ 2"
  shows "summable (λn. inverse (of_nat n ^ s :: 'a :: {real_normed_div_algebra,banach}))"
proof (rule summable_norm_cancel, subst summable_cong)
  from eventually_gt_at_top[of "0::nat"]
    show "eventually (λn. norm (inverse (of_nat n ^ s:: 'a)) = real_of_nat n powr (-real s)) at_top"
    by eventually_elim (simp add: norm_inverse norm_power powr_minus powr_realpow)
qed (insert s summable_real_powr_iff[of "-s"], simp_all)

lemma not_summable_harmonic: "¬summable (λn. inverse (of_nat n) :: 'a :: real_normed_field)"
proof
  assume "summable (λn. inverse (of_nat n) :: 'a)"
  hence "convergent (λn. norm (of_real (∑k
    by (simp add: summable_iff_convergent convergent_norm)
  hence "convergent (λn. abs (∑k by (simp only: norm_of_real)
  also have "(λn. abs (∑k∑k
    by (intro ext abs_of_nonneg sum_nonneg) auto
  also have "convergent … ⟷ summable (λk. inverse (of_nat k) :: real)"
    by (simp add: summable_iff_convergent)
  finally show False using summable_real_powr_iff[of "-1"] by (simp add: powr_minus)
qed


subsubsection ‹Kummer's test›

theorem kummers_test_convergence:
  fixes f p :: "nat ==> real"
  assumes pos_f: "eventually (λn. f n > 0) sequentially"
  assumes nonneg_p: "eventually (λn. p n ≥ 0) sequentially"
  defines "l ≡ liminf (λn. ereal (p n * f n / f (Suc n) - p (Suc n)))"
  assumes l: "l > 0"
  shows   "summable f"
  unfolding summable_iff_convergent'
proof -
  define r where "r = (if l = ∞ then 1 else real_of_ereal l / 2)"
  from l have "r > 0 ∧ of_real r < l" by (cases l) (simp_all add: r_def)
  hence r: "r > 0" "of_real r < l" by simp_all
  hence "eventually (λn. p n * f n / f (Suc n) - p (Suc n) > r) sequentially"
    unfolding l_def by (force dest: less_LiminfD)
  moreover from pos_f have "eventually (λn. f (Suc n) > 0) sequentially"
    by (subst eventually_sequentially_Suc)
  ultimately have "eventually (λn. p n * f n - p (Suc n) * f (Suc n) > r * f (Suc n)) sequentially"
    by eventually_elim (simp add: field_simps)
  from eventually_conj[OF pos_f eventually_conj[OF nonneg_p this]]
    obtain m where m: "∧n. n ≥ m ==> f n > 0" "∧n. n ≥ m ==> p n ≥ 0"
        "∧n. n ≥ m ==> p n * f n - p (Suc n) * f (Suc n) > r * f (Suc n)"
    unfolding eventually_at_top_linorder by blast

  let ?c = "(norm (∑k≤m. r * f k) + p m * f m) / r"
  have "Bseq (λn. (∑k≤n + Suc m. f k))"
  proof (rule BseqI')
    fix k :: nat
    define n where "n = k + Suc m"
    have n: "n > m" by (simp add: n_def)

    from r have "r * norm (∑k≤n. f k) = norm (∑k≤n. r * f k)"
      by (simp add: sum_distrib_left[symmetric] abs_mult)
    also from n have "{..n} = {..m} ∪ {Suc m..n}" by auto
    hence "(∑k≤n. r * f k) = (∑k∈{..m} ∪ {Suc m..n}. r * f k)" by (simp only:)
    also have "… = (∑k≤m. r * f k) + (∑k=Suc m..n. r * f k)"
      by (subst sum.union_disjoint) auto
    also have "norm … ≤ norm (∑k≤m. r * f k) + norm (∑k=Suc m..n. r * f k)"
      by (rule norm_triangle_ineq)
    also from r less_imp_le[OF m(1)] have "(∑k=Suc m..n. r * f k) ≥ 0"
      by (intro sum_nonneg) auto
    hence "norm (∑k=Suc m..n. r * f k) = (∑k=Suc m..n. r * f k)" by simp
    also have "(∑k=Suc m..n. r * f k) = (∑k=m..
     by (subst sum.shift_bounds_Suc_ivl [symmetric])
          (simp only: atLeastLessThanSuc_atLeastAtMost)
    also from m have "… ≤ (∑k=m..
      by (intro sum_mono[OF less_imp_le]) simp_all
    also have "… = -(∑k=m..
      by (simp add: sum_negf [symmetric] algebra_simps)
    also from n have "… = p m * f m - p n * f n"
      by (cases n, simp, simp only: atLeastLessThanSuc_atLeastAtMost, subst sum_Suc_diff) simp_all
    also from less_imp_le[OF m(1)] m(2) n have "… ≤ p m * f m" by simp
    finally show "norm (∑k≤n. f k) ≤ (norm (∑k≤m. r * f k) + p m * f m) / r" using r
      by (subst pos_le_divide_eq[OF r(1)]) (simp only: mult_ac)
  qed
  moreover have "(∑k≤n. f k) ≤ (∑k≤n'. f k)" if "Suc m ≤ n" "n ≤ n'" for n n'
    using less_imp_le[OF m(1)] that by (intro sum_mono2) auto
  ultimately show "convergent (λn. ∑k≤n. f k)" by (rule Bseq_monoseq_convergent'_inc)
qed


theorem kummers_test_divergence:
  fixes f p :: "nat ==> real"
  assumes pos_f: "eventually (λn. f n > 0) sequentially"
  assumes pos_p: "eventually (λn. p n > 0) sequentially"
  assumes divergent_p: "¬summable (λn. inverse (p n))"
  defines "l ≡ limsup (λn. ereal (p n * f n / f (Suc n) - p (Suc n)))"
  assumes l: "l < 0"
  shows   "¬summable f"
proof
  assume "summable f"
  from eventually_conj[OF pos_f eventually_conj[OF pos_p Limsup_lessD[OF l[unfolded l_def]]]]
    obtain N where N: "∧n. n ≥ N ==> p n > 0" "∧n. n ≥ N ==> f n > 0"
                      "∧n. n ≥ N ==> p n * f n / f (Suc n) - p (Suc n) < 0"
    by (auto simp: eventually_at_top_linorder)
  hence A: "p n * f n < p (Suc n) * f (Suc n)" if "n ≥ N" for n using that N[of n] N[of "Suc n"]
    by (simp add: field_simps)
  have B: "p n * f n ≥ p N * f N" if "n ≥ N" for n using that and A
    by (induction n rule: dec_induct) (auto intro!: less_imp_le elim!: order.trans)
  have "eventually (λn. norm (p N * f N * inverse (p n)) ≤ f n) sequentially"
    apply (rule eventually_mono [OF eventually_ge_at_top[of N]])
    using B N  by (auto  simp: field_simps abs_of_pos)
  from this and ‹summable f› have "summable (λn. p N * f N * inverse (p n))"
    by (rule summable_comparison_test_ev)
  from summable_mult[OF this, of "inverse (p N * f N)"] N[OF le_refl]
    have "summable (λn. inverse (p n))" by (simp add: field_split_simps)
  with divergent_p show False by contradiction
qed


subsubsection ‹Ratio test›

theorem ratio_test_convergence:
  fixes f :: "nat ==> real"
  assumes pos_f: "eventually (λn. f n > 0) sequentially"
  defines "l ≡ liminf (λn. ereal (f n / f (Suc n)))"
  assumes l: "l > 1"
  shows   "summable f"
proof (rule kummers_test_convergence[OF pos_f])
  note l
  also have "l = liminf (λn. ereal (f n / f (Suc n) - 1)) + 1"
    by (subst Liminf_add_ereal_right[symmetric]) (simp_all add: minus_ereal_def l_def one_ereal_def)
  finally show "liminf (λn. ereal (1 * f n / f (Suc n) - 1)) > 0"
    by (cases "liminf (λn. ereal (1 * f n / f (Suc n) - 1))") simp_all
qed simp

theorem ratio_test_divergence:
  fixes f :: "nat ==> real"
  assumes pos_f: "eventually (λn. f n > 0) sequentially"
  defines "l ≡ limsup (λn. ereal (f n / f (Suc n)))"
  assumes l: "l < 1"
  shows   "¬summable f"
proof (rule kummers_test_divergence[OF pos_f])
  have "limsup (λn. ereal (f n / f (Suc n) - 1)) + 1 = l"
    by (subst Limsup_add_ereal_right[symmetric]) (simp_all add: minus_ereal_def l_def one_ereal_def)
  also note l
  finally show "limsup (λn. ereal (1 * f n / f (Suc n) - 1)) < 0"
    by (cases "limsup (λn. ereal (1 * f n / f (Suc n) - 1))") simp_all
qed (simp_all add: summable_const_iff)


subsubsection ‹Raabe's test›

theorem raabes_test_convergence:
fixes f :: "nat ==> real"
  assumes pos: "eventually (λn. f n > 0) sequentially"
  defines "l ≡ liminf (λn. ereal (of_nat n * (f n / f (Suc n) - 1)))"
  assumes l: "l > 1"
  shows   "summable f"
proof (rule kummers_test_convergence)
  let ?l' = "liminf (λn. ereal (of_nat n * f n / f (Suc n) - of_nat (Suc n)))"
  have "1 < l" by fact
  also have "l = liminf (λn. ereal (of_nat n * f n / f (Suc n) - of_nat (Suc n)) + 1)"
    by (simp add: l_def algebra_simps)
  also have "… = ?l' + 1" by (subst Liminf_add_ereal_right) simp_all
  finally show "?l' > 0" by (cases ?l') (simp_all add: algebra_simps)
qed (simp_all add: pos)

theorem raabes_test_divergence:
fixes f :: "nat ==> real"
  assumes pos: "eventually (λn. f n > 0) sequentially"
  defines "l ≡ limsup (λn. ereal (of_nat n * (f n / f (Suc n) - 1)))"
  assumes l: "l < 1"
  shows   "¬summable f"
proof (rule kummers_test_divergence)
  let ?l' = "limsup (λn. ereal (of_nat n * f n / f (Suc n) - of_nat (Suc n)))"
  note l
  also have "l = limsup (λn. ereal (of_nat n * f n / f (Suc n) - of_nat (Suc n)) + 1)"
    by (simp add: l_def algebra_simps)
  also have "… = ?l' + 1" by (subst Limsup_add_ereal_right) simp_all
  finally show "?l' < 0" by (cases ?l') (simp_all add: algebra_simps)
qed (insert pos eventually_gt_at_top[of "0::nat"] not_summable_harmonic, simp_all)


subsection ‹Radius of convergence›

text ‹
  The radius of convergence of a power series. This value always exists, ranges from
  🍋‹0::ereal› to 🍋‹∞::ereal›, and the power series is guaranteed to converge for
  all inputs with a norm that is smaller than that radius and to diverge for all inputs with a
  norm that is greater.
 ›
definition🍋‹tag important› conv_radius :: "(nat ==> 'a :: banach) ==> ereal" where
  "conv_radius f = inverse (limsup (λn. ereal (root n (norm (f n)))))"

lemma conv_radius_cong_weak [cong]: "(∧n. f n = g n) ==> conv_radius f = conv_radius g"
  by (drule ext) simp_all

lemma conv_radius_nonneg: "conv_radius f ≥ 0"
proof -
  have "0 = limsup (λn. 0)" by (subst Limsup_const) simp_all
  also have "… ≤ limsup (λn. ereal (root n (norm (f n))))"
    by (intro Limsup_mono) (simp_all add: real_root_ge_zero)
  finally show ?thesis
    unfolding conv_radius_def by (auto simp: ereal_inverse_nonneg_iff)
qed

lemma conv_radius_zero [simp]: "conv_radius (λ_. 0) = ∞"
  by (auto simp: conv_radius_def zero_ereal_def [symmetric] Limsup_const)

lemma conv_radius_altdef:
  "conv_radius f = liminf (λn. inverse (ereal (root n (norm (f n)))))"
  by (subst Liminf_inverse_ereal) (simp_all add: real_root_ge_zero conv_radius_def)

lemma conv_radius_cong':
  assumes "eventually (λx. f x = g x) sequentially"
  shows   "conv_radius f = conv_radius g"
  unfolding conv_radius_altdef by (intro Liminf_eq eventually_mono [OF assms]) auto

lemma conv_radius_cong:
  assumes "eventually (λx. norm (f x) = norm (g x)) sequentially"
  shows   "conv_radius f = conv_radius g"
  unfolding conv_radius_altdef by (intro Liminf_eq eventually_mono [OF assms]) auto

theorem abs_summable_in_conv_radius:
  fixes f :: "nat ==> 'a :: {banach, real_normed_div_algebra}"
  assumes "ereal (norm z) < conv_radius f"
  shows   "summable (λn. norm (f n * z ^ n))"
proof (rule root_test_convergence')
  define l where "l = limsup (λn. ereal (root n (norm (f n))))"
  have "0 = limsup (λn. 0)" by (simp add: Limsup_const)
  also have "... ≤ l" unfolding l_def by (intro Limsup_mono) (simp_all add: real_root_ge_zero)
  finally have l_nonneg: "l ≥ 0" .

  have "limsup (λn. root n (norm (f n * z^n))) = l * ereal (norm z)" unfolding l_def
    by (rule limsup_root_powser)
  also from l_nonneg consider "l = 0" | "l = ∞" | "∃l'. l = ereal l' ∧ l' > 0"
    by (cases "l") (auto simp: less_le)
  hence "l * ereal (norm z) < 1"
  proof cases
    assume "l = ∞"
    hence "conv_radius f = 0" unfolding conv_radius_def l_def by simp
    with assms show ?thesis by simp
  next
    assume "∃l'. l = ereal l' ∧ l' > 0"
    then obtain l' where l': "l = ereal l'" "0 < l'" by auto
    hence "l ≠ ∞" by auto
    have "l * ereal (norm z) < l * conv_radius f"
      by (intro ereal_mult_strict_left_mono) (simp_all add: l' assms)
    also have "conv_radius f = inverse l" by (simp add: conv_radius_def l_def)
    also from l' have "l * inverse l = 1" by simp
    finally show ?thesis .
  qed simp_all
  finally show "limsup (λn. ereal (root n (norm (norm (f n * z ^ n))))) < 1" by simp
qed

lemma summable_in_conv_radius:
  fixes f :: "nat ==> 'a :: {banach, real_normed_div_algebra}"
  assumes "ereal (norm z) < conv_radius f"
  shows   "summable (λn. f n * z ^ n)"
  by (rule summable_norm_cancel, rule abs_summable_in_conv_radius) fact+

theorem not_summable_outside_conv_radius:
  fixes f :: "nat ==> 'a :: {banach, real_normed_div_algebra}"
  assumes "ereal (norm z) > conv_radius f"
  shows   "¬summable (λn. f n * z ^ n)"
proof (rule root_test_divergence)
  define l where "l = limsup (λn. ereal (root n (norm (f n))))"
  have "0 = limsup (λn. 0)" by (simp add: Limsup_const)
  also have "... ≤ l" unfolding l_def by (intro Limsup_mono) (simp_all add: real_root_ge_zero)
  finally have l_nonneg: "l ≥ 0" .
  from assms have l_nz: "l ≠ 0" unfolding conv_radius_def l_def by auto

  have "limsup (λn. ereal (root n (norm (f n * z^n)))) = l * ereal (norm z)"
    unfolding l_def by (rule limsup_root_powser)
  also have "... > 1"
  proof (cases l)
    assume "l = ∞"
    with assms conv_radius_nonneg[of f] show ?thesis
      by (auto simp: zero_ereal_def[symmetric])
  next
    fix l' assume l': "l = ereal l'"
    from l_nonneg l_nz have "1 = l * inverse l" by (auto simp: l' field_simps)
    also from l_nz have "inverse l = conv_radius f"
      unfolding l_def conv_radius_def by auto
    also from l' l_nz l_nonneg assms have "l * … < l * ereal (norm z)"
      by (intro ereal_mult_strict_left_mono) (auto simp: l')
    finally show ?thesis .
  qed (insert l_nonneg, simp_all)
  finally show "limsup (λn. ereal (root n (norm (f n * z^n)))) > 1" .
qed


lemma conv_radius_geI:
  assumes "summable (λn. f n * z ^ n :: 'a :: {banach, real_normed_div_algebra})"
  shows   "conv_radius f ≥ norm z"
  using not_summable_outside_conv_radius[of f z] assms by (force simp: not_le[symmetric])

lemma conv_radius_leI:
  assumes "¬summable (λn. norm (f n * z ^ n :: 'a :: {banach, real_normed_div_algebra}))"
  shows   "conv_radius f ≤ norm z"
  using abs_summable_in_conv_radius[of z f] assms by (force simp: not_le[symmetric])

lemma conv_radius_leI':
  assumes "¬summable (λn. f n * z ^ n :: 'a :: {banach, real_normed_div_algebra})"
  shows   "conv_radius f ≤ norm z"
  using summable_in_conv_radius[of z f] assms by (force simp: not_le[symmetric])

lemma conv_radius_geI_ex:
  fixes f :: "nat ==> 'a :: {banach, real_normed_div_algebra}"
  assumes "∧r. 0 < r ==> ereal r < R ==> ∃z. norm z = r ∧ summable (λn. f n * z^n)"
  shows   "conv_radius f ≥ R"
proof (rule linorder_cases[of "conv_radius f" R])
  assume R: "conv_radius f < R"
  with conv_radius_nonneg[of f] obtain conv_radius'
    where [simp]: "conv_radius f = ereal conv_radius'"
    by (cases "conv_radius f") simp_all
  define r where "r = (if R = ∞ then conv_radius' + 1 else (real_of_ereal R + conv_radius') / 2)"
  from R conv_radius_nonneg[of f] have "0 < r ∧ ereal r < R ∧ ereal r > conv_radius f"
    unfolding r_def by (cases R) (auto simp: r_def field_simps)
  with assms(1)[of r] obtain z where "norm z > conv_radius f" "summable (λn. f n * z^n)" by auto
  with not_summable_outside_conv_radius[of f z] show ?thesis by simp
qed simp_all

lemma conv_radius_geI_ex':
  fixes f :: "nat ==> 'a :: {banach, real_normed_div_algebra}"
  assumes "∧r. 0 < r ==> ereal r < R ==> summable (λn. f n * of_real r^n)"
  shows   "conv_radius f ≥ R"
proof (rule conv_radius_geI_ex)
  fix r assume "0 < r" "ereal r < R"
  with assms[of r] show "∃z. norm z = r ∧ summable (λn. f n * z ^ n)"
    by (intro exI[of _ "of_real r :: 'a"]) auto
qed

lemma conv_radius_leI_ex:
  fixes f :: "nat ==> 'a :: {banach, real_normed_div_algebra}"
  assumes "R ≥ 0"
  assumes "∧r. 0 < r ==> ereal r > R ==> ∃z. norm z = r ∧ ¬summable (λn. norm (f n * z^n))"
  shows   "conv_radius f ≤ R"
proof (rule linorder_cases[of "conv_radius f" R])
  assume R: "conv_radius f > R"
  from R assms(1) obtain R' where R': "R = ereal R'" by (cases R) simp_all
  define r where
    "r = (if conv_radius f = ∞ then R' + 1 else (R' + real_of_ereal (conv_radius f)) / 2)"
  from R conv_radius_nonneg[of f] have "r > R ∧ r < conv_radius f" unfolding r_def
    by (cases "conv_radius f") (auto simp: r_def field_simps R')
  with assms(1) assms(2)[of r] R'
    obtain z where "norm z < conv_radius f" "¬summable (λn. norm (f n * z^n))" by auto
  with abs_summable_in_conv_radius[of z f] show ?thesis by auto
qed simp_all

lemma conv_radius_leI_ex':
  fixes f :: "nat ==> 'a :: {banach, real_normed_div_algebra}"
  assumes "R ≥ 0"
  assumes "∧r. 0 < r ==> ereal r > R ==> ¬summable (λn. f n * of_real r^n)"
  shows   "conv_radius f ≤ R"
proof (rule conv_radius_leI_ex)
  fix r assume "0 < r" "ereal r > R"
  with assms(2)[of r] show "∃z. norm z = r ∧ ¬summable (λn. norm (f n * z ^ n))"
    by (intro exI[of _ "of_real r :: 'a"]) (auto dest: summable_norm_cancel)
qed fact+

lemma conv_radius_eqI:
  fixes f :: "nat ==> 'a :: {banach, real_normed_div_algebra}"
  assumes "R ≥ 0"
  assumes "∧r. 0 < r ==> ereal r < R ==> ∃z. norm z = r ∧ summable (λn. f n * z^n)"
  assumes "∧r. 0 < r ==> ereal r > R ==> ∃z. norm z = r ∧ ¬summable (λn. norm (f n * z^n))"
  shows   "conv_radius f = R"
  by (intro antisym conv_radius_geI_ex conv_radius_leI_ex assms)

lemma conv_radius_eqI':
  fixes f :: "nat ==> 'a :: {banach, real_normed_div_algebra}"
  assumes "R ≥ 0"
  assumes "∧r. 0 < r ==> ereal r < R ==> summable (λn. f n * (of_real r)^n)"
  assumes "∧r. 0 < r ==> ereal r > R ==> ¬summable (λn. norm (f n * (of_real r)^n))"
  shows   "conv_radius f = R"
proof (intro conv_radius_eqI[OF assms(1)])
  fix r assume "0 < r" "ereal r < R" with assms(2)[OF this]
    show "∃z. norm z = r ∧ summable (λn. f n * z ^ n)" by force
next
  fix r assume "0 < r" "ereal r > R" with assms(3)[OF this]
    show "∃z. norm z = r ∧ ¬summable (λn. norm (f n * z ^ n))" by force
qed

lemma conv_radius_zeroI:
  fixes f :: "nat ==> 'a :: {banach,real_normed_div_algebra}"
  assumes "∧z. z ≠ 0 ==> ¬summable (λn. f n * z^n)"
  shows   "conv_radius f = 0"
proof (rule ccontr)
  assume "conv_radius f ≠ 0"
  with conv_radius_nonneg[of f] have pos: "conv_radius f > 0" by simp
  define r where "r = (if conv_radius f = ∞ then 1 else real_of_ereal (conv_radius f) / 2)"
  from pos have r: "ereal r > 0 ∧ ereal r < conv_radius f"
    by (cases "conv_radius f") (simp_all add: r_def)
  hence "summable (λn. f n * of_real r ^ n)" by (intro summable_in_conv_radius) simp
  moreover from r and assms[of "of_real r"] have "¬summable (λn. f n * of_real r ^ n)" by simp
  ultimately show False by contradiction
qed

lemma conv_radius_inftyI':
  fixes f :: "nat ==> 'a :: {banach,real_normed_div_algebra}"
  assumes "∧r. r > c ==> ∃z. norm z = r ∧ summable (λn. f n * z^n)"
  shows   "conv_radius f = ∞"
proof -
  {
    fix r :: real
    have "max r (c + 1) > c" by (auto simp: max_def)
    from assms[OF this] obtain z where "norm z = max r (c + 1)" "summable (λn. f n * z^n)" by blast
    from conv_radius_geI[OF this(2)] this(1) have "conv_radius f ≥ r" by simp
  }
  from this[of "real_of_ereal (conv_radius f + 1)"] show "conv_radius f = ∞"
    by (cases "conv_radius f") simp_all
qed

lemma conv_radius_inftyI:
  fixes f :: "nat ==> 'a :: {banach,real_normed_div_algebra}"
  assumes "∧r. ∃z. norm z = r ∧ summable (λn. f n * z^n)"
  shows   "conv_radius f = ∞"
  using assms by (rule conv_radius_inftyI')

lemma conv_radius_inftyI'':
  fixes f :: "nat ==> 'a :: {banach,real_normed_div_algebra}"
  assumes "∧z. summable (λn. f n * z^n)"
  shows   "conv_radius f = ∞"
proof (rule conv_radius_inftyI')
  fix r :: real assume "r > 0"
  with assms show "∃z. norm z = r ∧ summable (λn. f n * z^n)"
    by (intro exI[of _ "of_real r"]) simp
qed

lemma conv_radius_conv_Sup:
  fixes f :: "nat ==> 'a :: {banach, real_normed_div_algebra}"
  shows "conv_radius f = Sup {r. ∀z. ereal (norm z) < r ⟶ summable (λn. f n * z ^ n)}"
proof (rule Sup_eqI [symmetric], goal_cases)
  case (1 r)
  thus ?case
    by (intro conv_radius_geI_ex') auto
next
  case (2 r)
  from 2[of 0] have r: "r ≥ 0" by auto
  show ?case
  proof (intro conv_radius_leI_ex' r)
    fix R assume R: "R > 0" "ereal R > r"
    with r obtain r' where [simp]: "r = ereal r'" by (cases r) auto
    show "¬summable (λn. f n * of_real R ^ n)"
    proof
      assume *: "summable (λn. f n * of_real R ^ n)"
      define R' where "R' = (R + r') / 2"
      from R have R': "R' > r'" "R' < R" by (simp_all add: R'_def)
      hence "∀z. norm z < R' ⟶ summable (λn. f n * z ^ n)"
        using powser_inside[OF *] by auto
      from 2[of R'] and this have "R' ≤ r'" by auto
      with ‹R' > r'› show False by simp
    qed
  qed
qed

lemma conv_radius_shift:
  fixes f :: "nat ==> 'a :: {banach, real_normed_div_algebra}"
  shows   "conv_radius (λn. f (n + m)) = conv_radius f"
  unfolding conv_radius_conv_Sup summable_powser_ignore_initial_segment ..

lemma conv_radius_norm [simp]: "conv_radius (λx. norm (f x)) = conv_radius f"
  by (simp add: conv_radius_def)

lemma conv_radius_ratio_limit_ereal:
  fixes f :: "nat ==> 'a :: {banach,real_normed_div_algebra}"
  assumes nz:  "eventually (λn. f n ≠ 0) sequentially"
  assumes lim: "(λn. ereal (norm (f n) / norm (f (Suc n)))) <---- c"
  shows   "conv_radius f = c"
proof (rule conv_radius_eqI')
  show "c ≥ 0" by (intro Lim_bounded2[OF lim]) simp_all
next
  fix r assume r: "0 < r" "ereal r < c"
  let ?l = "liminf (λn. ereal (norm (f n * of_real r ^ n) / norm (f (Suc n) * of_real r ^ Suc n)))"
  have "?l = liminf (λn. ereal (norm (f n) / (norm (f (Suc n)))) * ereal (inverse r))"
    using r by (simp add: norm_mult norm_power field_split_simps)
  also from r have "… = liminf (λn. ereal (norm (f n) / (norm (f (Suc n))))) * ereal (inverse r)"
    by (intro Liminf_ereal_mult_right) simp_all
  also have "liminf (λn. ereal (norm (f n) / (norm (f (Suc n))))) = c"
    by (intro lim_imp_Liminf lim) simp
  finally have l: "?l = c * ereal (inverse r)" by simp
  from r have  l': "c * ereal (inverse r) > 1" by (cases c) (simp_all add: field_simps)
  show "summable (λn. f n * of_real r^n)"
    by (rule summable_norm_cancel, rule ratio_test_convergence)
       (insert r nz l l', auto elim!: eventually_mono)
next
  fix r assume r: "0 < r" "ereal r > c"
  let ?l = "limsup (λn. ereal (norm (f n * of_real r ^ n) / norm (f (Suc n) * of_real r ^ Suc n)))"
  have "?l = limsup (λn. ereal (norm (f n) / (norm (f (Suc n)))) * ereal (inverse r))"
    using r by (simp add: norm_mult norm_power field_split_simps)
  also from r have "… = limsup (λn. ereal (norm (f n) / (norm (f (Suc n))))) * ereal (inverse r)"
    by (intro Limsup_ereal_mult_right) simp_all
  also have "limsup (λn. ereal (norm (f n) / (norm (f (Suc n))))) = c"
    by (intro lim_imp_Limsup lim) simp
  finally have l: "?l = c * ereal (inverse r)" by simp
  from r have  l': "c * ereal (inverse r) < 1" by (cases c) (simp_all add: field_simps)
  show "¬summable (λn. norm (f n * of_real r^n))"
    by (rule ratio_test_divergence) (insert r nz l l', auto elim!: eventually_mono)
qed

lemma conv_radius_ratio_limit_ereal_nonzero:
  fixes f :: "nat ==> 'a :: {banach,real_normed_div_algebra}"
  assumes nz:  "c ≠ 0"
  assumes lim: "(λn. ereal (norm (f n) / norm (f (Suc n)))) <---- c"
  shows   "conv_radius f = c"
proof (rule conv_radius_ratio_limit_ereal[OF _ lim], rule ccontr)
  assume "¬eventually (λn. f n ≠ 0) sequentially"
  hence "frequently (λn. f n = 0) sequentially" by (simp add: frequently_def)
  hence "frequently (λn. ereal (norm (f n) / norm (f (Suc n))) = 0) sequentially"
    by (force elim!: frequently_elim1)
  hence "c = 0" by (intro limit_frequently_eq[OF _ _ lim]) auto
  with nz show False by contradiction
qed

lemma conv_radius_ratio_limit:
  fixes f :: "nat ==> 'a :: {banach,real_normed_div_algebra}"
  assumes "c' = ereal c"
  assumes nz:  "eventually (λn. f n ≠ 0) sequentially"
  assumes lim: "(λn. norm (f n) / norm (f (Suc n))) <---- c"
  shows   "conv_radius f = c'"
  using assms by (intro conv_radius_ratio_limit_ereal) simp_all

lemma conv_radius_ratio_limit_nonzero:
  fixes f :: "nat ==> 'a :: {banach,real_normed_div_algebra}"
  assumes "c' = ereal c"
  assumes nz:  "c ≠ 0"
  assumes lim: "(λn. norm (f n) / norm (f (Suc n))) <---- c"
  shows   "conv_radius f = c'"
  using assms by (intro conv_radius_ratio_limit_ereal_nonzero) simp_all

lemma conv_radius_cmult_left:
  assumes "c ≠ (0 :: 'a :: {banach, real_normed_div_algebra})"
  shows   "conv_radius (λn. c * f n) = conv_radius f"
proof -
  have "conv_radius (λn. c * f n) =
          inverse (limsup (λn. ereal (root n (norm (c * f n)))))"
    unfolding conv_radius_def ..
  also have "(λn. ereal (root n (norm (c * f n)))) =
               (λn. ereal (root n (norm c)) * ereal (root n (norm (f n))))"
    by (rule ext) (auto simp: norm_mult real_root_mult)
  also have "limsup … = ereal 1 * limsup (λn. ereal (root n (norm (f n))))"
    using assms by (intro ereal_limsup_lim_mult tendsto_ereal LIMSEQ_root_const) auto
  also have "inverse … = conv_radius f" by (simp add: conv_radius_def)
  finally show ?thesis .
qed

lemma conv_radius_cmult_right:
  assumes "c ≠ (0 :: 'a :: {banach, real_normed_div_algebra})"
  shows   "conv_radius (λn. f n * c) = conv_radius f"
proof -
  have "conv_radius (λn. f n * c) = conv_radius (λn. c * f n)"
    by (simp add: conv_radius_def norm_mult mult.commute)
  with conv_radius_cmult_left[OF assms, of f] show ?thesis by simp
qed

lemma conv_radius_mult_power:
  assumes "c ≠ (0 :: 'a :: {real_normed_div_algebra,banach})"
  shows   "conv_radius (λn. c ^ n * f n) = conv_radius f / ereal (norm c)"
proof -
  have "limsup (λn. ereal (root n (norm (c ^ n * f n)))) =
          limsup (λn. ereal (norm c) * ereal (root n (norm (f n))))"
    by (intro Limsup_eq eventually_mono [OF eventually_gt_at_top[of "0::nat"]])
       (auto simp: norm_mult norm_power real_root_mult real_root_power)
  also have "… = ereal (norm c) * limsup (λn. ereal (root n (norm (f n))))"
    using assms by (subst Limsup_ereal_mult_left[symmetric]) simp_all
  finally have A: "limsup (λn. ereal (root n (norm (c ^ n * f n)))) =
                       ereal (norm c) * limsup (λn. ereal (root n (norm (f n))))" .
  show ?thesis using assms
    apply (cases "limsup (λn. ereal (root n (norm (f n)))) = 0")
    apply (simp add: A conv_radius_def)
    apply (unfold conv_radius_def A divide_ereal_def, simp add: mult.commute ereal_inverse_mult)
    done
qed

lemma conv_radius_mult_power_right:
  assumes "c ≠ (0 :: 'a :: {real_normed_div_algebra,banach})"
  shows   "conv_radius (λn. f n * c ^ n) = conv_radius f / ereal (norm c)"
  using conv_radius_mult_power[OF assms, of f]
  unfolding conv_radius_def by (simp add: mult.commute norm_mult)

lemma conv_radius_divide_power:
  assumes "c ≠ (0 :: 'a :: {real_normed_div_algebra,banach})"
  shows   "conv_radius (λn. f n / c^n) = conv_radius f * ereal (norm c)"
proof -
  from assms have "inverse c ≠ 0" by simp
  from conv_radius_mult_power_right[OF this, of f] show ?thesis
    by (simp add: divide_inverse divide_ereal_def assms norm_inverse power_inverse)
qed


lemma conv_radius_add_ge:
  "min (conv_radius f) (conv_radius g) ≤
       conv_radius (λx. f x + g x :: 'a :: {banach,real_normed_div_algebra})"
  by (rule conv_radius_geI_ex')
     (auto simp: algebra_simps intro!: summable_add summable_in_conv_radius)

lemma conv_radius_mult_ge:
  fixes f g :: "nat ==> ('a :: {banach,real_normed_div_algebra})"
  shows "conv_radius (λx. ∑i≤x. f i * g (x - i)) ≥ min (conv_radius f) (conv_radius g)"
proof (rule conv_radius_geI_ex')
  fix r assume r: "r > 0" "ereal r < min (conv_radius f) (conv_radius g)"
  from r have "summable (λn. (∑i≤n. (f i * of_real r^i) * (g (n - i) * of_real r^(n - i))))"
    by (intro summable_Cauchy_product abs_summable_in_conv_radius) simp_all
  thus "summable (λn. (∑i≤n. f i * g (n - i)) * of_real r ^ n)"
    by (simp add: algebra_simps of_real_def power_add [symmetric] scaleR_sum_right)
qed

lemma le_conv_radius_iff:
  fixes a :: "nat ==> 'a::{real_normed_div_algebra,banach}"
  shows "r ≤ conv_radius a ⟷ (∀x. norm (x-ξ) < r ⟶ summable (λi. a i * (x - ξ) ^ i))"
apply (intro iffI allI impI summable_in_conv_radius conv_radius_geI_ex)
apply (meson less_ereal.simps(1) not_le order_trans)
apply (rule_tac x="of_real ra" in exI, simp)
apply (metis abs_of_nonneg add_diff_cancel_left' less_eq_real_def norm_of_real)
done

end