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