Quelle Summation_Tests.thy Sprache: Isabelle

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

section \<open>Radius of Convergence and Summation Tests\<close>

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

text \<open>
  The definition of the radius of convergence of a power series,
  various summability tests, lemmas to compute the radius of convergence etc.
\<close>

subsection \<open>Convergence tests for infinite sums\<close>

subsubsection \<open>Root test\<close>

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 (\<lambda>n. ereal (root n (norm (f n)))) * ereal (norm z)"
proof -
  have A: "(\n. ereal (root n (norm (f n * z ^ n)))) =
              (\<lambda>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 \<open>l \<ge> 0\<close> have c: "l + c > l" "l' + c \<ge> 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 \<open>Cauchy's condensation test\<close>

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..
          "(\k=1.. (\k=1..
  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)) =
                 (\<Sum>k<n. 2^k * f (2^k)) + (\<Sum>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)) =
                 (\<Sum>k<n. 2^k * f (2^Suc k)) + (\<Sum>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
  also have "monoseq (\n. \k
    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..
    by (subst sum_shift_lb_Suc0_0_upt) (simp_all add: f'_def atLeast0LessThan)
  also have "\ \ Bseq (\n. \k=1..
  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 (\kk
        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
    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 \<open>Summability of powers\<close>

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
  also have "(\n. abs (\kn. \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 \<open>Kummer's test\<close>

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 \<open>summable f\<close> have "summable (\<lambda>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 \<open>Ratio test\<close>

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 \<open>Raabe's test\<close>

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 \<open>Radius of convergence\<close>

text \<open>
  The radius of convergence of a power series. This value always exists, ranges from
  \<^term>\<open>0::ereal\<close> to \<^term>\<open>\<infinity>::ereal\<close>, 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.
\<close>
definition\<^marker>\<open>tag important\<close> conv_radius :: "(nat \<Rightarrow> 'a :: banach) \<Rightarrow> 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' \<le> r'" by auto
      with \<open>R' > r'\<close> 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 (\<lambda>n. ereal (root n (norm (c * f n)))))"
    unfolding conv_radius_def ..
  also have "(\n. ereal (root n (norm (c * f n)))) =
               (\<lambda>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 (\<lambda>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 (\<lambda>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 (\<lambda>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

quality99%

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.