src/HOL/Analysis/Summation_Tests.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (3 weeks ago)
changeset 69981 3dced198b9ec
parent 69597 ff784d5a5bfb
child 70097 4005298550a6
permissions -rw-r--r--
more strict AFP properties;
     1 (*  Title:    HOL/Analysis/Summation_Tests.thy
     2     Author:   Manuel Eberl, TU M√ľnchen
     3 *)
     4 
     5 section \<open>Radius of Convergence and Summation Tests\<close>
     6 
     7 theory Summation_Tests
     8 imports
     9   Complex_Main
    10   "HOL-Library.Discrete"
    11   "HOL-Library.Extended_Real"
    12   "HOL-Library.Liminf_Limsup"
    13   Extended_Real_Limits
    14 begin
    15 
    16 text \<open>
    17   The definition of the radius of convergence of a power series,
    18   various summability tests, lemmas to compute the radius of convergence etc.
    19 \<close>
    20 
    21 subsection \<open>Convergence tests for infinite sums\<close>
    22 
    23 subsubsection \<open>Root test\<close>
    24 
    25 lemma limsup_root_powser:
    26   fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
    27   shows "limsup (\<lambda>n. ereal (root n (norm (f n * z ^ n)))) =
    28              limsup (\<lambda>n. ereal (root n (norm (f n)))) * ereal (norm z)"
    29 proof -
    30   have A: "(\<lambda>n. ereal (root n (norm (f n * z ^ n)))) =
    31               (\<lambda>n. ereal (root n (norm (f n))) * ereal (norm z))" (is "?g = ?h")
    32   proof
    33     fix n show "?g n = ?h n"
    34     by (cases "n = 0") (simp_all add: norm_mult real_root_mult real_root_pos2 norm_power)
    35   qed
    36   show ?thesis by (subst A, subst limsup_ereal_mult_right) simp_all
    37 qed
    38 
    39 lemma limsup_root_limit:
    40   assumes "(\<lambda>n. ereal (root n (norm (f n)))) \<longlonglongrightarrow> l" (is "?g \<longlonglongrightarrow> _")
    41   shows   "limsup (\<lambda>n. ereal (root n (norm (f n)))) = l"
    42 proof -
    43   from assms have "convergent ?g" "lim ?g = l"
    44     unfolding convergent_def by (blast intro: limI)+
    45   with convergent_limsup_cl show ?thesis by force
    46 qed
    47 
    48 lemma limsup_root_limit':
    49   assumes "(\<lambda>n. root n (norm (f n))) \<longlonglongrightarrow> l"
    50   shows   "limsup (\<lambda>n. ereal (root n (norm (f n)))) = ereal l"
    51   by (intro limsup_root_limit tendsto_ereal assms)
    52 
    53 theorem root_test_convergence':
    54   fixes f :: "nat \<Rightarrow> 'a :: banach"
    55   defines "l \<equiv> limsup (\<lambda>n. ereal (root n (norm (f n))))"
    56   assumes l: "l < 1"
    57   shows   "summable f"
    58 proof -
    59   have "0 = limsup (\<lambda>n. 0)" by (simp add: Limsup_const)
    60   also have "... \<le> l" unfolding l_def by (intro Limsup_mono) (simp_all add: real_root_ge_zero)
    61   finally have "l \<ge> 0" by simp
    62   with l obtain l' where l': "l = ereal l'" by (cases l) simp_all
    63 
    64   define c where "c = (1 - l') / 2"
    65   from l and \<open>l \<ge> 0\<close> have c: "l + c > l" "l' + c \<ge> 0" "l' + c < 1" unfolding c_def
    66     by (simp_all add: field_simps l')
    67   have "\<forall>C>l. eventually (\<lambda>n. ereal (root n (norm (f n))) < C) sequentially"
    68     by (subst Limsup_le_iff[symmetric]) (simp add: l_def)
    69   with c have "eventually (\<lambda>n. ereal (root n (norm (f n))) < l + ereal c) sequentially" by simp
    70   with eventually_gt_at_top[of "0::nat"]
    71     have "eventually (\<lambda>n. norm (f n) \<le> (l' + c) ^ n) sequentially"
    72   proof eventually_elim
    73     fix n :: nat assume n: "n > 0"
    74     assume "ereal (root n (norm (f n))) < l + ereal c"
    75     hence "root n (norm (f n)) \<le> l' + c" by (simp add: l')
    76     with c n have "root n (norm (f n)) ^ n \<le> (l' + c) ^ n"
    77       by (intro power_mono) (simp_all add: real_root_ge_zero)
    78     also from n have "root n (norm (f n)) ^ n = norm (f n)" by simp
    79     finally show "norm (f n) \<le> (l' + c) ^ n" by simp
    80   qed
    81   thus ?thesis
    82     by (rule summable_comparison_test_ev[OF _ summable_geometric]) (simp add: c)
    83 qed
    84 
    85 theorem root_test_divergence:
    86   fixes f :: "nat \<Rightarrow> 'a :: banach"
    87   defines "l \<equiv> limsup (\<lambda>n. ereal (root n (norm (f n))))"
    88   assumes l: "l > 1"
    89   shows   "\<not>summable f"
    90 proof
    91   assume "summable f"
    92   hence bounded: "Bseq f" by (simp add: summable_imp_Bseq)
    93 
    94   have "0 = limsup (\<lambda>n. 0)" by (simp add: Limsup_const)
    95   also have "... \<le> l" unfolding l_def by (intro Limsup_mono) (simp_all add: real_root_ge_zero)
    96   finally have l_nonneg: "l \<ge> 0" by simp
    97 
    98   define c where "c = (if l = \<infinity> then 2 else 1 + (real_of_ereal l - 1) / 2)"
    99   from l l_nonneg consider "l = \<infinity>" | "\<exists>l'. l = ereal l'" by (cases l) simp_all
   100   hence c: "c > 1 \<and> ereal c < l" by cases (insert l, auto simp: c_def field_simps)
   101 
   102   have unbounded: "\<not>bdd_above {n. root n (norm (f n)) > c}"
   103   proof
   104     assume "bdd_above {n. root n (norm (f n)) > c}"
   105     then obtain N where "\<forall>n. root n (norm (f n)) > c \<longrightarrow> n \<le> N" unfolding bdd_above_def by blast
   106     hence "\<exists>N. \<forall>n\<ge>N. root n (norm (f n)) \<le> c"
   107       by (intro exI[of _ "N + 1"]) (force simp: not_less_eq_eq[symmetric])
   108     hence "eventually (\<lambda>n. root n (norm (f n)) \<le> c) sequentially"
   109       by (auto simp: eventually_at_top_linorder)
   110     hence "l \<le> c" unfolding l_def by (intro Limsup_bounded) simp_all
   111     with c show False by auto
   112   qed
   113 
   114   from bounded obtain K where K: "K > 0" "\<And>n. norm (f n) \<le> K" using BseqE by blast
   115   define n where "n = nat \<lceil>log c K\<rceil>"
   116   from unbounded have "\<exists>m>n. c < root m (norm (f m))" unfolding bdd_above_def
   117     by (auto simp: not_le)
   118   then guess m by (elim exE conjE) note m = this
   119   from c K have "K = c powr log c K" by (simp add: powr_def log_def)
   120   also from c have "c powr log c K \<le> c powr real n" unfolding n_def
   121     by (intro powr_mono, linarith, simp)
   122   finally have "K \<le> c ^ n" using c by (simp add: powr_realpow)
   123   also from c m have "c ^ n < c ^ m" by simp
   124   also from c m have "c ^ m < root m (norm (f m)) ^ m" by (intro power_strict_mono) simp_all
   125   also from m have "... = norm (f m)" by simp
   126   finally show False using K(2)[of m]  by simp
   127 qed
   128 
   129 
   130 subsubsection \<open>Cauchy's condensation test\<close>
   131 
   132 context
   133 fixes f :: "nat \<Rightarrow> real"
   134 begin
   135 
   136 private lemma condensation_inequality:
   137   assumes mono: "\<And>m n. 0 < m \<Longrightarrow> m \<le> n \<Longrightarrow> f n \<le> f m"
   138   shows   "(\<Sum>k=1..<n. f k) \<ge> (\<Sum>k=1..<n. f (2 * 2 ^ Discrete.log k))" (is "?thesis1")
   139           "(\<Sum>k=1..<n. f k) \<le> (\<Sum>k=1..<n. f (2 ^ Discrete.log k))" (is "?thesis2")
   140   by (intro sum_mono mono Discrete.log_exp2_ge Discrete.log_exp2_le, simp, simp)+
   141 
   142 private lemma condensation_condense1: "(\<Sum>k=1..<2^n. f (2 ^ Discrete.log k)) = (\<Sum>k<n. 2^k * f (2 ^ k))"
   143 proof (induction n)
   144   case (Suc n)
   145   have "{1..<2^Suc n} = {1..<2^n} \<union> {2^n..<(2^Suc n :: nat)}" by auto
   146   also have "(\<Sum>k\<in>\<dots>. f (2 ^ Discrete.log k)) =
   147                  (\<Sum>k<n. 2^k * f (2^k)) + (\<Sum>k = 2^n..<2^Suc n. f (2^Discrete.log k))"
   148     by (subst sum.union_disjoint) (insert Suc, auto)
   149   also have "Discrete.log k = n" if "k \<in> {2^n..<2^Suc n}" for k using that by (intro Discrete.log_eqI) simp_all
   150   hence "(\<Sum>k = 2^n..<2^Suc n. f (2^Discrete.log k)) = (\<Sum>(_::nat) = 2^n..<2^Suc n. f (2^n))"
   151     by (intro sum.cong) simp_all
   152   also have "\<dots> = 2^n * f (2^n)" by (simp add: of_nat_power)
   153   finally show ?case by simp
   154 qed simp
   155 
   156 private lemma condensation_condense2: "(\<Sum>k=1..<2^n. f (2 * 2 ^ Discrete.log k)) = (\<Sum>k<n. 2^k * f (2 ^ Suc k))"
   157 proof (induction n)
   158   case (Suc n)
   159   have "{1..<2^Suc n} = {1..<2^n} \<union> {2^n..<(2^Suc n :: nat)}" by auto
   160   also have "(\<Sum>k\<in>\<dots>. f (2 * 2 ^ Discrete.log k)) =
   161                  (\<Sum>k<n. 2^k * f (2^Suc k)) + (\<Sum>k = 2^n..<2^Suc n. f (2 * 2^Discrete.log k))"
   162     by (subst sum.union_disjoint) (insert Suc, auto)
   163   also have "Discrete.log k = n" if "k \<in> {2^n..<2^Suc n}" for k using that by (intro Discrete.log_eqI) simp_all
   164   hence "(\<Sum>k = 2^n..<2^Suc n. f (2*2^Discrete.log k)) = (\<Sum>(_::nat) = 2^n..<2^Suc n. f (2^Suc n))"
   165     by (intro sum.cong) simp_all
   166   also have "\<dots> = 2^n * f (2^Suc n)" by (simp add: of_nat_power)
   167   finally show ?case by simp
   168 qed simp
   169 
   170 theorem condensation_test:
   171   assumes mono: "\<And>m. 0 < m \<Longrightarrow> f (Suc m) \<le> f m"
   172   assumes nonneg: "\<And>n. f n \<ge> 0"
   173   shows "summable f \<longleftrightarrow> summable (\<lambda>n. 2^n * f (2^n))"
   174 proof -
   175   define f' where "f' n = (if n = 0 then 0 else f n)" for n
   176   from mono have mono': "decseq (\<lambda>n. f (Suc n))" by (intro decseq_SucI) simp
   177   hence mono': "f n \<le> f m" if "m \<le> n" "m > 0" for m n
   178     using that decseqD[OF mono', of "m - 1" "n - 1"] by simp
   179 
   180   have "(\<lambda>n. f (Suc n)) = (\<lambda>n. f' (Suc n))" by (intro ext) (simp add: f'_def)
   181   hence "summable f \<longleftrightarrow> summable f'"
   182     by (subst (1 2) summable_Suc_iff [symmetric]) (simp only:)
   183   also have "\<dots> \<longleftrightarrow> convergent (\<lambda>n. \<Sum>k<n. f' k)" unfolding summable_iff_convergent ..
   184   also have "monoseq (\<lambda>n. \<Sum>k<n. f' k)" unfolding f'_def
   185     by (intro mono_SucI1) (auto intro!: mult_nonneg_nonneg nonneg)
   186   hence "convergent (\<lambda>n. \<Sum>k<n. f' k) \<longleftrightarrow> Bseq (\<lambda>n. \<Sum>k<n. f' k)"
   187     by (rule monoseq_imp_convergent_iff_Bseq)
   188   also have "\<dots> \<longleftrightarrow> Bseq (\<lambda>n. \<Sum>k=1..<n. f' k)" unfolding One_nat_def
   189     by (subst sum_shift_lb_Suc0_0_upt) (simp_all add: f'_def atLeast0LessThan)
   190   also have "\<dots> \<longleftrightarrow> Bseq (\<lambda>n. \<Sum>k=1..<n. f k)" unfolding f'_def by simp
   191   also have "\<dots> \<longleftrightarrow> Bseq (\<lambda>n. \<Sum>k=1..<2^n. f k)"
   192     by (rule nonneg_incseq_Bseq_subseq_iff[symmetric])
   193        (auto intro!: sum_nonneg incseq_SucI nonneg simp: strict_mono_def)
   194   also have "\<dots> \<longleftrightarrow> Bseq (\<lambda>n. \<Sum>k<n. 2^k * f (2^k))"
   195   proof (intro iffI)
   196     assume A: "Bseq (\<lambda>n. \<Sum>k=1..<2^n. f k)"
   197     have "eventually (\<lambda>n. norm (\<Sum>k<n. 2^k * f (2^Suc k)) \<le> norm (\<Sum>k=1..<2^n. f k)) sequentially"
   198     proof (intro always_eventually allI)
   199       fix n :: nat
   200       have "norm (\<Sum>k<n. 2^k * f (2^Suc k)) = (\<Sum>k<n. 2^k * f (2^Suc k))" unfolding real_norm_def
   201         by (intro abs_of_nonneg sum_nonneg ballI mult_nonneg_nonneg nonneg) simp_all
   202       also have "\<dots> \<le> (\<Sum>k=1..<2^n. f k)"
   203         by (subst condensation_condense2 [symmetric]) (intro condensation_inequality mono')
   204       also have "\<dots> = norm \<dots>" unfolding real_norm_def
   205         by (intro abs_of_nonneg[symmetric] sum_nonneg ballI mult_nonneg_nonneg nonneg)
   206       finally show "norm (\<Sum>k<n. 2 ^ k * f (2 ^ Suc k)) \<le> norm (\<Sum>k=1..<2^n. f k)" .
   207     qed
   208     from this and A have "Bseq (\<lambda>n. \<Sum>k<n. 2^k * f (2^Suc k))" by (rule Bseq_eventually_mono)
   209     from Bseq_mult[OF Bfun_const[of 2] this] have "Bseq (\<lambda>n. \<Sum>k<n. 2^Suc k * f (2^Suc k))"
   210       by (simp add: sum_distrib_left sum_distrib_right mult_ac)
   211     hence "Bseq (\<lambda>n. (\<Sum>k=Suc 0..<Suc n. 2^k * f (2^k)) + f 1)"
   212       by (intro Bseq_add, subst sum_shift_bounds_Suc_ivl) (simp add: atLeast0LessThan)
   213     hence "Bseq (\<lambda>n. (\<Sum>k=0..<Suc n. 2^k * f (2^k)))"
   214       by (subst sum_head_upt_Suc) (simp_all add: add_ac)
   215     thus "Bseq (\<lambda>n. (\<Sum>k<n. 2^k * f (2^k)))"
   216       by (subst (asm) Bseq_Suc_iff) (simp add: atLeast0LessThan)
   217   next
   218     assume A: "Bseq (\<lambda>n. (\<Sum>k<n. 2^k * f (2^k)))"
   219     have "eventually (\<lambda>n. norm (\<Sum>k=1..<2^n. f k) \<le> norm (\<Sum>k<n. 2^k * f (2^k))) sequentially"
   220     proof (intro always_eventually allI)
   221       fix n :: nat
   222       have "norm (\<Sum>k=1..<2^n. f k) = (\<Sum>k=1..<2^n. f k)" unfolding real_norm_def
   223         by (intro abs_of_nonneg sum_nonneg ballI mult_nonneg_nonneg nonneg)
   224       also have "\<dots> \<le> (\<Sum>k<n. 2^k * f (2^k))"
   225         by (subst condensation_condense1 [symmetric]) (intro condensation_inequality mono')
   226       also have "\<dots> = norm \<dots>" unfolding real_norm_def
   227         by (intro abs_of_nonneg [symmetric] sum_nonneg ballI mult_nonneg_nonneg nonneg) simp_all
   228       finally show "norm (\<Sum>k=1..<2^n. f k) \<le> norm (\<Sum>k<n. 2^k * f (2^k))" .
   229     qed
   230     from this and A show "Bseq (\<lambda>n. \<Sum>k=1..<2^n. f k)" by (rule Bseq_eventually_mono)
   231   qed
   232   also have "monoseq (\<lambda>n. (\<Sum>k<n. 2^k * f (2^k)))"
   233     by (intro mono_SucI1) (auto intro!: mult_nonneg_nonneg nonneg)
   234   hence "Bseq (\<lambda>n. (\<Sum>k<n. 2^k * f (2^k))) \<longleftrightarrow> convergent (\<lambda>n. (\<Sum>k<n. 2^k * f (2^k)))"
   235     by (rule monoseq_imp_convergent_iff_Bseq [symmetric])
   236   also have "\<dots> \<longleftrightarrow> summable (\<lambda>k. 2^k * f (2^k))" by (simp only: summable_iff_convergent)
   237   finally show ?thesis .
   238 qed
   239 
   240 end
   241 
   242 
   243 subsubsection \<open>Summability of powers\<close>
   244 
   245 lemma abs_summable_complex_powr_iff:
   246     "summable (\<lambda>n. norm (exp (of_real (ln (of_nat n)) * s))) \<longleftrightarrow> Re s < -1"
   247 proof (cases "Re s \<le> 0")
   248   let ?l = "\<lambda>n. complex_of_real (ln (of_nat n))"
   249   case False
   250   have "eventually (\<lambda>n. norm (1 :: real) \<le> norm (exp (?l n * s))) sequentially"
   251     apply (rule eventually_mono [OF eventually_gt_at_top[of "0::nat"]])
   252     using False ge_one_powr_ge_zero by auto
   253   from summable_comparison_test_ev[OF this] False show ?thesis by (auto simp: summable_const_iff)
   254 next
   255   let ?l = "\<lambda>n. complex_of_real (ln (of_nat n))"
   256   case True
   257   hence "summable (\<lambda>n. norm (exp (?l n * s))) \<longleftrightarrow> summable (\<lambda>n. 2^n * norm (exp (?l (2^n) * s)))"
   258     by (intro condensation_test) (auto intro!: mult_right_mono_neg)
   259   also have "(\<lambda>n. 2^n * norm (exp (?l (2^n) * s))) = (\<lambda>n. (2 powr (Re s + 1)) ^ n)"
   260   proof
   261     fix n :: nat
   262     have "2^n * norm (exp (?l (2^n) * s)) = exp (real n * ln 2) * exp (real n * ln 2 * Re s)"
   263       using True by (subst exp_of_nat_mult) (simp add: ln_realpow algebra_simps)
   264     also have "\<dots> = exp (real n * (ln 2 * (Re s + 1)))"
   265       by (simp add: algebra_simps exp_add)
   266     also have "\<dots> = exp (ln 2 * (Re s + 1)) ^ n" by (subst exp_of_nat_mult) simp
   267     also have "exp (ln 2 * (Re s + 1)) = 2 powr (Re s + 1)" by (simp add: powr_def)
   268     finally show "2^n * norm (exp (?l (2^n) * s)) = (2 powr (Re s + 1)) ^ n" .
   269   qed
   270   also have "summable \<dots> \<longleftrightarrow> 2 powr (Re s + 1) < 2 powr 0"
   271     by (subst summable_geometric_iff) simp
   272   also have "\<dots> \<longleftrightarrow> Re s < -1" by (subst powr_less_cancel_iff) (simp, linarith)
   273   finally show ?thesis .
   274 qed
   275 
   276 theorem summable_complex_powr_iff:
   277   assumes "Re s < -1"
   278   shows   "summable (\<lambda>n. exp (of_real (ln (of_nat n)) * s))"
   279   by (rule summable_norm_cancel, subst abs_summable_complex_powr_iff) fact
   280 
   281 lemma summable_real_powr_iff: "summable (\<lambda>n. of_nat n powr s :: real) \<longleftrightarrow> s < -1"
   282 proof -
   283   from eventually_gt_at_top[of "0::nat"]
   284     have "summable (\<lambda>n. of_nat n powr s) \<longleftrightarrow> summable (\<lambda>n. exp (ln (of_nat n) * s))"
   285     by (intro summable_cong) (auto elim!: eventually_mono simp: powr_def)
   286   also have "\<dots> \<longleftrightarrow> s < -1" using abs_summable_complex_powr_iff[of "of_real s"] by simp
   287   finally show ?thesis .
   288 qed
   289 
   290 lemma inverse_power_summable:
   291   assumes s: "s \<ge> 2"
   292   shows "summable (\<lambda>n. inverse (of_nat n ^ s :: 'a :: {real_normed_div_algebra,banach}))"
   293 proof (rule summable_norm_cancel, subst summable_cong)
   294   from eventually_gt_at_top[of "0::nat"]
   295     show "eventually (\<lambda>n. norm (inverse (of_nat n ^ s:: 'a)) = real_of_nat n powr (-real s)) at_top"
   296     by eventually_elim (simp add: norm_inverse norm_power powr_minus powr_realpow)
   297 qed (insert s summable_real_powr_iff[of "-s"], simp_all)
   298 
   299 lemma not_summable_harmonic: "\<not>summable (\<lambda>n. inverse (of_nat n) :: 'a :: real_normed_field)"
   300 proof
   301   assume "summable (\<lambda>n. inverse (of_nat n) :: 'a)"
   302   hence "convergent (\<lambda>n. norm (of_real (\<Sum>k<n. inverse (of_nat k)) :: 'a))"
   303     by (simp add: summable_iff_convergent convergent_norm)
   304   hence "convergent (\<lambda>n. abs (\<Sum>k<n. inverse (of_nat k)) :: real)" by (simp only: norm_of_real)
   305   also have "(\<lambda>n. abs (\<Sum>k<n. inverse (of_nat k)) :: real) = (\<lambda>n. \<Sum>k<n. inverse (of_nat k))"
   306     by (intro ext abs_of_nonneg sum_nonneg) auto
   307   also have "convergent \<dots> \<longleftrightarrow> summable (\<lambda>k. inverse (of_nat k) :: real)"
   308     by (simp add: summable_iff_convergent)
   309   finally show False using summable_real_powr_iff[of "-1"] by (simp add: powr_minus)
   310 qed
   311 
   312 
   313 subsubsection \<open>Kummer's test\<close>
   314 
   315 theorem kummers_test_convergence:
   316   fixes f p :: "nat \<Rightarrow> real"
   317   assumes pos_f: "eventually (\<lambda>n. f n > 0) sequentially"
   318   assumes nonneg_p: "eventually (\<lambda>n. p n \<ge> 0) sequentially"
   319   defines "l \<equiv> liminf (\<lambda>n. ereal (p n * f n / f (Suc n) - p (Suc n)))"
   320   assumes l: "l > 0"
   321   shows   "summable f"
   322   unfolding summable_iff_convergent'
   323 proof -
   324   define r where "r = (if l = \<infinity> then 1 else real_of_ereal l / 2)"
   325   from l have "r > 0 \<and> of_real r < l" by (cases l) (simp_all add: r_def)
   326   hence r: "r > 0" "of_real r < l" by simp_all
   327   hence "eventually (\<lambda>n. p n * f n / f (Suc n) - p (Suc n) > r) sequentially"
   328     unfolding l_def by (force dest: less_LiminfD)
   329   moreover from pos_f have "eventually (\<lambda>n. f (Suc n) > 0) sequentially"
   330     by (subst eventually_sequentially_Suc)
   331   ultimately have "eventually (\<lambda>n. p n * f n - p (Suc n) * f (Suc n) > r * f (Suc n)) sequentially"
   332     by eventually_elim (simp add: field_simps)
   333   from eventually_conj[OF pos_f eventually_conj[OF nonneg_p this]]
   334     obtain m where m: "\<And>n. n \<ge> m \<Longrightarrow> f n > 0" "\<And>n. n \<ge> m \<Longrightarrow> p n \<ge> 0"
   335         "\<And>n. n \<ge> m \<Longrightarrow> p n * f n - p (Suc n) * f (Suc n) > r * f (Suc n)"
   336     unfolding eventually_at_top_linorder by blast
   337 
   338   let ?c = "(norm (\<Sum>k\<le>m. r * f k) + p m * f m) / r"
   339   have "Bseq (\<lambda>n. (\<Sum>k\<le>n + Suc m. f k))"
   340   proof (rule BseqI')
   341     fix k :: nat
   342     define n where "n = k + Suc m"
   343     have n: "n > m" by (simp add: n_def)
   344 
   345     from r have "r * norm (\<Sum>k\<le>n. f k) = norm (\<Sum>k\<le>n. r * f k)"
   346       by (simp add: sum_distrib_left[symmetric] abs_mult)
   347     also from n have "{..n} = {..m} \<union> {Suc m..n}" by auto
   348     hence "(\<Sum>k\<le>n. r * f k) = (\<Sum>k\<in>{..m} \<union> {Suc m..n}. r * f k)" by (simp only:)
   349     also have "\<dots> = (\<Sum>k\<le>m. r * f k) + (\<Sum>k=Suc m..n. r * f k)"
   350       by (subst sum.union_disjoint) auto
   351     also have "norm \<dots> \<le> norm (\<Sum>k\<le>m. r * f k) + norm (\<Sum>k=Suc m..n. r * f k)"
   352       by (rule norm_triangle_ineq)
   353     also from r less_imp_le[OF m(1)] have "(\<Sum>k=Suc m..n. r * f k) \<ge> 0"
   354       by (intro sum_nonneg) auto
   355     hence "norm (\<Sum>k=Suc m..n. r * f k) = (\<Sum>k=Suc m..n. r * f k)" by simp
   356     also have "(\<Sum>k=Suc m..n. r * f k) = (\<Sum>k=m..<n. r * f (Suc k))"
   357      by (subst sum_shift_bounds_Suc_ivl [symmetric])
   358           (simp only: atLeastLessThanSuc_atLeastAtMost)
   359     also from m have "\<dots> \<le> (\<Sum>k=m..<n. p k * f k - p (Suc k) * f (Suc k))"
   360       by (intro sum_mono[OF less_imp_le]) simp_all
   361     also have "\<dots> = -(\<Sum>k=m..<n. p (Suc k) * f (Suc k) - p k * f k)"
   362       by (simp add: sum_negf [symmetric] algebra_simps)
   363     also from n have "\<dots> = p m * f m - p n * f n"
   364       by (cases n, simp, simp only: atLeastLessThanSuc_atLeastAtMost, subst sum_Suc_diff) simp_all
   365     also from less_imp_le[OF m(1)] m(2) n have "\<dots> \<le> p m * f m" by simp
   366     finally show "norm (\<Sum>k\<le>n. f k) \<le> (norm (\<Sum>k\<le>m. r * f k) + p m * f m) / r" using r
   367       by (subst pos_le_divide_eq[OF r(1)]) (simp only: mult_ac)
   368   qed
   369   moreover have "(\<Sum>k\<le>n. f k) \<le> (\<Sum>k\<le>n'. f k)" if "Suc m \<le> n" "n \<le> n'" for n n'
   370     using less_imp_le[OF m(1)] that by (intro sum_mono2) auto
   371   ultimately show "convergent (\<lambda>n. \<Sum>k\<le>n. f k)" by (rule Bseq_monoseq_convergent'_inc)
   372 qed
   373 
   374 
   375 theorem kummers_test_divergence:
   376   fixes f p :: "nat \<Rightarrow> real"
   377   assumes pos_f: "eventually (\<lambda>n. f n > 0) sequentially"
   378   assumes pos_p: "eventually (\<lambda>n. p n > 0) sequentially"
   379   assumes divergent_p: "\<not>summable (\<lambda>n. inverse (p n))"
   380   defines "l \<equiv> limsup (\<lambda>n. ereal (p n * f n / f (Suc n) - p (Suc n)))"
   381   assumes l: "l < 0"
   382   shows   "\<not>summable f"
   383 proof
   384   assume "summable f"
   385   from eventually_conj[OF pos_f eventually_conj[OF pos_p Limsup_lessD[OF l[unfolded l_def]]]]
   386     obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> p n > 0" "\<And>n. n \<ge> N \<Longrightarrow> f n > 0"
   387                       "\<And>n. n \<ge> N \<Longrightarrow> p n * f n / f (Suc n) - p (Suc n) < 0"
   388     by (auto simp: eventually_at_top_linorder)
   389   hence A: "p n * f n < p (Suc n) * f (Suc n)" if "n \<ge> N" for n using that N[of n] N[of "Suc n"]
   390     by (simp add: field_simps)
   391   have B: "p n * f n \<ge> p N * f N" if "n \<ge> N" for n using that and A
   392     by (induction n rule: dec_induct) (auto intro!: less_imp_le elim!: order.trans)
   393   have "eventually (\<lambda>n. norm (p N * f N * inverse (p n)) \<le> f n) sequentially"
   394     apply (rule eventually_mono [OF eventually_ge_at_top[of N]])
   395     using B N  by (auto  simp: field_simps abs_of_pos)
   396   from this and \<open>summable f\<close> have "summable (\<lambda>n. p N * f N * inverse (p n))"
   397     by (rule summable_comparison_test_ev)
   398   from summable_mult[OF this, of "inverse (p N * f N)"] N[OF le_refl]
   399     have "summable (\<lambda>n. inverse (p n))" by (simp add: divide_simps)
   400   with divergent_p show False by contradiction
   401 qed
   402 
   403 
   404 subsubsection \<open>Ratio test\<close>
   405 
   406 theorem ratio_test_convergence:
   407   fixes f :: "nat \<Rightarrow> real"
   408   assumes pos_f: "eventually (\<lambda>n. f n > 0) sequentially"
   409   defines "l \<equiv> liminf (\<lambda>n. ereal (f n / f (Suc n)))"
   410   assumes l: "l > 1"
   411   shows   "summable f"
   412 proof (rule kummers_test_convergence[OF pos_f])
   413   note l
   414   also have "l = liminf (\<lambda>n. ereal (f n / f (Suc n) - 1)) + 1"
   415     by (subst Liminf_add_ereal_right[symmetric]) (simp_all add: minus_ereal_def l_def one_ereal_def)
   416   finally show "liminf (\<lambda>n. ereal (1 * f n / f (Suc n) - 1)) > 0"
   417     by (cases "liminf (\<lambda>n. ereal (1 * f n / f (Suc n) - 1))") simp_all
   418 qed simp
   419 
   420 theorem ratio_test_divergence:
   421   fixes f :: "nat \<Rightarrow> real"
   422   assumes pos_f: "eventually (\<lambda>n. f n > 0) sequentially"
   423   defines "l \<equiv> limsup (\<lambda>n. ereal (f n / f (Suc n)))"
   424   assumes l: "l < 1"
   425   shows   "\<not>summable f"
   426 proof (rule kummers_test_divergence[OF pos_f])
   427   have "limsup (\<lambda>n. ereal (f n / f (Suc n) - 1)) + 1 = l"
   428     by (subst Limsup_add_ereal_right[symmetric]) (simp_all add: minus_ereal_def l_def one_ereal_def)
   429   also note l
   430   finally show "limsup (\<lambda>n. ereal (1 * f n / f (Suc n) - 1)) < 0"
   431     by (cases "limsup (\<lambda>n. ereal (1 * f n / f (Suc n) - 1))") simp_all
   432 qed (simp_all add: summable_const_iff)
   433 
   434 
   435 subsubsection \<open>Raabe's test\<close>
   436 
   437 theorem raabes_test_convergence:
   438 fixes f :: "nat \<Rightarrow> real"
   439   assumes pos: "eventually (\<lambda>n. f n > 0) sequentially"
   440   defines "l \<equiv> liminf (\<lambda>n. ereal (of_nat n * (f n / f (Suc n) - 1)))"
   441   assumes l: "l > 1"
   442   shows   "summable f"
   443 proof (rule kummers_test_convergence)
   444   let ?l' = "liminf (\<lambda>n. ereal (of_nat n * f n / f (Suc n) - of_nat (Suc n)))"
   445   have "1 < l" by fact
   446   also have "l = liminf (\<lambda>n. ereal (of_nat n * f n / f (Suc n) - of_nat (Suc n)) + 1)"
   447     by (simp add: l_def algebra_simps)
   448   also have "\<dots> = ?l' + 1" by (subst Liminf_add_ereal_right) simp_all
   449   finally show "?l' > 0" by (cases ?l') (simp_all add: algebra_simps)
   450 qed (simp_all add: pos)
   451 
   452 theorem raabes_test_divergence:
   453 fixes f :: "nat \<Rightarrow> real"
   454   assumes pos: "eventually (\<lambda>n. f n > 0) sequentially"
   455   defines "l \<equiv> limsup (\<lambda>n. ereal (of_nat n * (f n / f (Suc n) - 1)))"
   456   assumes l: "l < 1"
   457   shows   "\<not>summable f"
   458 proof (rule kummers_test_divergence)
   459   let ?l' = "limsup (\<lambda>n. ereal (of_nat n * f n / f (Suc n) - of_nat (Suc n)))"
   460   note l
   461   also have "l = limsup (\<lambda>n. ereal (of_nat n * f n / f (Suc n) - of_nat (Suc n)) + 1)"
   462     by (simp add: l_def algebra_simps)
   463   also have "\<dots> = ?l' + 1" by (subst Limsup_add_ereal_right) simp_all
   464   finally show "?l' < 0" by (cases ?l') (simp_all add: algebra_simps)
   465 qed (insert pos eventually_gt_at_top[of "0::nat"] not_summable_harmonic, simp_all)
   466 
   467 
   468 subsection \<open>Radius of convergence\<close>
   469 
   470 text \<open>
   471   The radius of convergence of a power series. This value always exists, ranges from
   472   \<^term>\<open>0::ereal\<close> to \<^term>\<open>\<infinity>::ereal\<close>, and the power series is guaranteed to converge for
   473   all inputs with a norm that is smaller than that radius and to diverge for all inputs with a
   474   norm that is greater.
   475 \<close>
   476 definition%important conv_radius :: "(nat \<Rightarrow> 'a :: banach) \<Rightarrow> ereal" where
   477   "conv_radius f = inverse (limsup (\<lambda>n. ereal (root n (norm (f n)))))"
   478 
   479 lemma conv_radius_cong_weak [cong]: "(\<And>n. f n = g n) \<Longrightarrow> conv_radius f = conv_radius g"
   480   by (drule ext) simp_all
   481 
   482 lemma conv_radius_nonneg: "conv_radius f \<ge> 0"
   483 proof -
   484   have "0 = limsup (\<lambda>n. 0)" by (subst Limsup_const) simp_all
   485   also have "\<dots> \<le> limsup (\<lambda>n. ereal (root n (norm (f n))))"
   486     by (intro Limsup_mono) (simp_all add: real_root_ge_zero)
   487   finally show ?thesis
   488     unfolding conv_radius_def by (auto simp: ereal_inverse_nonneg_iff)
   489 qed
   490 
   491 lemma conv_radius_zero [simp]: "conv_radius (\<lambda>_. 0) = \<infinity>"
   492   by (auto simp: conv_radius_def zero_ereal_def [symmetric] Limsup_const)
   493 
   494 lemma conv_radius_altdef:
   495   "conv_radius f = liminf (\<lambda>n. inverse (ereal (root n (norm (f n)))))"
   496   by (subst Liminf_inverse_ereal) (simp_all add: real_root_ge_zero conv_radius_def)
   497 
   498 lemma conv_radius_cong':
   499   assumes "eventually (\<lambda>x. f x = g x) sequentially"
   500   shows   "conv_radius f = conv_radius g"
   501   unfolding conv_radius_altdef by (intro Liminf_eq eventually_mono [OF assms]) auto
   502 
   503 lemma conv_radius_cong:
   504   assumes "eventually (\<lambda>x. norm (f x) = norm (g x)) sequentially"
   505   shows   "conv_radius f = conv_radius g"
   506   unfolding conv_radius_altdef by (intro Liminf_eq eventually_mono [OF assms]) auto
   507 
   508 theorem abs_summable_in_conv_radius:
   509   fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   510   assumes "ereal (norm z) < conv_radius f"
   511   shows   "summable (\<lambda>n. norm (f n * z ^ n))"
   512 proof (rule root_test_convergence')
   513   define l where "l = limsup (\<lambda>n. ereal (root n (norm (f n))))"
   514   have "0 = limsup (\<lambda>n. 0)" by (simp add: Limsup_const)
   515   also have "... \<le> l" unfolding l_def by (intro Limsup_mono) (simp_all add: real_root_ge_zero)
   516   finally have l_nonneg: "l \<ge> 0" .
   517 
   518   have "limsup (\<lambda>n. root n (norm (f n * z^n))) = l * ereal (norm z)" unfolding l_def
   519     by (rule limsup_root_powser)
   520   also from l_nonneg consider "l = 0" | "l = \<infinity>" | "\<exists>l'. l = ereal l' \<and> l' > 0"
   521     by (cases "l") (auto simp: less_le)
   522   hence "l * ereal (norm z) < 1"
   523   proof cases
   524     assume "l = \<infinity>"
   525     hence "conv_radius f = 0" unfolding conv_radius_def l_def by simp
   526     with assms show ?thesis by simp
   527   next
   528     assume "\<exists>l'. l = ereal l' \<and> l' > 0"
   529     then guess l' by (elim exE conjE) note l' = this
   530     hence "l \<noteq> \<infinity>" by auto
   531     have "l * ereal (norm z) < l * conv_radius f"
   532       by (intro ereal_mult_strict_left_mono) (simp_all add: l' assms)
   533     also have "conv_radius f = inverse l" by (simp add: conv_radius_def l_def)
   534     also from l' have "l * inverse l = 1" by simp
   535     finally show ?thesis .
   536   qed simp_all
   537   finally show "limsup (\<lambda>n. ereal (root n (norm (norm (f n * z ^ n))))) < 1" by simp
   538 qed
   539 
   540 lemma summable_in_conv_radius:
   541   fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   542   assumes "ereal (norm z) < conv_radius f"
   543   shows   "summable (\<lambda>n. f n * z ^ n)"
   544   by (rule summable_norm_cancel, rule abs_summable_in_conv_radius) fact+
   545 
   546 theorem not_summable_outside_conv_radius:
   547   fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   548   assumes "ereal (norm z) > conv_radius f"
   549   shows   "\<not>summable (\<lambda>n. f n * z ^ n)"
   550 proof (rule root_test_divergence)
   551   define l where "l = limsup (\<lambda>n. ereal (root n (norm (f n))))"
   552   have "0 = limsup (\<lambda>n. 0)" by (simp add: Limsup_const)
   553   also have "... \<le> l" unfolding l_def by (intro Limsup_mono) (simp_all add: real_root_ge_zero)
   554   finally have l_nonneg: "l \<ge> 0" .
   555   from assms have l_nz: "l \<noteq> 0" unfolding conv_radius_def l_def by auto
   556 
   557   have "limsup (\<lambda>n. ereal (root n (norm (f n * z^n)))) = l * ereal (norm z)"
   558     unfolding l_def by (rule limsup_root_powser)
   559   also have "... > 1"
   560   proof (cases l)
   561     assume "l = \<infinity>"
   562     with assms conv_radius_nonneg[of f] show ?thesis
   563       by (auto simp: zero_ereal_def[symmetric])
   564   next
   565     fix l' assume l': "l = ereal l'"
   566     from l_nonneg l_nz have "1 = l * inverse l" by (auto simp: l' field_simps)
   567     also from l_nz have "inverse l = conv_radius f"
   568       unfolding l_def conv_radius_def by auto
   569     also from l' l_nz l_nonneg assms have "l * \<dots> < l * ereal (norm z)"
   570       by (intro ereal_mult_strict_left_mono) (auto simp: l')
   571     finally show ?thesis .
   572   qed (insert l_nonneg, simp_all)
   573   finally show "limsup (\<lambda>n. ereal (root n (norm (f n * z^n)))) > 1" .
   574 qed
   575 
   576 
   577 lemma conv_radius_geI:
   578   assumes "summable (\<lambda>n. f n * z ^ n :: 'a :: {banach, real_normed_div_algebra})"
   579   shows   "conv_radius f \<ge> norm z"
   580   using not_summable_outside_conv_radius[of f z] assms by (force simp: not_le[symmetric])
   581 
   582 lemma conv_radius_leI:
   583   assumes "\<not>summable (\<lambda>n. norm (f n * z ^ n :: 'a :: {banach, real_normed_div_algebra}))"
   584   shows   "conv_radius f \<le> norm z"
   585   using abs_summable_in_conv_radius[of z f] assms by (force simp: not_le[symmetric])
   586 
   587 lemma conv_radius_leI':
   588   assumes "\<not>summable (\<lambda>n. f n * z ^ n :: 'a :: {banach, real_normed_div_algebra})"
   589   shows   "conv_radius f \<le> norm z"
   590   using summable_in_conv_radius[of z f] assms by (force simp: not_le[symmetric])
   591 
   592 lemma conv_radius_geI_ex:
   593   fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   594   assumes "\<And>r. 0 < r \<Longrightarrow> ereal r < R \<Longrightarrow> \<exists>z. norm z = r \<and> summable (\<lambda>n. f n * z^n)"
   595   shows   "conv_radius f \<ge> R"
   596 proof (rule linorder_cases[of "conv_radius f" R])
   597   assume R: "conv_radius f < R"
   598   with conv_radius_nonneg[of f] obtain conv_radius'
   599     where [simp]: "conv_radius f = ereal conv_radius'"
   600     by (cases "conv_radius f") simp_all
   601   define r where "r = (if R = \<infinity> then conv_radius' + 1 else (real_of_ereal R + conv_radius') / 2)"
   602   from R conv_radius_nonneg[of f] have "0 < r \<and> ereal r < R \<and> ereal r > conv_radius f"
   603     unfolding r_def by (cases R) (auto simp: r_def field_simps)
   604   with assms(1)[of r] obtain z where "norm z > conv_radius f" "summable (\<lambda>n. f n * z^n)" by auto
   605   with not_summable_outside_conv_radius[of f z] show ?thesis by simp
   606 qed simp_all
   607 
   608 lemma conv_radius_geI_ex':
   609   fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   610   assumes "\<And>r. 0 < r \<Longrightarrow> ereal r < R \<Longrightarrow> summable (\<lambda>n. f n * of_real r^n)"
   611   shows   "conv_radius f \<ge> R"
   612 proof (rule conv_radius_geI_ex)
   613   fix r assume "0 < r" "ereal r < R"
   614   with assms[of r] show "\<exists>z. norm z = r \<and> summable (\<lambda>n. f n * z ^ n)"
   615     by (intro exI[of _ "of_real r :: 'a"]) auto
   616 qed
   617 
   618 lemma conv_radius_leI_ex:
   619   fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   620   assumes "R \<ge> 0"
   621   assumes "\<And>r. 0 < r \<Longrightarrow> ereal r > R \<Longrightarrow> \<exists>z. norm z = r \<and> \<not>summable (\<lambda>n. norm (f n * z^n))"
   622   shows   "conv_radius f \<le> R"
   623 proof (rule linorder_cases[of "conv_radius f" R])
   624   assume R: "conv_radius f > R"
   625   from R assms(1) obtain R' where R': "R = ereal R'" by (cases R) simp_all
   626   define r where
   627     "r = (if conv_radius f = \<infinity> then R' + 1 else (R' + real_of_ereal (conv_radius f)) / 2)"
   628   from R conv_radius_nonneg[of f] have "r > R \<and> r < conv_radius f" unfolding r_def
   629     by (cases "conv_radius f") (auto simp: r_def field_simps R')
   630   with assms(1) assms(2)[of r] R'
   631     obtain z where "norm z < conv_radius f" "\<not>summable (\<lambda>n. norm (f n * z^n))" by auto
   632   with abs_summable_in_conv_radius[of z f] show ?thesis by auto
   633 qed simp_all
   634 
   635 lemma conv_radius_leI_ex':
   636   fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   637   assumes "R \<ge> 0"
   638   assumes "\<And>r. 0 < r \<Longrightarrow> ereal r > R \<Longrightarrow> \<not>summable (\<lambda>n. f n * of_real r^n)"
   639   shows   "conv_radius f \<le> R"
   640 proof (rule conv_radius_leI_ex)
   641   fix r assume "0 < r" "ereal r > R"
   642   with assms(2)[of r] show "\<exists>z. norm z = r \<and> \<not>summable (\<lambda>n. norm (f n * z ^ n))"
   643     by (intro exI[of _ "of_real r :: 'a"]) (auto dest: summable_norm_cancel)
   644 qed fact+
   645 
   646 lemma conv_radius_eqI:
   647   fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   648   assumes "R \<ge> 0"
   649   assumes "\<And>r. 0 < r \<Longrightarrow> ereal r < R \<Longrightarrow> \<exists>z. norm z = r \<and> summable (\<lambda>n. f n * z^n)"
   650   assumes "\<And>r. 0 < r \<Longrightarrow> ereal r > R \<Longrightarrow> \<exists>z. norm z = r \<and> \<not>summable (\<lambda>n. norm (f n * z^n))"
   651   shows   "conv_radius f = R"
   652   by (intro antisym conv_radius_geI_ex conv_radius_leI_ex assms)
   653 
   654 lemma conv_radius_eqI':
   655   fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   656   assumes "R \<ge> 0"
   657   assumes "\<And>r. 0 < r \<Longrightarrow> ereal r < R \<Longrightarrow> summable (\<lambda>n. f n * (of_real r)^n)"
   658   assumes "\<And>r. 0 < r \<Longrightarrow> ereal r > R \<Longrightarrow> \<not>summable (\<lambda>n. norm (f n * (of_real r)^n))"
   659   shows   "conv_radius f = R"
   660 proof (intro conv_radius_eqI[OF assms(1)])
   661   fix r assume "0 < r" "ereal r < R" with assms(2)[OF this]
   662     show "\<exists>z. norm z = r \<and> summable (\<lambda>n. f n * z ^ n)" by force
   663 next
   664   fix r assume "0 < r" "ereal r > R" with assms(3)[OF this]
   665     show "\<exists>z. norm z = r \<and> \<not>summable (\<lambda>n. norm (f n * z ^ n))" by force
   666 qed
   667 
   668 lemma conv_radius_zeroI:
   669   fixes f :: "nat \<Rightarrow> 'a :: {banach,real_normed_div_algebra}"
   670   assumes "\<And>z. z \<noteq> 0 \<Longrightarrow> \<not>summable (\<lambda>n. f n * z^n)"
   671   shows   "conv_radius f = 0"
   672 proof (rule ccontr)
   673   assume "conv_radius f \<noteq> 0"
   674   with conv_radius_nonneg[of f] have pos: "conv_radius f > 0" by simp
   675   define r where "r = (if conv_radius f = \<infinity> then 1 else real_of_ereal (conv_radius f) / 2)"
   676   from pos have r: "ereal r > 0 \<and> ereal r < conv_radius f"
   677     by (cases "conv_radius f") (simp_all add: r_def)
   678   hence "summable (\<lambda>n. f n * of_real r ^ n)" by (intro summable_in_conv_radius) simp
   679   moreover from r and assms[of "of_real r"] have "\<not>summable (\<lambda>n. f n * of_real r ^ n)" by simp
   680   ultimately show False by contradiction
   681 qed
   682 
   683 lemma conv_radius_inftyI':
   684   fixes f :: "nat \<Rightarrow> 'a :: {banach,real_normed_div_algebra}"
   685   assumes "\<And>r. r > c \<Longrightarrow> \<exists>z. norm z = r \<and> summable (\<lambda>n. f n * z^n)"
   686   shows   "conv_radius f = \<infinity>"
   687 proof -
   688   {
   689     fix r :: real
   690     have "max r (c + 1) > c" by (auto simp: max_def)
   691     from assms[OF this] obtain z where "norm z = max r (c + 1)" "summable (\<lambda>n. f n * z^n)" by blast
   692     from conv_radius_geI[OF this(2)] this(1) have "conv_radius f \<ge> r" by simp
   693   }
   694   from this[of "real_of_ereal (conv_radius f + 1)"] show "conv_radius f = \<infinity>"
   695     by (cases "conv_radius f") simp_all
   696 qed
   697 
   698 lemma conv_radius_inftyI:
   699   fixes f :: "nat \<Rightarrow> 'a :: {banach,real_normed_div_algebra}"
   700   assumes "\<And>r. \<exists>z. norm z = r \<and> summable (\<lambda>n. f n * z^n)"
   701   shows   "conv_radius f = \<infinity>"
   702   using assms by (rule conv_radius_inftyI')
   703 
   704 lemma conv_radius_inftyI'':
   705   fixes f :: "nat \<Rightarrow> 'a :: {banach,real_normed_div_algebra}"
   706   assumes "\<And>z. summable (\<lambda>n. f n * z^n)"
   707   shows   "conv_radius f = \<infinity>"
   708 proof (rule conv_radius_inftyI')
   709   fix r :: real assume "r > 0"
   710   with assms show "\<exists>z. norm z = r \<and> summable (\<lambda>n. f n * z^n)"
   711     by (intro exI[of _ "of_real r"]) simp
   712 qed
   713 
   714 lemma conv_radius_conv_Sup:
   715   fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   716   shows "conv_radius f = Sup {r. \<forall>z. ereal (norm z) < r \<longrightarrow> summable (\<lambda>n. f n * z ^ n)}"
   717 proof (rule Sup_eqI [symmetric], goal_cases)
   718   case (1 r)
   719   thus ?case
   720     by (intro conv_radius_geI_ex') auto
   721 next
   722   case (2 r)
   723   from 2[of 0] have r: "r \<ge> 0" by auto
   724   show ?case
   725   proof (intro conv_radius_leI_ex' r)
   726     fix R assume R: "R > 0" "ereal R > r"
   727     with r obtain r' where [simp]: "r = ereal r'" by (cases r) auto
   728     show "\<not>summable (\<lambda>n. f n * of_real R ^ n)"
   729     proof
   730       assume *: "summable (\<lambda>n. f n * of_real R ^ n)"
   731       define R' where "R' = (R + r') / 2"
   732       from R have R': "R' > r'" "R' < R" by (simp_all add: R'_def)
   733       hence "\<forall>z. norm z < R' \<longrightarrow> summable (\<lambda>n. f n * z ^ n)"
   734         using powser_inside[OF *] by auto
   735       from 2[of R'] and this have "R' \<le> r'" by auto
   736       with \<open>R' > r'\<close> show False by simp
   737     qed
   738   qed
   739 qed
   740 
   741 lemma conv_radius_shift:
   742   fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   743   shows   "conv_radius (\<lambda>n. f (n + m)) = conv_radius f"
   744   unfolding conv_radius_conv_Sup summable_powser_ignore_initial_segment ..
   745 
   746 lemma conv_radius_norm [simp]: "conv_radius (\<lambda>x. norm (f x)) = conv_radius f"
   747   by (simp add: conv_radius_def)
   748 
   749 lemma conv_radius_ratio_limit_ereal:
   750   fixes f :: "nat \<Rightarrow> 'a :: {banach,real_normed_div_algebra}"
   751   assumes nz:  "eventually (\<lambda>n. f n \<noteq> 0) sequentially"
   752   assumes lim: "(\<lambda>n. ereal (norm (f n) / norm (f (Suc n)))) \<longlonglongrightarrow> c"
   753   shows   "conv_radius f = c"
   754 proof (rule conv_radius_eqI')
   755   show "c \<ge> 0" by (intro Lim_bounded2[OF lim]) simp_all
   756 next
   757   fix r assume r: "0 < r" "ereal r < c"
   758   let ?l = "liminf (\<lambda>n. ereal (norm (f n * of_real r ^ n) / norm (f (Suc n) * of_real r ^ Suc n)))"
   759   have "?l = liminf (\<lambda>n. ereal (norm (f n) / (norm (f (Suc n)))) * ereal (inverse r))"
   760     using r by (simp add: norm_mult norm_power divide_simps)
   761   also from r have "\<dots> = liminf (\<lambda>n. ereal (norm (f n) / (norm (f (Suc n))))) * ereal (inverse r)"
   762     by (intro Liminf_ereal_mult_right) simp_all
   763   also have "liminf (\<lambda>n. ereal (norm (f n) / (norm (f (Suc n))))) = c"
   764     by (intro lim_imp_Liminf lim) simp
   765   finally have l: "?l = c * ereal (inverse r)" by simp
   766   from r have  l': "c * ereal (inverse r) > 1" by (cases c) (simp_all add: field_simps)
   767   show "summable (\<lambda>n. f n * of_real r^n)"
   768     by (rule summable_norm_cancel, rule ratio_test_convergence)
   769        (insert r nz l l', auto elim!: eventually_mono)
   770 next
   771   fix r assume r: "0 < r" "ereal r > c"
   772   let ?l = "limsup (\<lambda>n. ereal (norm (f n * of_real r ^ n) / norm (f (Suc n) * of_real r ^ Suc n)))"
   773   have "?l = limsup (\<lambda>n. ereal (norm (f n) / (norm (f (Suc n)))) * ereal (inverse r))"
   774     using r by (simp add: norm_mult norm_power divide_simps)
   775   also from r have "\<dots> = limsup (\<lambda>n. ereal (norm (f n) / (norm (f (Suc n))))) * ereal (inverse r)"
   776     by (intro Limsup_ereal_mult_right) simp_all
   777   also have "limsup (\<lambda>n. ereal (norm (f n) / (norm (f (Suc n))))) = c"
   778     by (intro lim_imp_Limsup lim) simp
   779   finally have l: "?l = c * ereal (inverse r)" by simp
   780   from r have  l': "c * ereal (inverse r) < 1" by (cases c) (simp_all add: field_simps)
   781   show "\<not>summable (\<lambda>n. norm (f n * of_real r^n))"
   782     by (rule ratio_test_divergence) (insert r nz l l', auto elim!: eventually_mono)
   783 qed
   784 
   785 lemma conv_radius_ratio_limit_ereal_nonzero:
   786   fixes f :: "nat \<Rightarrow> 'a :: {banach,real_normed_div_algebra}"
   787   assumes nz:  "c \<noteq> 0"
   788   assumes lim: "(\<lambda>n. ereal (norm (f n) / norm (f (Suc n)))) \<longlonglongrightarrow> c"
   789   shows   "conv_radius f = c"
   790 proof (rule conv_radius_ratio_limit_ereal[OF _ lim], rule ccontr)
   791   assume "\<not>eventually (\<lambda>n. f n \<noteq> 0) sequentially"
   792   hence "frequently (\<lambda>n. f n = 0) sequentially" by (simp add: frequently_def)
   793   hence "frequently (\<lambda>n. ereal (norm (f n) / norm (f (Suc n))) = 0) sequentially"
   794     by (force elim!: frequently_elim1)
   795   hence "c = 0" by (intro limit_frequently_eq[OF _ _ lim]) auto
   796   with nz show False by contradiction
   797 qed
   798 
   799 lemma conv_radius_ratio_limit:
   800   fixes f :: "nat \<Rightarrow> 'a :: {banach,real_normed_div_algebra}"
   801   assumes "c' = ereal c"
   802   assumes nz:  "eventually (\<lambda>n. f n \<noteq> 0) sequentially"
   803   assumes lim: "(\<lambda>n. norm (f n) / norm (f (Suc n))) \<longlonglongrightarrow> c"
   804   shows   "conv_radius f = c'"
   805   using assms by (intro conv_radius_ratio_limit_ereal) simp_all
   806 
   807 lemma conv_radius_ratio_limit_nonzero:
   808   fixes f :: "nat \<Rightarrow> 'a :: {banach,real_normed_div_algebra}"
   809   assumes "c' = ereal c"
   810   assumes nz:  "c \<noteq> 0"
   811   assumes lim: "(\<lambda>n. norm (f n) / norm (f (Suc n))) \<longlonglongrightarrow> c"
   812   shows   "conv_radius f = c'"
   813   using assms by (intro conv_radius_ratio_limit_ereal_nonzero) simp_all
   814 
   815 lemma conv_radius_cmult_left:
   816   assumes "c \<noteq> (0 :: 'a :: {banach, real_normed_div_algebra})"
   817   shows   "conv_radius (\<lambda>n. c * f n) = conv_radius f"
   818 proof -
   819   have "conv_radius (\<lambda>n. c * f n) = 
   820           inverse (limsup (\<lambda>n. ereal (root n (norm (c * f n)))))"
   821     unfolding conv_radius_def ..
   822   also have "(\<lambda>n. ereal (root n (norm (c * f n)))) = 
   823                (\<lambda>n. ereal (root n (norm c)) * ereal (root n (norm (f n))))"
   824     by (rule ext) (auto simp: norm_mult real_root_mult)
   825   also have "limsup \<dots> = ereal 1 * limsup (\<lambda>n. ereal (root n (norm (f n))))"
   826     using assms by (intro ereal_limsup_lim_mult tendsto_ereal LIMSEQ_root_const) auto
   827   also have "inverse \<dots> = conv_radius f" by (simp add: conv_radius_def)
   828   finally show ?thesis .
   829 qed
   830 
   831 lemma conv_radius_cmult_right:
   832   assumes "c \<noteq> (0 :: 'a :: {banach, real_normed_div_algebra})"
   833   shows   "conv_radius (\<lambda>n. f n * c) = conv_radius f"
   834 proof -
   835   have "conv_radius (\<lambda>n. f n * c) = conv_radius (\<lambda>n. c * f n)"
   836     by (simp add: conv_radius_def norm_mult mult.commute)
   837   with conv_radius_cmult_left[OF assms, of f] show ?thesis by simp
   838 qed
   839 
   840 lemma conv_radius_mult_power:
   841   assumes "c \<noteq> (0 :: 'a :: {real_normed_div_algebra,banach})"
   842   shows   "conv_radius (\<lambda>n. c ^ n * f n) = conv_radius f / ereal (norm c)"
   843 proof -
   844   have "limsup (\<lambda>n. ereal (root n (norm (c ^ n * f n)))) =
   845           limsup (\<lambda>n. ereal (norm c) * ereal (root n (norm (f n))))"
   846     by (intro Limsup_eq eventually_mono [OF eventually_gt_at_top[of "0::nat"]])
   847        (auto simp: norm_mult norm_power real_root_mult real_root_power)
   848   also have "\<dots> = ereal (norm c) * limsup (\<lambda>n. ereal (root n (norm (f n))))"
   849     using assms by (subst Limsup_ereal_mult_left[symmetric]) simp_all
   850   finally have A: "limsup (\<lambda>n. ereal (root n (norm (c ^ n * f n)))) =
   851                        ereal (norm c) * limsup (\<lambda>n. ereal (root n (norm (f n))))" .
   852   show ?thesis using assms
   853     apply (cases "limsup (\<lambda>n. ereal (root n (norm (f n)))) = 0")
   854     apply (simp add: A conv_radius_def)
   855     apply (unfold conv_radius_def A divide_ereal_def, simp add: mult.commute ereal_inverse_mult)
   856     done
   857 qed
   858 
   859 lemma conv_radius_mult_power_right:
   860   assumes "c \<noteq> (0 :: 'a :: {real_normed_div_algebra,banach})"
   861   shows   "conv_radius (\<lambda>n. f n * c ^ n) = conv_radius f / ereal (norm c)"
   862   using conv_radius_mult_power[OF assms, of f]
   863   unfolding conv_radius_def by (simp add: mult.commute norm_mult)
   864 
   865 lemma conv_radius_divide_power:
   866   assumes "c \<noteq> (0 :: 'a :: {real_normed_div_algebra,banach})"
   867   shows   "conv_radius (\<lambda>n. f n / c^n) = conv_radius f * ereal (norm c)"
   868 proof -
   869   from assms have "inverse c \<noteq> 0" by simp
   870   from conv_radius_mult_power_right[OF this, of f] show ?thesis
   871     by (simp add: divide_inverse divide_ereal_def assms norm_inverse power_inverse)
   872 qed
   873 
   874 
   875 lemma conv_radius_add_ge:
   876   "min (conv_radius f) (conv_radius g) \<le>
   877        conv_radius (\<lambda>x. f x + g x :: 'a :: {banach,real_normed_div_algebra})"
   878   by (rule conv_radius_geI_ex')
   879      (auto simp: algebra_simps intro!: summable_add summable_in_conv_radius)
   880 
   881 lemma conv_radius_mult_ge:
   882   fixes f g :: "nat \<Rightarrow> ('a :: {banach,real_normed_div_algebra})"
   883   shows "conv_radius (\<lambda>x. \<Sum>i\<le>x. f i * g (x - i)) \<ge> min (conv_radius f) (conv_radius g)"
   884 proof (rule conv_radius_geI_ex')
   885   fix r assume r: "r > 0" "ereal r < min (conv_radius f) (conv_radius g)"
   886   from r have "summable (\<lambda>n. (\<Sum>i\<le>n. (f i * of_real r^i) * (g (n - i) * of_real r^(n - i))))"
   887     by (intro summable_Cauchy_product abs_summable_in_conv_radius) simp_all
   888   thus "summable (\<lambda>n. (\<Sum>i\<le>n. f i * g (n - i)) * of_real r ^ n)"
   889     by (simp add: algebra_simps of_real_def power_add [symmetric] scaleR_sum_right)
   890 qed
   891 
   892 lemma le_conv_radius_iff:
   893   fixes a :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
   894   shows "r \<le> conv_radius a \<longleftrightarrow> (\<forall>x. norm (x-\<xi>) < r \<longrightarrow> summable (\<lambda>i. a i * (x - \<xi>) ^ i))"
   895 apply (intro iffI allI impI summable_in_conv_radius conv_radius_geI_ex)
   896 apply (meson less_ereal.simps(1) not_le order_trans)
   897 apply (rule_tac x="of_real ra" in exI, simp)
   898 apply (metis abs_of_nonneg add_diff_cancel_left' less_eq_real_def norm_of_real)
   899 done
   900 
   901 end