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