src/HOL/Analysis/Summation_Tests.thy
changeset 63627 6ddb43c6b711
parent 63594 bd218a9320b5
child 63918 6bf55e6e0b75
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Analysis/Summation_Tests.thy	Mon Aug 08 14:13:14 2016 +0200
     1.3 @@ -0,0 +1,920 @@
     1.4 +(*  Title:    HOL/Analysis/Summation.thy
     1.5 +    Author:   Manuel Eberl, TU M√ľnchen
     1.6 +*)
     1.7 +
     1.8 +section \<open>Radius of Convergence and Summation Tests\<close>
     1.9 +
    1.10 +theory Summation_Tests
    1.11 +imports
    1.12 +  Complex_Main
    1.13 +  "~~/src/HOL/Library/Extended_Real"
    1.14 +  "~~/src/HOL/Library/Liminf_Limsup"
    1.15 +begin
    1.16 +
    1.17 +text \<open>
    1.18 +  The definition of the radius of convergence of a power series,
    1.19 +  various summability tests, lemmas to compute the radius of convergence etc.
    1.20 +\<close>
    1.21 +
    1.22 +subsection \<open>Rounded dual logarithm\<close>
    1.23 +
    1.24 +(* This is required for the Cauchy condensation criterion *)
    1.25 +
    1.26 +definition "natlog2 n = (if n = 0 then 0 else nat \<lfloor>log 2 (real_of_nat n)\<rfloor>)"
    1.27 +
    1.28 +lemma natlog2_0 [simp]: "natlog2 0 = 0" by (simp add: natlog2_def)
    1.29 +lemma natlog2_1 [simp]: "natlog2 1 = 0" by (simp add: natlog2_def)
    1.30 +lemma natlog2_eq_0_iff: "natlog2 n = 0 \<longleftrightarrow> n < 2" by (simp add: natlog2_def)
    1.31 +
    1.32 +lemma natlog2_power_of_two [simp]: "natlog2 (2 ^ n) = n"
    1.33 +  by (simp add: natlog2_def log_nat_power)
    1.34 +
    1.35 +lemma natlog2_mono: "m \<le> n \<Longrightarrow> natlog2 m \<le> natlog2 n"
    1.36 +  unfolding natlog2_def by (simp_all add: nat_mono floor_mono)
    1.37 +
    1.38 +lemma pow_natlog2_le: "n > 0 \<Longrightarrow> 2 ^ natlog2 n \<le> n"
    1.39 +proof -
    1.40 +  assume n: "n > 0"
    1.41 +  from n have "of_nat (2 ^ natlog2 n) = 2 powr real_of_nat (nat \<lfloor>log 2 (real_of_nat n)\<rfloor>)"
    1.42 +    by (subst powr_realpow) (simp_all add: natlog2_def)
    1.43 +  also have "\<dots> = 2 powr of_int \<lfloor>log 2 (real_of_nat n)\<rfloor>" using n by simp
    1.44 +  also have "\<dots> \<le> 2 powr log 2 (real_of_nat n)" by (intro powr_mono) (linarith, simp_all)
    1.45 +  also have "\<dots> = of_nat n" using n by simp
    1.46 +  finally show ?thesis by simp
    1.47 +qed
    1.48 +
    1.49 +lemma pow_natlog2_gt: "n > 0 \<Longrightarrow> 2 * 2 ^ natlog2 n > n"
    1.50 +  and pow_natlog2_ge: "n > 0 \<Longrightarrow> 2 * 2 ^ natlog2 n \<ge> n"
    1.51 +proof -
    1.52 +  assume n: "n > 0"
    1.53 +  from n have "of_nat n = 2 powr log 2 (real_of_nat n)" by simp
    1.54 +  also have "\<dots> < 2 powr (1 + of_int \<lfloor>log 2 (real_of_nat n)\<rfloor>)"
    1.55 +    by (intro powr_less_mono) (linarith, simp_all)
    1.56 +  also from n have "\<dots> = 2 powr (1 + real_of_nat (nat \<lfloor>log 2 (real_of_nat n)\<rfloor>))" by simp
    1.57 +  also from n have "\<dots> = of_nat (2 * 2 ^ natlog2 n)"
    1.58 +    by (simp_all add: natlog2_def powr_real_of_int powr_add)
    1.59 +  finally show "2 * 2 ^ natlog2 n > n" by (rule of_nat_less_imp_less)
    1.60 +  thus "2 * 2 ^ natlog2 n \<ge> n" by simp
    1.61 +qed
    1.62 +
    1.63 +lemma natlog2_eqI:
    1.64 +  assumes "n > 0" "2^k \<le> n" "n < 2 * 2^k"
    1.65 +  shows   "natlog2 n = k"
    1.66 +proof -
    1.67 +  from assms have "of_nat (2 ^ k) \<le> real_of_nat n"  by (subst of_nat_le_iff) simp_all
    1.68 +  hence "real_of_int (int k) \<le> log (of_nat 2) (real_of_nat n)"
    1.69 +    by (subst le_log_iff) (simp_all add: powr_realpow assms del: of_nat_le_iff)
    1.70 +  moreover from assms have "real_of_nat n < of_nat (2 ^ Suc k)" by (subst of_nat_less_iff) simp_all
    1.71 +  hence "log 2 (real_of_nat n) < of_nat k + 1"
    1.72 +    by (subst log_less_iff) (simp_all add: assms powr_realpow powr_add)
    1.73 +  ultimately have "\<lfloor>log 2 (real_of_nat n)\<rfloor> = of_nat k" by (intro floor_unique) simp_all
    1.74 +  with assms show ?thesis by (simp add: natlog2_def)
    1.75 +qed
    1.76 +
    1.77 +lemma natlog2_rec:
    1.78 +  assumes "n \<ge> 2"
    1.79 +  shows   "natlog2 n = 1 + natlog2 (n div 2)"
    1.80 +proof (rule natlog2_eqI)
    1.81 +  from assms have "2 ^ (1 + natlog2 (n div 2)) \<le> 2 * (n div 2)"
    1.82 +    by (simp add: pow_natlog2_le)
    1.83 +  also have "\<dots> \<le> n" by simp
    1.84 +  finally show "2 ^ (1 + natlog2 (n div 2)) \<le> n" .
    1.85 +next
    1.86 +  from assms have "n < 2 * (n div 2 + 1)" by simp
    1.87 +  also from assms have "(n div 2) < 2 ^ (1 + natlog2 (n div 2))"
    1.88 +    by (simp add: pow_natlog2_gt)
    1.89 +  hence "2 * (n div 2 + 1) \<le> 2 * (2 ^ (1 + natlog2 (n div 2)))"
    1.90 +    by (intro mult_left_mono) simp_all
    1.91 +  finally show "n < 2 * 2 ^ (1 + natlog2 (n div 2))" .
    1.92 +qed (insert assms, simp_all)
    1.93 +
    1.94 +fun natlog2_aux where
    1.95 +  "natlog2_aux n acc = (if (n::nat) < 2 then acc else natlog2_aux (n div 2) (acc + 1))"
    1.96 +
    1.97 +lemma natlog2_aux_correct:
    1.98 +  "natlog2_aux n acc = acc + natlog2 n"
    1.99 +  by (induction n acc rule: natlog2_aux.induct) (auto simp: natlog2_rec natlog2_eq_0_iff)
   1.100 +
   1.101 +lemma natlog2_code [code]: "natlog2 n = natlog2_aux n 0"
   1.102 +  by (subst natlog2_aux_correct) simp
   1.103 +
   1.104 +
   1.105 +subsection \<open>Convergence tests for infinite sums\<close>
   1.106 +
   1.107 +subsubsection \<open>Root test\<close>
   1.108 +
   1.109 +lemma limsup_root_powser:
   1.110 +  fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   1.111 +  shows "limsup (\<lambda>n. ereal (root n (norm (f n * z ^ n)))) =
   1.112 +             limsup (\<lambda>n. ereal (root n (norm (f n)))) * ereal (norm z)"
   1.113 +proof -
   1.114 +  have A: "(\<lambda>n. ereal (root n (norm (f n * z ^ n)))) =
   1.115 +              (\<lambda>n. ereal (root n (norm (f n))) * ereal (norm z))" (is "?g = ?h")
   1.116 +  proof
   1.117 +    fix n show "?g n = ?h n"
   1.118 +    by (cases "n = 0") (simp_all add: norm_mult real_root_mult real_root_pos2 norm_power)
   1.119 +  qed
   1.120 +  show ?thesis by (subst A, subst limsup_ereal_mult_right) simp_all
   1.121 +qed
   1.122 +
   1.123 +lemma limsup_root_limit:
   1.124 +  assumes "(\<lambda>n. ereal (root n (norm (f n)))) \<longlonglongrightarrow> l" (is "?g \<longlonglongrightarrow> _")
   1.125 +  shows   "limsup (\<lambda>n. ereal (root n (norm (f n)))) = l"
   1.126 +proof -
   1.127 +  from assms have "convergent ?g" "lim ?g = l"
   1.128 +    unfolding convergent_def by (blast intro: limI)+
   1.129 +  with convergent_limsup_cl show ?thesis by force
   1.130 +qed
   1.131 +
   1.132 +lemma limsup_root_limit':
   1.133 +  assumes "(\<lambda>n. root n (norm (f n))) \<longlonglongrightarrow> l"
   1.134 +  shows   "limsup (\<lambda>n. ereal (root n (norm (f n)))) = ereal l"
   1.135 +  by (intro limsup_root_limit tendsto_ereal assms)
   1.136 +
   1.137 +lemma root_test_convergence':
   1.138 +  fixes f :: "nat \<Rightarrow> 'a :: banach"
   1.139 +  defines "l \<equiv> limsup (\<lambda>n. ereal (root n (norm (f n))))"
   1.140 +  assumes l: "l < 1"
   1.141 +  shows   "summable f"
   1.142 +proof -
   1.143 +  have "0 = limsup (\<lambda>n. 0)" by (simp add: Limsup_const)
   1.144 +  also have "... \<le> l" unfolding l_def by (intro Limsup_mono) (simp_all add: real_root_ge_zero)
   1.145 +  finally have "l \<ge> 0" by simp
   1.146 +  with l obtain l' where l': "l = ereal l'" by (cases l) simp_all
   1.147 +
   1.148 +  define c where "c = (1 - l') / 2"
   1.149 +  from l and \<open>l \<ge> 0\<close> have c: "l + c > l" "l' + c \<ge> 0" "l' + c < 1" unfolding c_def
   1.150 +    by (simp_all add: field_simps l')
   1.151 +  have "\<forall>C>l. eventually (\<lambda>n. ereal (root n (norm (f n))) < C) sequentially"
   1.152 +    by (subst Limsup_le_iff[symmetric]) (simp add: l_def)
   1.153 +  with c have "eventually (\<lambda>n. ereal (root n (norm (f n))) < l + ereal c) sequentially" by simp
   1.154 +  with eventually_gt_at_top[of "0::nat"]
   1.155 +    have "eventually (\<lambda>n. norm (f n) \<le> (l' + c) ^ n) sequentially"
   1.156 +  proof eventually_elim
   1.157 +    fix n :: nat assume n: "n > 0"
   1.158 +    assume "ereal (root n (norm (f n))) < l + ereal c"
   1.159 +    hence "root n (norm (f n)) \<le> l' + c" by (simp add: l')
   1.160 +    with c n have "root n (norm (f n)) ^ n \<le> (l' + c) ^ n"
   1.161 +      by (intro power_mono) (simp_all add: real_root_ge_zero)
   1.162 +    also from n have "root n (norm (f n)) ^ n = norm (f n)" by simp
   1.163 +    finally show "norm (f n) \<le> (l' + c) ^ n" by simp
   1.164 +  qed
   1.165 +  thus ?thesis
   1.166 +    by (rule summable_comparison_test_ev[OF _ summable_geometric]) (simp add: c)
   1.167 +qed
   1.168 +
   1.169 +lemma root_test_divergence:
   1.170 +  fixes f :: "nat \<Rightarrow> 'a :: banach"
   1.171 +  defines "l \<equiv> limsup (\<lambda>n. ereal (root n (norm (f n))))"
   1.172 +  assumes l: "l > 1"
   1.173 +  shows   "\<not>summable f"
   1.174 +proof
   1.175 +  assume "summable f"
   1.176 +  hence bounded: "Bseq f" by (simp add: summable_imp_Bseq)
   1.177 +
   1.178 +  have "0 = limsup (\<lambda>n. 0)" by (simp add: Limsup_const)
   1.179 +  also have "... \<le> l" unfolding l_def by (intro Limsup_mono) (simp_all add: real_root_ge_zero)
   1.180 +  finally have l_nonneg: "l \<ge> 0" by simp
   1.181 +
   1.182 +  define c where "c = (if l = \<infinity> then 2 else 1 + (real_of_ereal l - 1) / 2)"
   1.183 +  from l l_nonneg consider "l = \<infinity>" | "\<exists>l'. l = ereal l'" by (cases l) simp_all
   1.184 +  hence c: "c > 1 \<and> ereal c < l" by cases (insert l, auto simp: c_def field_simps)
   1.185 +
   1.186 +  have unbounded: "\<not>bdd_above {n. root n (norm (f n)) > c}"
   1.187 +  proof
   1.188 +    assume "bdd_above {n. root n (norm (f n)) > c}"
   1.189 +    then obtain N where "\<forall>n. root n (norm (f n)) > c \<longrightarrow> n \<le> N" unfolding bdd_above_def by blast
   1.190 +    hence "\<exists>N. \<forall>n\<ge>N. root n (norm (f n)) \<le> c"
   1.191 +      by (intro exI[of _ "N + 1"]) (force simp: not_less_eq_eq[symmetric])
   1.192 +    hence "eventually (\<lambda>n. root n (norm (f n)) \<le> c) sequentially"
   1.193 +      by (auto simp: eventually_at_top_linorder)
   1.194 +    hence "l \<le> c" unfolding l_def by (intro Limsup_bounded) simp_all
   1.195 +    with c show False by auto
   1.196 +  qed
   1.197 +
   1.198 +  from bounded obtain K where K: "K > 0" "\<And>n. norm (f n) \<le> K" using BseqE by blast
   1.199 +  define n where "n = nat \<lceil>log c K\<rceil>"
   1.200 +  from unbounded have "\<exists>m>n. c < root m (norm (f m))" unfolding bdd_above_def
   1.201 +    by (auto simp: not_le)
   1.202 +  then guess m by (elim exE conjE) note m = this
   1.203 +  from c K have "K = c powr log c K" by (simp add: powr_def log_def)
   1.204 +  also from c have "c powr log c K \<le> c powr real n" unfolding n_def
   1.205 +    by (intro powr_mono, linarith, simp)
   1.206 +  finally have "K \<le> c ^ n" using c by (simp add: powr_realpow)
   1.207 +  also from c m have "c ^ n < c ^ m" by simp
   1.208 +  also from c m have "c ^ m < root m (norm (f m)) ^ m" by (intro power_strict_mono) simp_all
   1.209 +  also from m have "... = norm (f m)" by simp
   1.210 +  finally show False using K(2)[of m]  by simp
   1.211 +qed
   1.212 +
   1.213 +
   1.214 +subsubsection \<open>Cauchy's condensation test\<close>
   1.215 +
   1.216 +context
   1.217 +fixes f :: "nat \<Rightarrow> real"
   1.218 +begin
   1.219 +
   1.220 +private lemma condensation_inequality:
   1.221 +  assumes mono: "\<And>m n. 0 < m \<Longrightarrow> m \<le> n \<Longrightarrow> f n \<le> f m"
   1.222 +  shows   "(\<Sum>k=1..<n. f k) \<ge> (\<Sum>k=1..<n. f (2 * 2 ^ natlog2 k))" (is "?thesis1")
   1.223 +          "(\<Sum>k=1..<n. f k) \<le> (\<Sum>k=1..<n. f (2 ^ natlog2 k))" (is "?thesis2")
   1.224 +  by (intro setsum_mono mono pow_natlog2_ge pow_natlog2_le, simp, simp)+
   1.225 +
   1.226 +private lemma condensation_condense1: "(\<Sum>k=1..<2^n. f (2 ^ natlog2 k)) = (\<Sum>k<n. 2^k * f (2 ^ k))"
   1.227 +proof (induction n)
   1.228 +  case (Suc n)
   1.229 +  have "{1..<2^Suc n} = {1..<2^n} \<union> {2^n..<(2^Suc n :: nat)}" by auto
   1.230 +  also have "(\<Sum>k\<in>\<dots>. f (2 ^ natlog2 k)) =
   1.231 +                 (\<Sum>k<n. 2^k * f (2^k)) + (\<Sum>k = 2^n..<2^Suc n. f (2^natlog2 k))"
   1.232 +    by (subst setsum.union_disjoint) (insert Suc, auto)
   1.233 +  also have "natlog2 k = n" if "k \<in> {2^n..<2^Suc n}" for k using that by (intro natlog2_eqI) simp_all
   1.234 +  hence "(\<Sum>k = 2^n..<2^Suc n. f (2^natlog2 k)) = (\<Sum>(_::nat) = 2^n..<2^Suc n. f (2^n))"
   1.235 +    by (intro setsum.cong) simp_all
   1.236 +  also have "\<dots> = 2^n * f (2^n)" by (simp add: of_nat_power)
   1.237 +  finally show ?case by simp
   1.238 +qed simp
   1.239 +
   1.240 +private lemma condensation_condense2: "(\<Sum>k=1..<2^n. f (2 * 2 ^ natlog2 k)) = (\<Sum>k<n. 2^k * f (2 ^ Suc k))"
   1.241 +proof (induction n)
   1.242 +  case (Suc n)
   1.243 +  have "{1..<2^Suc n} = {1..<2^n} \<union> {2^n..<(2^Suc n :: nat)}" by auto
   1.244 +  also have "(\<Sum>k\<in>\<dots>. f (2 * 2 ^ natlog2 k)) =
   1.245 +                 (\<Sum>k<n. 2^k * f (2^Suc k)) + (\<Sum>k = 2^n..<2^Suc n. f (2 * 2^natlog2 k))"
   1.246 +    by (subst setsum.union_disjoint) (insert Suc, auto)
   1.247 +  also have "natlog2 k = n" if "k \<in> {2^n..<2^Suc n}" for k using that by (intro natlog2_eqI) simp_all
   1.248 +  hence "(\<Sum>k = 2^n..<2^Suc n. f (2*2^natlog2 k)) = (\<Sum>(_::nat) = 2^n..<2^Suc n. f (2^Suc n))"
   1.249 +    by (intro setsum.cong) simp_all
   1.250 +  also have "\<dots> = 2^n * f (2^Suc n)" by (simp add: of_nat_power)
   1.251 +  finally show ?case by simp
   1.252 +qed simp
   1.253 +
   1.254 +lemma condensation_test:
   1.255 +  assumes mono: "\<And>m. 0 < m \<Longrightarrow> f (Suc m) \<le> f m"
   1.256 +  assumes nonneg: "\<And>n. f n \<ge> 0"
   1.257 +  shows "summable f \<longleftrightarrow> summable (\<lambda>n. 2^n * f (2^n))"
   1.258 +proof -
   1.259 +  define f' where "f' n = (if n = 0 then 0 else f n)" for n
   1.260 +  from mono have mono': "decseq (\<lambda>n. f (Suc n))" by (intro decseq_SucI) simp
   1.261 +  hence mono': "f n \<le> f m" if "m \<le> n" "m > 0" for m n
   1.262 +    using that decseqD[OF mono', of "m - 1" "n - 1"] by simp
   1.263 +
   1.264 +  have "(\<lambda>n. f (Suc n)) = (\<lambda>n. f' (Suc n))" by (intro ext) (simp add: f'_def)
   1.265 +  hence "summable f \<longleftrightarrow> summable f'"
   1.266 +    by (subst (1 2) summable_Suc_iff [symmetric]) (simp only:)
   1.267 +  also have "\<dots> \<longleftrightarrow> convergent (\<lambda>n. \<Sum>k<n. f' k)" unfolding summable_iff_convergent ..
   1.268 +  also have "monoseq (\<lambda>n. \<Sum>k<n. f' k)" unfolding f'_def
   1.269 +    by (intro mono_SucI1) (auto intro!: mult_nonneg_nonneg nonneg)
   1.270 +  hence "convergent (\<lambda>n. \<Sum>k<n. f' k) \<longleftrightarrow> Bseq (\<lambda>n. \<Sum>k<n. f' k)"
   1.271 +    by (rule monoseq_imp_convergent_iff_Bseq)
   1.272 +  also have "\<dots> \<longleftrightarrow> Bseq (\<lambda>n. \<Sum>k=1..<n. f' k)" unfolding One_nat_def
   1.273 +    by (subst setsum_shift_lb_Suc0_0_upt) (simp_all add: f'_def atLeast0LessThan)
   1.274 +  also have "\<dots> \<longleftrightarrow> Bseq (\<lambda>n. \<Sum>k=1..<n. f k)" unfolding f'_def by simp
   1.275 +  also have "\<dots> \<longleftrightarrow> Bseq (\<lambda>n. \<Sum>k=1..<2^n. f k)"
   1.276 +    by (rule nonneg_incseq_Bseq_subseq_iff[symmetric])
   1.277 +       (auto intro!: setsum_nonneg incseq_SucI nonneg simp: subseq_def)
   1.278 +  also have "\<dots> \<longleftrightarrow> Bseq (\<lambda>n. \<Sum>k<n. 2^k * f (2^k))"
   1.279 +  proof (intro iffI)
   1.280 +    assume A: "Bseq (\<lambda>n. \<Sum>k=1..<2^n. f k)"
   1.281 +    have "eventually (\<lambda>n. norm (\<Sum>k<n. 2^k * f (2^Suc k)) \<le> norm (\<Sum>k=1..<2^n. f k)) sequentially"
   1.282 +    proof (intro always_eventually allI)
   1.283 +      fix n :: nat
   1.284 +      have "norm (\<Sum>k<n. 2^k * f (2^Suc k)) = (\<Sum>k<n. 2^k * f (2^Suc k))" unfolding real_norm_def
   1.285 +        by (intro abs_of_nonneg setsum_nonneg ballI mult_nonneg_nonneg nonneg) simp_all
   1.286 +      also have "\<dots> \<le> (\<Sum>k=1..<2^n. f k)"
   1.287 +        by (subst condensation_condense2 [symmetric]) (intro condensation_inequality mono')
   1.288 +      also have "\<dots> = norm \<dots>" unfolding real_norm_def
   1.289 +        by (intro abs_of_nonneg[symmetric] setsum_nonneg ballI mult_nonneg_nonneg nonneg)
   1.290 +      finally show "norm (\<Sum>k<n. 2 ^ k * f (2 ^ Suc k)) \<le> norm (\<Sum>k=1..<2^n. f k)" .
   1.291 +    qed
   1.292 +    from this and A have "Bseq (\<lambda>n. \<Sum>k<n. 2^k * f (2^Suc k))" by (rule Bseq_eventually_mono)
   1.293 +    from Bseq_mult[OF Bfun_const[of 2] this] have "Bseq (\<lambda>n. \<Sum>k<n. 2^Suc k * f (2^Suc k))"
   1.294 +      by (simp add: setsum_right_distrib setsum_left_distrib mult_ac)
   1.295 +    hence "Bseq (\<lambda>n. (\<Sum>k=Suc 0..<Suc n. 2^k * f (2^k)) + f 1)"
   1.296 +      by (intro Bseq_add, subst setsum_shift_bounds_Suc_ivl) (simp add: atLeast0LessThan)
   1.297 +    hence "Bseq (\<lambda>n. (\<Sum>k=0..<Suc n. 2^k * f (2^k)))"
   1.298 +      by (subst setsum_head_upt_Suc) (simp_all add: add_ac)
   1.299 +    thus "Bseq (\<lambda>n. (\<Sum>k<n. 2^k * f (2^k)))"
   1.300 +      by (subst (asm) Bseq_Suc_iff) (simp add: atLeast0LessThan)
   1.301 +  next
   1.302 +    assume A: "Bseq (\<lambda>n. (\<Sum>k<n. 2^k * f (2^k)))"
   1.303 +    have "eventually (\<lambda>n. norm (\<Sum>k=1..<2^n. f k) \<le> norm (\<Sum>k<n. 2^k * f (2^k))) sequentially"
   1.304 +    proof (intro always_eventually allI)
   1.305 +      fix n :: nat
   1.306 +      have "norm (\<Sum>k=1..<2^n. f k) = (\<Sum>k=1..<2^n. f k)" unfolding real_norm_def
   1.307 +        by (intro abs_of_nonneg setsum_nonneg ballI mult_nonneg_nonneg nonneg)
   1.308 +      also have "\<dots> \<le> (\<Sum>k<n. 2^k * f (2^k))"
   1.309 +        by (subst condensation_condense1 [symmetric]) (intro condensation_inequality mono')
   1.310 +      also have "\<dots> = norm \<dots>" unfolding real_norm_def
   1.311 +        by (intro abs_of_nonneg [symmetric] setsum_nonneg ballI mult_nonneg_nonneg nonneg) simp_all
   1.312 +      finally show "norm (\<Sum>k=1..<2^n. f k) \<le> norm (\<Sum>k<n. 2^k * f (2^k))" .
   1.313 +    qed
   1.314 +    from this and A show "Bseq (\<lambda>n. \<Sum>k=1..<2^n. f k)" by (rule Bseq_eventually_mono)
   1.315 +  qed
   1.316 +  also have "monoseq (\<lambda>n. (\<Sum>k<n. 2^k * f (2^k)))"
   1.317 +    by (intro mono_SucI1) (auto intro!: mult_nonneg_nonneg nonneg)
   1.318 +  hence "Bseq (\<lambda>n. (\<Sum>k<n. 2^k * f (2^k))) \<longleftrightarrow> convergent (\<lambda>n. (\<Sum>k<n. 2^k * f (2^k)))"
   1.319 +    by (rule monoseq_imp_convergent_iff_Bseq [symmetric])
   1.320 +  also have "\<dots> \<longleftrightarrow> summable (\<lambda>k. 2^k * f (2^k))" by (simp only: summable_iff_convergent)
   1.321 +  finally show ?thesis .
   1.322 +qed
   1.323 +
   1.324 +end
   1.325 +
   1.326 +
   1.327 +subsubsection \<open>Summability of powers\<close>
   1.328 +
   1.329 +lemma abs_summable_complex_powr_iff:
   1.330 +    "summable (\<lambda>n. norm (exp (of_real (ln (of_nat n)) * s))) \<longleftrightarrow> Re s < -1"
   1.331 +proof (cases "Re s \<le> 0")
   1.332 +  let ?l = "\<lambda>n. complex_of_real (ln (of_nat n))"
   1.333 +  case False
   1.334 +  with eventually_gt_at_top[of "0::nat"]
   1.335 +    have "eventually (\<lambda>n. norm (1 :: real) \<le> norm (exp (?l n * s))) sequentially"
   1.336 +    by (auto intro!: ge_one_powr_ge_zero elim!: eventually_mono)
   1.337 +  from summable_comparison_test_ev[OF this] False show ?thesis by (auto simp: summable_const_iff)
   1.338 +next
   1.339 +  let ?l = "\<lambda>n. complex_of_real (ln (of_nat n))"
   1.340 +  case True
   1.341 +  hence "summable (\<lambda>n. norm (exp (?l n * s))) \<longleftrightarrow> summable (\<lambda>n. 2^n * norm (exp (?l (2^n) * s)))"
   1.342 +    by (intro condensation_test) (auto intro!: mult_right_mono_neg)
   1.343 +  also have "(\<lambda>n. 2^n * norm (exp (?l (2^n) * s))) = (\<lambda>n. (2 powr (Re s + 1)) ^ n)"
   1.344 +  proof
   1.345 +    fix n :: nat
   1.346 +    have "2^n * norm (exp (?l (2^n) * s)) = exp (real n * ln 2) * exp (real n * ln 2 * Re s)"
   1.347 +      using True by (subst exp_of_nat_mult) (simp add: ln_realpow algebra_simps)
   1.348 +    also have "\<dots> = exp (real n * (ln 2 * (Re s + 1)))"
   1.349 +      by (simp add: algebra_simps exp_add)
   1.350 +    also have "\<dots> = exp (ln 2 * (Re s + 1)) ^ n" by (subst exp_of_nat_mult) simp
   1.351 +    also have "exp (ln 2 * (Re s + 1)) = 2 powr (Re s + 1)" by (simp add: powr_def)
   1.352 +    finally show "2^n * norm (exp (?l (2^n) * s)) = (2 powr (Re s + 1)) ^ n" .
   1.353 +  qed
   1.354 +  also have "summable \<dots> \<longleftrightarrow> 2 powr (Re s + 1) < 2 powr 0"
   1.355 +    by (subst summable_geometric_iff) simp
   1.356 +  also have "\<dots> \<longleftrightarrow> Re s < -1" by (subst powr_less_cancel_iff) (simp, linarith)
   1.357 +  finally show ?thesis .
   1.358 +qed
   1.359 +
   1.360 +lemma summable_complex_powr_iff:
   1.361 +  assumes "Re s < -1"
   1.362 +  shows   "summable (\<lambda>n. exp (of_real (ln (of_nat n)) * s))"
   1.363 +  by (rule summable_norm_cancel, subst abs_summable_complex_powr_iff) fact
   1.364 +
   1.365 +lemma summable_real_powr_iff: "summable (\<lambda>n. of_nat n powr s :: real) \<longleftrightarrow> s < -1"
   1.366 +proof -
   1.367 +  from eventually_gt_at_top[of "0::nat"]
   1.368 +    have "summable (\<lambda>n. of_nat n powr s) \<longleftrightarrow> summable (\<lambda>n. exp (ln (of_nat n) * s))"
   1.369 +    by (intro summable_cong) (auto elim!: eventually_mono simp: powr_def)
   1.370 +  also have "\<dots> \<longleftrightarrow> s < -1" using abs_summable_complex_powr_iff[of "of_real s"] by simp
   1.371 +  finally show ?thesis .
   1.372 +qed
   1.373 +
   1.374 +lemma inverse_power_summable:
   1.375 +  assumes s: "s \<ge> 2"
   1.376 +  shows "summable (\<lambda>n. inverse (of_nat n ^ s :: 'a :: {real_normed_div_algebra,banach}))"
   1.377 +proof (rule summable_norm_cancel, subst summable_cong)
   1.378 +  from eventually_gt_at_top[of "0::nat"]
   1.379 +    show "eventually (\<lambda>n. norm (inverse (of_nat n ^ s:: 'a)) = real_of_nat n powr (-real s)) at_top"
   1.380 +    by eventually_elim (simp add: norm_inverse norm_power powr_minus powr_realpow)
   1.381 +qed (insert s summable_real_powr_iff[of "-s"], simp_all)
   1.382 +
   1.383 +lemma not_summable_harmonic: "\<not>summable (\<lambda>n. inverse (of_nat n) :: 'a :: real_normed_field)"
   1.384 +proof
   1.385 +  assume "summable (\<lambda>n. inverse (of_nat n) :: 'a)"
   1.386 +  hence "convergent (\<lambda>n. norm (of_real (\<Sum>k<n. inverse (of_nat k)) :: 'a))"
   1.387 +    by (simp add: summable_iff_convergent convergent_norm)
   1.388 +  hence "convergent (\<lambda>n. abs (\<Sum>k<n. inverse (of_nat k)) :: real)" by (simp only: norm_of_real)
   1.389 +  also have "(\<lambda>n. abs (\<Sum>k<n. inverse (of_nat k)) :: real) = (\<lambda>n. \<Sum>k<n. inverse (of_nat k))"
   1.390 +    by (intro ext abs_of_nonneg setsum_nonneg) auto
   1.391 +  also have "convergent \<dots> \<longleftrightarrow> summable (\<lambda>k. inverse (of_nat k) :: real)"
   1.392 +    by (simp add: summable_iff_convergent)
   1.393 +  finally show False using summable_real_powr_iff[of "-1"] by (simp add: powr_minus)
   1.394 +qed
   1.395 +
   1.396 +
   1.397 +subsubsection \<open>Kummer's test\<close>
   1.398 +
   1.399 +lemma kummers_test_convergence:
   1.400 +  fixes f p :: "nat \<Rightarrow> real"
   1.401 +  assumes pos_f: "eventually (\<lambda>n. f n > 0) sequentially"
   1.402 +  assumes nonneg_p: "eventually (\<lambda>n. p n \<ge> 0) sequentially"
   1.403 +  defines "l \<equiv> liminf (\<lambda>n. ereal (p n * f n / f (Suc n) - p (Suc n)))"
   1.404 +  assumes l: "l > 0"
   1.405 +  shows   "summable f"
   1.406 +  unfolding summable_iff_convergent'
   1.407 +proof -
   1.408 +  define r where "r = (if l = \<infinity> then 1 else real_of_ereal l / 2)"
   1.409 +  from l have "r > 0 \<and> of_real r < l" by (cases l) (simp_all add: r_def)
   1.410 +  hence r: "r > 0" "of_real r < l" by simp_all
   1.411 +  hence "eventually (\<lambda>n. p n * f n / f (Suc n) - p (Suc n) > r) sequentially"
   1.412 +    unfolding l_def by (force dest: less_LiminfD)
   1.413 +  moreover from pos_f have "eventually (\<lambda>n. f (Suc n) > 0) sequentially"
   1.414 +    by (subst eventually_sequentially_Suc)
   1.415 +  ultimately have "eventually (\<lambda>n. p n * f n - p (Suc n) * f (Suc n) > r * f (Suc n)) sequentially"
   1.416 +    by eventually_elim (simp add: field_simps)
   1.417 +  from eventually_conj[OF pos_f eventually_conj[OF nonneg_p this]]
   1.418 +    obtain m where m: "\<And>n. n \<ge> m \<Longrightarrow> f n > 0" "\<And>n. n \<ge> m \<Longrightarrow> p n \<ge> 0"
   1.419 +        "\<And>n. n \<ge> m \<Longrightarrow> p n * f n - p (Suc n) * f (Suc n) > r * f (Suc n)"
   1.420 +    unfolding eventually_at_top_linorder by blast
   1.421 +
   1.422 +  let ?c = "(norm (\<Sum>k\<le>m. r * f k) + p m * f m) / r"
   1.423 +  have "Bseq (\<lambda>n. (\<Sum>k\<le>n + Suc m. f k))"
   1.424 +  proof (rule BseqI')
   1.425 +    fix k :: nat
   1.426 +    define n where "n = k + Suc m"
   1.427 +    have n: "n > m" by (simp add: n_def)
   1.428 +
   1.429 +    from r have "r * norm (\<Sum>k\<le>n. f k) = norm (\<Sum>k\<le>n. r * f k)"
   1.430 +      by (simp add: setsum_right_distrib[symmetric] abs_mult)
   1.431 +    also from n have "{..n} = {..m} \<union> {Suc m..n}" by auto
   1.432 +    hence "(\<Sum>k\<le>n. r * f k) = (\<Sum>k\<in>{..m} \<union> {Suc m..n}. r * f k)" by (simp only:)
   1.433 +    also have "\<dots> = (\<Sum>k\<le>m. r * f k) + (\<Sum>k=Suc m..n. r * f k)"
   1.434 +      by (subst setsum.union_disjoint) auto
   1.435 +    also have "norm \<dots> \<le> norm (\<Sum>k\<le>m. r * f k) + norm (\<Sum>k=Suc m..n. r * f k)"
   1.436 +      by (rule norm_triangle_ineq)
   1.437 +    also from r less_imp_le[OF m(1)] have "(\<Sum>k=Suc m..n. r * f k) \<ge> 0"
   1.438 +      by (intro setsum_nonneg) auto
   1.439 +    hence "norm (\<Sum>k=Suc m..n. r * f k) = (\<Sum>k=Suc m..n. r * f k)" by simp
   1.440 +    also have "(\<Sum>k=Suc m..n. r * f k) = (\<Sum>k=m..<n. r * f (Suc k))"
   1.441 +     by (subst setsum_shift_bounds_Suc_ivl [symmetric])
   1.442 +          (simp only: atLeastLessThanSuc_atLeastAtMost)
   1.443 +    also from m have "\<dots> \<le> (\<Sum>k=m..<n. p k * f k - p (Suc k) * f (Suc k))"
   1.444 +      by (intro setsum_mono[OF less_imp_le]) simp_all
   1.445 +    also have "\<dots> = -(\<Sum>k=m..<n. p (Suc k) * f (Suc k) - p k * f k)"
   1.446 +      by (simp add: setsum_negf [symmetric] algebra_simps)
   1.447 +    also from n have "\<dots> = p m * f m - p n * f n"
   1.448 +      by (cases n, simp, simp only: atLeastLessThanSuc_atLeastAtMost, subst setsum_Suc_diff) simp_all
   1.449 +    also from less_imp_le[OF m(1)] m(2) n have "\<dots> \<le> p m * f m" by simp
   1.450 +    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
   1.451 +      by (subst pos_le_divide_eq[OF r(1)]) (simp only: mult_ac)
   1.452 +  qed
   1.453 +  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'
   1.454 +    using less_imp_le[OF m(1)] that by (intro setsum_mono2) auto
   1.455 +  ultimately show "convergent (\<lambda>n. \<Sum>k\<le>n. f k)" by (rule Bseq_monoseq_convergent'_inc)
   1.456 +qed
   1.457 +
   1.458 +
   1.459 +lemma kummers_test_divergence:
   1.460 +  fixes f p :: "nat \<Rightarrow> real"
   1.461 +  assumes pos_f: "eventually (\<lambda>n. f n > 0) sequentially"
   1.462 +  assumes pos_p: "eventually (\<lambda>n. p n > 0) sequentially"
   1.463 +  assumes divergent_p: "\<not>summable (\<lambda>n. inverse (p n))"
   1.464 +  defines "l \<equiv> limsup (\<lambda>n. ereal (p n * f n / f (Suc n) - p (Suc n)))"
   1.465 +  assumes l: "l < 0"
   1.466 +  shows   "\<not>summable f"
   1.467 +proof
   1.468 +  assume "summable f"
   1.469 +  from eventually_conj[OF pos_f eventually_conj[OF pos_p Limsup_lessD[OF l[unfolded l_def]]]]
   1.470 +    obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> p n > 0" "\<And>n. n \<ge> N \<Longrightarrow> f n > 0"
   1.471 +                      "\<And>n. n \<ge> N \<Longrightarrow> p n * f n / f (Suc n) - p (Suc n) < 0"
   1.472 +    by (auto simp: eventually_at_top_linorder)
   1.473 +  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"]
   1.474 +    by (simp add: field_simps)
   1.475 +  have "p n * f n \<ge> p N * f N" if "n \<ge> N" for n using that and A
   1.476 +      by (induction n rule: dec_induct) (auto intro!: less_imp_le elim!: order.trans)
   1.477 +  from eventually_ge_at_top[of N] N this
   1.478 +    have "eventually (\<lambda>n. norm (p N * f N * inverse (p n)) \<le> f n) sequentially"
   1.479 +    by (auto elim!: eventually_mono simp: field_simps abs_of_pos)
   1.480 +  from this and \<open>summable f\<close> have "summable (\<lambda>n. p N * f N * inverse (p n))"
   1.481 +    by (rule summable_comparison_test_ev)
   1.482 +  from summable_mult[OF this, of "inverse (p N * f N)"] N[OF le_refl]
   1.483 +    have "summable (\<lambda>n. inverse (p n))" by (simp add: divide_simps)
   1.484 +  with divergent_p show False by contradiction
   1.485 +qed
   1.486 +
   1.487 +
   1.488 +subsubsection \<open>Ratio test\<close>
   1.489 +
   1.490 +lemma ratio_test_convergence:
   1.491 +  fixes f :: "nat \<Rightarrow> real"
   1.492 +  assumes pos_f: "eventually (\<lambda>n. f n > 0) sequentially"
   1.493 +  defines "l \<equiv> liminf (\<lambda>n. ereal (f n / f (Suc n)))"
   1.494 +  assumes l: "l > 1"
   1.495 +  shows   "summable f"
   1.496 +proof (rule kummers_test_convergence[OF pos_f])
   1.497 +  note l
   1.498 +  also have "l = liminf (\<lambda>n. ereal (f n / f (Suc n) - 1)) + 1"
   1.499 +    by (subst Liminf_add_ereal_right[symmetric]) (simp_all add: minus_ereal_def l_def one_ereal_def)
   1.500 +  finally show "liminf (\<lambda>n. ereal (1 * f n / f (Suc n) - 1)) > 0"
   1.501 +    by (cases "liminf (\<lambda>n. ereal (1 * f n / f (Suc n) - 1))") simp_all
   1.502 +qed simp
   1.503 +
   1.504 +lemma ratio_test_divergence:
   1.505 +  fixes f :: "nat \<Rightarrow> real"
   1.506 +  assumes pos_f: "eventually (\<lambda>n. f n > 0) sequentially"
   1.507 +  defines "l \<equiv> limsup (\<lambda>n. ereal (f n / f (Suc n)))"
   1.508 +  assumes l: "l < 1"
   1.509 +  shows   "\<not>summable f"
   1.510 +proof (rule kummers_test_divergence[OF pos_f])
   1.511 +  have "limsup (\<lambda>n. ereal (f n / f (Suc n) - 1)) + 1 = l"
   1.512 +    by (subst Limsup_add_ereal_right[symmetric]) (simp_all add: minus_ereal_def l_def one_ereal_def)
   1.513 +  also note l
   1.514 +  finally show "limsup (\<lambda>n. ereal (1 * f n / f (Suc n) - 1)) < 0"
   1.515 +    by (cases "limsup (\<lambda>n. ereal (1 * f n / f (Suc n) - 1))") simp_all
   1.516 +qed (simp_all add: summable_const_iff)
   1.517 +
   1.518 +
   1.519 +subsubsection \<open>Raabe's test\<close>
   1.520 +
   1.521 +lemma raabes_test_convergence:
   1.522 +fixes f :: "nat \<Rightarrow> real"
   1.523 +  assumes pos: "eventually (\<lambda>n. f n > 0) sequentially"
   1.524 +  defines "l \<equiv> liminf (\<lambda>n. ereal (of_nat n * (f n / f (Suc n) - 1)))"
   1.525 +  assumes l: "l > 1"
   1.526 +  shows   "summable f"
   1.527 +proof (rule kummers_test_convergence)
   1.528 +  let ?l' = "liminf (\<lambda>n. ereal (of_nat n * f n / f (Suc n) - of_nat (Suc n)))"
   1.529 +  have "1 < l" by fact
   1.530 +  also have "l = liminf (\<lambda>n. ereal (of_nat n * f n / f (Suc n) - of_nat (Suc n)) + 1)"
   1.531 +    by (simp add: l_def algebra_simps)
   1.532 +  also have "\<dots> = ?l' + 1" by (subst Liminf_add_ereal_right) simp_all
   1.533 +  finally show "?l' > 0" by (cases ?l') (simp_all add: algebra_simps)
   1.534 +qed (simp_all add: pos)
   1.535 +
   1.536 +lemma raabes_test_divergence:
   1.537 +fixes f :: "nat \<Rightarrow> real"
   1.538 +  assumes pos: "eventually (\<lambda>n. f n > 0) sequentially"
   1.539 +  defines "l \<equiv> limsup (\<lambda>n. ereal (of_nat n * (f n / f (Suc n) - 1)))"
   1.540 +  assumes l: "l < 1"
   1.541 +  shows   "\<not>summable f"
   1.542 +proof (rule kummers_test_divergence)
   1.543 +  let ?l' = "limsup (\<lambda>n. ereal (of_nat n * f n / f (Suc n) - of_nat (Suc n)))"
   1.544 +  note l
   1.545 +  also have "l = limsup (\<lambda>n. ereal (of_nat n * f n / f (Suc n) - of_nat (Suc n)) + 1)"
   1.546 +    by (simp add: l_def algebra_simps)
   1.547 +  also have "\<dots> = ?l' + 1" by (subst Limsup_add_ereal_right) simp_all
   1.548 +  finally show "?l' < 0" by (cases ?l') (simp_all add: algebra_simps)
   1.549 +qed (insert pos eventually_gt_at_top[of "0::nat"] not_summable_harmonic, simp_all)
   1.550 +
   1.551 +
   1.552 +
   1.553 +subsection \<open>Radius of convergence\<close>
   1.554 +
   1.555 +text \<open>
   1.556 +  The radius of convergence of a power series. This value always exists, ranges from
   1.557 +  @{term "0::ereal"} to @{term "\<infinity>::ereal"}, and the power series is guaranteed to converge for
   1.558 +  all inputs with a norm that is smaller than that radius and to diverge for all inputs with a
   1.559 +  norm that is greater.
   1.560 +\<close>
   1.561 +definition conv_radius :: "(nat \<Rightarrow> 'a :: banach) \<Rightarrow> ereal" where
   1.562 +  "conv_radius f = inverse (limsup (\<lambda>n. ereal (root n (norm (f n)))))"
   1.563 +
   1.564 +lemma conv_radius_nonneg: "conv_radius f \<ge> 0"
   1.565 +proof -
   1.566 +  have "0 = limsup (\<lambda>n. 0)" by (subst Limsup_const) simp_all
   1.567 +  also have "\<dots> \<le> limsup (\<lambda>n. ereal (root n (norm (f n))))"
   1.568 +    by (intro Limsup_mono) (simp_all add: real_root_ge_zero)
   1.569 +  finally show ?thesis
   1.570 +    unfolding conv_radius_def by (auto simp: ereal_inverse_nonneg_iff)
   1.571 +qed
   1.572 +
   1.573 +lemma conv_radius_zero [simp]: "conv_radius (\<lambda>_. 0) = \<infinity>"
   1.574 +  by (auto simp: conv_radius_def zero_ereal_def [symmetric] Limsup_const)
   1.575 +
   1.576 +lemma conv_radius_cong:
   1.577 +  assumes "eventually (\<lambda>x. f x = g x) sequentially"
   1.578 +  shows   "conv_radius f = conv_radius g"
   1.579 +proof -
   1.580 +  have "eventually (\<lambda>n. ereal (root n (norm (f n))) = ereal (root n (norm (g n)))) sequentially"
   1.581 +    using assms by eventually_elim simp
   1.582 +  from Limsup_eq[OF this] show ?thesis unfolding conv_radius_def by simp
   1.583 +qed
   1.584 +
   1.585 +lemma conv_radius_altdef:
   1.586 +  "conv_radius f = liminf (\<lambda>n. inverse (ereal (root n (norm (f n)))))"
   1.587 +  by (subst Liminf_inverse_ereal) (simp_all add: real_root_ge_zero conv_radius_def)
   1.588 +
   1.589 +lemma abs_summable_in_conv_radius:
   1.590 +  fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   1.591 +  assumes "ereal (norm z) < conv_radius f"
   1.592 +  shows   "summable (\<lambda>n. norm (f n * z ^ n))"
   1.593 +proof (rule root_test_convergence')
   1.594 +  define l where "l = limsup (\<lambda>n. ereal (root n (norm (f n))))"
   1.595 +  have "0 = limsup (\<lambda>n. 0)" by (simp add: Limsup_const)
   1.596 +  also have "... \<le> l" unfolding l_def by (intro Limsup_mono) (simp_all add: real_root_ge_zero)
   1.597 +  finally have l_nonneg: "l \<ge> 0" .
   1.598 +
   1.599 +  have "limsup (\<lambda>n. root n (norm (f n * z^n))) = l * ereal (norm z)" unfolding l_def
   1.600 +    by (rule limsup_root_powser)
   1.601 +  also from l_nonneg consider "l = 0" | "l = \<infinity>" | "\<exists>l'. l = ereal l' \<and> l' > 0"
   1.602 +    by (cases "l") (auto simp: less_le)
   1.603 +  hence "l * ereal (norm z) < 1"
   1.604 +  proof cases
   1.605 +    assume "l = \<infinity>"
   1.606 +    hence "conv_radius f = 0" unfolding conv_radius_def l_def by simp
   1.607 +    with assms show ?thesis by simp
   1.608 +  next
   1.609 +    assume "\<exists>l'. l = ereal l' \<and> l' > 0"
   1.610 +    then guess l' by (elim exE conjE) note l' = this
   1.611 +    hence "l \<noteq> \<infinity>" by auto
   1.612 +    have "l * ereal (norm z) < l * conv_radius f"
   1.613 +      by (intro ereal_mult_strict_left_mono) (simp_all add: l' assms)
   1.614 +    also have "conv_radius f = inverse l" by (simp add: conv_radius_def l_def)
   1.615 +    also from l' have "l * inverse l = 1" by simp
   1.616 +    finally show ?thesis .
   1.617 +  qed simp_all
   1.618 +  finally show "limsup (\<lambda>n. ereal (root n (norm (norm (f n * z ^ n))))) < 1" by simp
   1.619 +qed
   1.620 +
   1.621 +lemma summable_in_conv_radius:
   1.622 +  fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   1.623 +  assumes "ereal (norm z) < conv_radius f"
   1.624 +  shows   "summable (\<lambda>n. f n * z ^ n)"
   1.625 +  by (rule summable_norm_cancel, rule abs_summable_in_conv_radius) fact+
   1.626 +
   1.627 +lemma not_summable_outside_conv_radius:
   1.628 +  fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   1.629 +  assumes "ereal (norm z) > conv_radius f"
   1.630 +  shows   "\<not>summable (\<lambda>n. f n * z ^ n)"
   1.631 +proof (rule root_test_divergence)
   1.632 +  define l where "l = limsup (\<lambda>n. ereal (root n (norm (f n))))"
   1.633 +  have "0 = limsup (\<lambda>n. 0)" by (simp add: Limsup_const)
   1.634 +  also have "... \<le> l" unfolding l_def by (intro Limsup_mono) (simp_all add: real_root_ge_zero)
   1.635 +  finally have l_nonneg: "l \<ge> 0" .
   1.636 +  from assms have l_nz: "l \<noteq> 0" unfolding conv_radius_def l_def by auto
   1.637 +
   1.638 +  have "limsup (\<lambda>n. ereal (root n (norm (f n * z^n)))) = l * ereal (norm z)"
   1.639 +    unfolding l_def by (rule limsup_root_powser)
   1.640 +  also have "... > 1"
   1.641 +  proof (cases l)
   1.642 +    assume "l = \<infinity>"
   1.643 +    with assms conv_radius_nonneg[of f] show ?thesis
   1.644 +      by (auto simp: zero_ereal_def[symmetric])
   1.645 +  next
   1.646 +    fix l' assume l': "l = ereal l'"
   1.647 +    from l_nonneg l_nz have "1 = l * inverse l" by (auto simp: l' field_simps)
   1.648 +    also from l_nz have "inverse l = conv_radius f"
   1.649 +      unfolding l_def conv_radius_def by auto
   1.650 +    also from l' l_nz l_nonneg assms have "l * \<dots> < l * ereal (norm z)"
   1.651 +      by (intro ereal_mult_strict_left_mono) (auto simp: l')
   1.652 +    finally show ?thesis .
   1.653 +  qed (insert l_nonneg, simp_all)
   1.654 +  finally show "limsup (\<lambda>n. ereal (root n (norm (f n * z^n)))) > 1" .
   1.655 +qed
   1.656 +
   1.657 +
   1.658 +lemma conv_radius_geI:
   1.659 +  assumes "summable (\<lambda>n. f n * z ^ n :: 'a :: {banach, real_normed_div_algebra})"
   1.660 +  shows   "conv_radius f \<ge> norm z"
   1.661 +  using not_summable_outside_conv_radius[of f z] assms by (force simp: not_le[symmetric])
   1.662 +
   1.663 +lemma conv_radius_leI:
   1.664 +  assumes "\<not>summable (\<lambda>n. norm (f n * z ^ n :: 'a :: {banach, real_normed_div_algebra}))"
   1.665 +  shows   "conv_radius f \<le> norm z"
   1.666 +  using abs_summable_in_conv_radius[of z f] assms by (force simp: not_le[symmetric])
   1.667 +
   1.668 +lemma conv_radius_leI':
   1.669 +  assumes "\<not>summable (\<lambda>n. f n * z ^ n :: 'a :: {banach, real_normed_div_algebra})"
   1.670 +  shows   "conv_radius f \<le> norm z"
   1.671 +  using summable_in_conv_radius[of z f] assms by (force simp: not_le[symmetric])
   1.672 +
   1.673 +lemma conv_radius_geI_ex:
   1.674 +  fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   1.675 +  assumes "\<And>r. 0 < r \<Longrightarrow> ereal r < R \<Longrightarrow> \<exists>z. norm z = r \<and> summable (\<lambda>n. f n * z^n)"
   1.676 +  shows   "conv_radius f \<ge> R"
   1.677 +proof (rule linorder_cases[of "conv_radius f" R])
   1.678 +  assume R: "conv_radius f < R"
   1.679 +  with conv_radius_nonneg[of f] obtain conv_radius'
   1.680 +    where [simp]: "conv_radius f = ereal conv_radius'"
   1.681 +    by (cases "conv_radius f") simp_all
   1.682 +  define r where "r = (if R = \<infinity> then conv_radius' + 1 else (real_of_ereal R + conv_radius') / 2)"
   1.683 +  from R conv_radius_nonneg[of f] have "0 < r \<and> ereal r < R \<and> ereal r > conv_radius f"
   1.684 +    unfolding r_def by (cases R) (auto simp: r_def field_simps)
   1.685 +  with assms(1)[of r] obtain z where "norm z > conv_radius f" "summable (\<lambda>n. f n * z^n)" by auto
   1.686 +  with not_summable_outside_conv_radius[of f z] show ?thesis by simp
   1.687 +qed simp_all
   1.688 +
   1.689 +lemma conv_radius_geI_ex':
   1.690 +  fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   1.691 +  assumes "\<And>r. 0 < r \<Longrightarrow> ereal r < R \<Longrightarrow> summable (\<lambda>n. f n * of_real r^n)"
   1.692 +  shows   "conv_radius f \<ge> R"
   1.693 +proof (rule conv_radius_geI_ex)
   1.694 +  fix r assume "0 < r" "ereal r < R"
   1.695 +  with assms[of r] show "\<exists>z. norm z = r \<and> summable (\<lambda>n. f n * z ^ n)"
   1.696 +    by (intro exI[of _ "of_real r :: 'a"]) auto
   1.697 +qed
   1.698 +
   1.699 +lemma conv_radius_leI_ex:
   1.700 +  fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   1.701 +  assumes "R \<ge> 0"
   1.702 +  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))"
   1.703 +  shows   "conv_radius f \<le> R"
   1.704 +proof (rule linorder_cases[of "conv_radius f" R])
   1.705 +  assume R: "conv_radius f > R"
   1.706 +  from R assms(1) obtain R' where R': "R = ereal R'" by (cases R) simp_all
   1.707 +  define r where
   1.708 +    "r = (if conv_radius f = \<infinity> then R' + 1 else (R' + real_of_ereal (conv_radius f)) / 2)"
   1.709 +  from R conv_radius_nonneg[of f] have "r > R \<and> r < conv_radius f" unfolding r_def
   1.710 +    by (cases "conv_radius f") (auto simp: r_def field_simps R')
   1.711 +  with assms(1) assms(2)[of r] R'
   1.712 +    obtain z where "norm z < conv_radius f" "\<not>summable (\<lambda>n. norm (f n * z^n))" by auto
   1.713 +  with abs_summable_in_conv_radius[of z f] show ?thesis by auto
   1.714 +qed simp_all
   1.715 +
   1.716 +lemma conv_radius_leI_ex':
   1.717 +  fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   1.718 +  assumes "R \<ge> 0"
   1.719 +  assumes "\<And>r. 0 < r \<Longrightarrow> ereal r > R \<Longrightarrow> \<not>summable (\<lambda>n. f n * of_real r^n)"
   1.720 +  shows   "conv_radius f \<le> R"
   1.721 +proof (rule conv_radius_leI_ex)
   1.722 +  fix r assume "0 < r" "ereal r > R"
   1.723 +  with assms(2)[of r] show "\<exists>z. norm z = r \<and> \<not>summable (\<lambda>n. norm (f n * z ^ n))"
   1.724 +    by (intro exI[of _ "of_real r :: 'a"]) (auto dest: summable_norm_cancel)
   1.725 +qed fact+
   1.726 +
   1.727 +lemma conv_radius_eqI:
   1.728 +  fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   1.729 +  assumes "R \<ge> 0"
   1.730 +  assumes "\<And>r. 0 < r \<Longrightarrow> ereal r < R \<Longrightarrow> \<exists>z. norm z = r \<and> summable (\<lambda>n. f n * z^n)"
   1.731 +  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))"
   1.732 +  shows   "conv_radius f = R"
   1.733 +  by (intro antisym conv_radius_geI_ex conv_radius_leI_ex assms)
   1.734 +
   1.735 +lemma conv_radius_eqI':
   1.736 +  fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   1.737 +  assumes "R \<ge> 0"
   1.738 +  assumes "\<And>r. 0 < r \<Longrightarrow> ereal r < R \<Longrightarrow> summable (\<lambda>n. f n * (of_real r)^n)"
   1.739 +  assumes "\<And>r. 0 < r \<Longrightarrow> ereal r > R \<Longrightarrow> \<not>summable (\<lambda>n. norm (f n * (of_real r)^n))"
   1.740 +  shows   "conv_radius f = R"
   1.741 +proof (intro conv_radius_eqI[OF assms(1)])
   1.742 +  fix r assume "0 < r" "ereal r < R" with assms(2)[OF this]
   1.743 +    show "\<exists>z. norm z = r \<and> summable (\<lambda>n. f n * z ^ n)" by force
   1.744 +next
   1.745 +  fix r assume "0 < r" "ereal r > R" with assms(3)[OF this]
   1.746 +    show "\<exists>z. norm z = r \<and> \<not>summable (\<lambda>n. norm (f n * z ^ n))" by force
   1.747 +qed
   1.748 +
   1.749 +lemma conv_radius_zeroI:
   1.750 +  fixes f :: "nat \<Rightarrow> 'a :: {banach,real_normed_div_algebra}"
   1.751 +  assumes "\<And>z. z \<noteq> 0 \<Longrightarrow> \<not>summable (\<lambda>n. f n * z^n)"
   1.752 +  shows   "conv_radius f = 0"
   1.753 +proof (rule ccontr)
   1.754 +  assume "conv_radius f \<noteq> 0"
   1.755 +  with conv_radius_nonneg[of f] have pos: "conv_radius f > 0" by simp
   1.756 +  define r where "r = (if conv_radius f = \<infinity> then 1 else real_of_ereal (conv_radius f) / 2)"
   1.757 +  from pos have r: "ereal r > 0 \<and> ereal r < conv_radius f"
   1.758 +    by (cases "conv_radius f") (simp_all add: r_def)
   1.759 +  hence "summable (\<lambda>n. f n * of_real r ^ n)" by (intro summable_in_conv_radius) simp
   1.760 +  moreover from r and assms[of "of_real r"] have "\<not>summable (\<lambda>n. f n * of_real r ^ n)" by simp
   1.761 +  ultimately show False by contradiction
   1.762 +qed
   1.763 +
   1.764 +lemma conv_radius_inftyI':
   1.765 +  fixes f :: "nat \<Rightarrow> 'a :: {banach,real_normed_div_algebra}"
   1.766 +  assumes "\<And>r. r > c \<Longrightarrow> \<exists>z. norm z = r \<and> summable (\<lambda>n. f n * z^n)"
   1.767 +  shows   "conv_radius f = \<infinity>"
   1.768 +proof -
   1.769 +  {
   1.770 +    fix r :: real
   1.771 +    have "max r (c + 1) > c" by (auto simp: max_def)
   1.772 +    from assms[OF this] obtain z where "norm z = max r (c + 1)" "summable (\<lambda>n. f n * z^n)" by blast
   1.773 +    from conv_radius_geI[OF this(2)] this(1) have "conv_radius f \<ge> r" by simp
   1.774 +  }
   1.775 +  from this[of "real_of_ereal (conv_radius f + 1)"] show "conv_radius f = \<infinity>"
   1.776 +    by (cases "conv_radius f") simp_all
   1.777 +qed
   1.778 +
   1.779 +lemma conv_radius_inftyI:
   1.780 +  fixes f :: "nat \<Rightarrow> 'a :: {banach,real_normed_div_algebra}"
   1.781 +  assumes "\<And>r. \<exists>z. norm z = r \<and> summable (\<lambda>n. f n * z^n)"
   1.782 +  shows   "conv_radius f = \<infinity>"
   1.783 +  using assms by (rule conv_radius_inftyI')
   1.784 +
   1.785 +lemma conv_radius_inftyI'':
   1.786 +  fixes f :: "nat \<Rightarrow> 'a :: {banach,real_normed_div_algebra}"
   1.787 +  assumes "\<And>z. summable (\<lambda>n. f n * z^n)"
   1.788 +  shows   "conv_radius f = \<infinity>"
   1.789 +proof (rule conv_radius_inftyI')
   1.790 +  fix r :: real assume "r > 0"
   1.791 +  with assms show "\<exists>z. norm z = r \<and> summable (\<lambda>n. f n * z^n)"
   1.792 +    by (intro exI[of _ "of_real r"]) simp
   1.793 +qed
   1.794 +
   1.795 +lemma conv_radius_ratio_limit_ereal:
   1.796 +  fixes f :: "nat \<Rightarrow> 'a :: {banach,real_normed_div_algebra}"
   1.797 +  assumes nz:  "eventually (\<lambda>n. f n \<noteq> 0) sequentially"
   1.798 +  assumes lim: "(\<lambda>n. ereal (norm (f n) / norm (f (Suc n)))) \<longlonglongrightarrow> c"
   1.799 +  shows   "conv_radius f = c"
   1.800 +proof (rule conv_radius_eqI')
   1.801 +  show "c \<ge> 0" by (intro Lim_bounded2_ereal[OF lim]) simp_all
   1.802 +next
   1.803 +  fix r assume r: "0 < r" "ereal r < c"
   1.804 +  let ?l = "liminf (\<lambda>n. ereal (norm (f n * of_real r ^ n) / norm (f (Suc n) * of_real r ^ Suc n)))"
   1.805 +  have "?l = liminf (\<lambda>n. ereal (norm (f n) / (norm (f (Suc n)))) * ereal (inverse r))"
   1.806 +    using r by (simp add: norm_mult norm_power divide_simps)
   1.807 +  also from r have "\<dots> = liminf (\<lambda>n. ereal (norm (f n) / (norm (f (Suc n))))) * ereal (inverse r)"
   1.808 +    by (intro Liminf_ereal_mult_right) simp_all
   1.809 +  also have "liminf (\<lambda>n. ereal (norm (f n) / (norm (f (Suc n))))) = c"
   1.810 +    by (intro lim_imp_Liminf lim) simp
   1.811 +  finally have l: "?l = c * ereal (inverse r)" by simp
   1.812 +  from r have  l': "c * ereal (inverse r) > 1" by (cases c) (simp_all add: field_simps)
   1.813 +  show "summable (\<lambda>n. f n * of_real r^n)"
   1.814 +    by (rule summable_norm_cancel, rule ratio_test_convergence)
   1.815 +       (insert r nz l l', auto elim!: eventually_mono)
   1.816 +next
   1.817 +  fix r assume r: "0 < r" "ereal r > c"
   1.818 +  let ?l = "limsup (\<lambda>n. ereal (norm (f n * of_real r ^ n) / norm (f (Suc n) * of_real r ^ Suc n)))"
   1.819 +  have "?l = limsup (\<lambda>n. ereal (norm (f n) / (norm (f (Suc n)))) * ereal (inverse r))"
   1.820 +    using r by (simp add: norm_mult norm_power divide_simps)
   1.821 +  also from r have "\<dots> = limsup (\<lambda>n. ereal (norm (f n) / (norm (f (Suc n))))) * ereal (inverse r)"
   1.822 +    by (intro Limsup_ereal_mult_right) simp_all
   1.823 +  also have "limsup (\<lambda>n. ereal (norm (f n) / (norm (f (Suc n))))) = c"
   1.824 +    by (intro lim_imp_Limsup lim) simp
   1.825 +  finally have l: "?l = c * ereal (inverse r)" by simp
   1.826 +  from r have  l': "c * ereal (inverse r) < 1" by (cases c) (simp_all add: field_simps)
   1.827 +  show "\<not>summable (\<lambda>n. norm (f n * of_real r^n))"
   1.828 +    by (rule ratio_test_divergence) (insert r nz l l', auto elim!: eventually_mono)
   1.829 +qed
   1.830 +
   1.831 +lemma conv_radius_ratio_limit_ereal_nonzero:
   1.832 +  fixes f :: "nat \<Rightarrow> 'a :: {banach,real_normed_div_algebra}"
   1.833 +  assumes nz:  "c \<noteq> 0"
   1.834 +  assumes lim: "(\<lambda>n. ereal (norm (f n) / norm (f (Suc n)))) \<longlonglongrightarrow> c"
   1.835 +  shows   "conv_radius f = c"
   1.836 +proof (rule conv_radius_ratio_limit_ereal[OF _ lim], rule ccontr)
   1.837 +  assume "\<not>eventually (\<lambda>n. f n \<noteq> 0) sequentially"
   1.838 +  hence "frequently (\<lambda>n. f n = 0) sequentially" by (simp add: frequently_def)
   1.839 +  hence "frequently (\<lambda>n. ereal (norm (f n) / norm (f (Suc n))) = 0) sequentially"
   1.840 +    by (force elim!: frequently_elim1)
   1.841 +  hence "c = 0" by (intro limit_frequently_eq[OF _ _ lim]) auto
   1.842 +  with nz show False by contradiction
   1.843 +qed
   1.844 +
   1.845 +lemma conv_radius_ratio_limit:
   1.846 +  fixes f :: "nat \<Rightarrow> 'a :: {banach,real_normed_div_algebra}"
   1.847 +  assumes "c' = ereal c"
   1.848 +  assumes nz:  "eventually (\<lambda>n. f n \<noteq> 0) sequentially"
   1.849 +  assumes lim: "(\<lambda>n. norm (f n) / norm (f (Suc n))) \<longlonglongrightarrow> c"
   1.850 +  shows   "conv_radius f = c'"
   1.851 +  using assms by (intro conv_radius_ratio_limit_ereal) simp_all
   1.852 +
   1.853 +lemma conv_radius_ratio_limit_nonzero:
   1.854 +  fixes f :: "nat \<Rightarrow> 'a :: {banach,real_normed_div_algebra}"
   1.855 +  assumes "c' = ereal c"
   1.856 +  assumes nz:  "c \<noteq> 0"
   1.857 +  assumes lim: "(\<lambda>n. norm (f n) / norm (f (Suc n))) \<longlonglongrightarrow> c"
   1.858 +  shows   "conv_radius f = c'"
   1.859 +  using assms by (intro conv_radius_ratio_limit_ereal_nonzero) simp_all
   1.860 +
   1.861 +lemma conv_radius_mult_power:
   1.862 +  assumes "c \<noteq> (0 :: 'a :: {real_normed_div_algebra,banach})"
   1.863 +  shows   "conv_radius (\<lambda>n. c ^ n * f n) = conv_radius f / ereal (norm c)"
   1.864 +proof -
   1.865 +  have "limsup (\<lambda>n. ereal (root n (norm (c ^ n * f n)))) =
   1.866 +          limsup (\<lambda>n. ereal (norm c) * ereal (root n (norm (f n))))"
   1.867 +    using eventually_gt_at_top[of "0::nat"]
   1.868 +    by (intro Limsup_eq)
   1.869 +       (auto elim!: eventually_mono simp: norm_mult norm_power real_root_mult real_root_power)
   1.870 +  also have "\<dots> = ereal (norm c) * limsup (\<lambda>n. ereal (root n (norm (f n))))"
   1.871 +    using assms by (subst Limsup_ereal_mult_left[symmetric]) simp_all
   1.872 +  finally have A: "limsup (\<lambda>n. ereal (root n (norm (c ^ n * f n)))) =
   1.873 +                       ereal (norm c) * limsup (\<lambda>n. ereal (root n (norm (f n))))" .
   1.874 +  show ?thesis using assms
   1.875 +    apply (cases "limsup (\<lambda>n. ereal (root n (norm (f n)))) = 0")
   1.876 +    apply (simp add: A conv_radius_def)
   1.877 +    apply (unfold conv_radius_def A divide_ereal_def, simp add: mult.commute ereal_inverse_mult)
   1.878 +    done
   1.879 +qed
   1.880 +
   1.881 +lemma conv_radius_mult_power_right:
   1.882 +  assumes "c \<noteq> (0 :: 'a :: {real_normed_div_algebra,banach})"
   1.883 +  shows   "conv_radius (\<lambda>n. f n * c ^ n) = conv_radius f / ereal (norm c)"
   1.884 +  using conv_radius_mult_power[OF assms, of f]
   1.885 +  unfolding conv_radius_def by (simp add: mult.commute norm_mult)
   1.886 +
   1.887 +lemma conv_radius_divide_power:
   1.888 +  assumes "c \<noteq> (0 :: 'a :: {real_normed_div_algebra,banach})"
   1.889 +  shows   "conv_radius (\<lambda>n. f n / c^n) = conv_radius f * ereal (norm c)"
   1.890 +proof -
   1.891 +  from assms have "inverse c \<noteq> 0" by simp
   1.892 +  from conv_radius_mult_power_right[OF this, of f] show ?thesis
   1.893 +    by (simp add: divide_inverse divide_ereal_def assms norm_inverse power_inverse)
   1.894 +qed
   1.895 +
   1.896 +
   1.897 +lemma conv_radius_add_ge:
   1.898 +  "min (conv_radius f) (conv_radius g) \<le>
   1.899 +       conv_radius (\<lambda>x. f x + g x :: 'a :: {banach,real_normed_div_algebra})"
   1.900 +  by (rule conv_radius_geI_ex')
   1.901 +     (auto simp: algebra_simps intro!: summable_add summable_in_conv_radius)
   1.902 +
   1.903 +lemma conv_radius_mult_ge:
   1.904 +  fixes f g :: "nat \<Rightarrow> ('a :: {banach,real_normed_div_algebra})"
   1.905 +  shows "conv_radius (\<lambda>x. \<Sum>i\<le>x. f i * g (x - i)) \<ge> min (conv_radius f) (conv_radius g)"
   1.906 +proof (rule conv_radius_geI_ex')
   1.907 +  fix r assume r: "r > 0" "ereal r < min (conv_radius f) (conv_radius g)"
   1.908 +  from r have "summable (\<lambda>n. (\<Sum>i\<le>n. (f i * of_real r^i) * (g (n - i) * of_real r^(n - i))))"
   1.909 +    by (intro summable_Cauchy_product abs_summable_in_conv_radius) simp_all
   1.910 +  thus "summable (\<lambda>n. (\<Sum>i\<le>n. f i * g (n - i)) * of_real r ^ n)"
   1.911 +    by (simp add: algebra_simps of_real_def power_add [symmetric] scaleR_setsum_right)
   1.912 +qed
   1.913 +
   1.914 +lemma le_conv_radius_iff:
   1.915 +  fixes a :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
   1.916 +  shows "r \<le> conv_radius a \<longleftrightarrow> (\<forall>x. norm (x-\<xi>) < r \<longrightarrow> summable (\<lambda>i. a i * (x - \<xi>) ^ i))"
   1.917 +apply (intro iffI allI impI summable_in_conv_radius conv_radius_geI_ex)
   1.918 +apply (meson less_ereal.simps(1) not_le order_trans)
   1.919 +apply (rule_tac x="of_real ra" in exI, simp)
   1.920 +apply (metis abs_of_nonneg add_diff_cancel_left' less_eq_real_def norm_of_real)
   1.921 +done
   1.922 +
   1.923 +end