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