src/HOL/Series.thy
changeset 28952 15a4b2cf8c34
parent 27108 e447b3107696
child 29197 6d4cb27ed19c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Series.thy	Wed Dec 03 15:58:44 2008 +0100
     1.3 @@ -0,0 +1,654 @@
     1.4 +(*  Title       : Series.thy
     1.5 +    Author      : Jacques D. Fleuriot
     1.6 +    Copyright   : 1998  University of Cambridge
     1.7 +
     1.8 +Converted to Isar and polished by lcp
     1.9 +Converted to setsum and polished yet more by TNN
    1.10 +Additional contributions by Jeremy Avigad
    1.11 +*) 
    1.12 +
    1.13 +header{*Finite Summation and Infinite Series*}
    1.14 +
    1.15 +theory Series
    1.16 +imports "~~/src/HOL/Hyperreal/SEQ"
    1.17 +begin
    1.18 +
    1.19 +definition
    1.20 +   sums  :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool"
    1.21 +     (infixr "sums" 80) where
    1.22 +   "f sums s = (%n. setsum f {0..<n}) ----> s"
    1.23 +
    1.24 +definition
    1.25 +   summable :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> bool" where
    1.26 +   "summable f = (\<exists>s. f sums s)"
    1.27 +
    1.28 +definition
    1.29 +   suminf   :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a" where
    1.30 +   "suminf f = (THE s. f sums s)"
    1.31 +
    1.32 +syntax
    1.33 +  "_suminf" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a" ("\<Sum>_. _" [0, 10] 10)
    1.34 +translations
    1.35 +  "\<Sum>i. b" == "CONST suminf (%i. b)"
    1.36 +
    1.37 +
    1.38 +lemma sumr_diff_mult_const:
    1.39 + "setsum f {0..<n} - (real n*r) = setsum (%i. f i - r) {0..<n::nat}"
    1.40 +by (simp add: diff_minus setsum_addf real_of_nat_def)
    1.41 +
    1.42 +lemma real_setsum_nat_ivl_bounded:
    1.43 +     "(!!p. p < n \<Longrightarrow> f(p) \<le> K)
    1.44 +      \<Longrightarrow> setsum f {0..<n::nat} \<le> real n * K"
    1.45 +using setsum_bounded[where A = "{0..<n}"]
    1.46 +by (auto simp:real_of_nat_def)
    1.47 +
    1.48 +(* Generalize from real to some algebraic structure? *)
    1.49 +lemma sumr_minus_one_realpow_zero [simp]:
    1.50 +  "(\<Sum>i=0..<2*n. (-1) ^ Suc i) = (0::real)"
    1.51 +by (induct "n", auto)
    1.52 +
    1.53 +(* FIXME this is an awful lemma! *)
    1.54 +lemma sumr_one_lb_realpow_zero [simp]:
    1.55 +  "(\<Sum>n=Suc 0..<n. f(n) * (0::real) ^ n) = 0"
    1.56 +by (rule setsum_0', simp)
    1.57 +
    1.58 +lemma sumr_group:
    1.59 +     "(\<Sum>m=0..<n::nat. setsum f {m * k ..< m*k + k}) = setsum f {0 ..< n * k}"
    1.60 +apply (subgoal_tac "k = 0 | 0 < k", auto)
    1.61 +apply (induct "n")
    1.62 +apply (simp_all add: setsum_add_nat_ivl add_commute)
    1.63 +done
    1.64 +
    1.65 +lemma sumr_offset3:
    1.66 +  "setsum f {0::nat..<n+k} = (\<Sum>m=0..<n. f (m+k)) + setsum f {0..<k}"
    1.67 +apply (subst setsum_shift_bounds_nat_ivl [symmetric])
    1.68 +apply (simp add: setsum_add_nat_ivl add_commute)
    1.69 +done
    1.70 +
    1.71 +lemma sumr_offset:
    1.72 +  fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
    1.73 +  shows "(\<Sum>m=0..<n. f(m+k)) = setsum f {0..<n+k} - setsum f {0..<k}"
    1.74 +by (simp add: sumr_offset3)
    1.75 +
    1.76 +lemma sumr_offset2:
    1.77 + "\<forall>f. (\<Sum>m=0..<n::nat. f(m+k)::real) = setsum f {0..<n+k} - setsum f {0..<k}"
    1.78 +by (simp add: sumr_offset)
    1.79 +
    1.80 +lemma sumr_offset4:
    1.81 +  "\<forall>n f. setsum f {0::nat..<n+k} = (\<Sum>m=0..<n. f (m+k)::real) + setsum f {0..<k}"
    1.82 +by (clarify, rule sumr_offset3)
    1.83 +
    1.84 +(*
    1.85 +lemma sumr_from_1_from_0: "0 < n ==>
    1.86 +      (\<Sum>n=Suc 0 ..< Suc n. if even(n) then 0 else
    1.87 +             ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n =
    1.88 +      (\<Sum>n=0..<Suc n. if even(n) then 0 else
    1.89 +             ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n"
    1.90 +by (rule_tac n1 = 1 in sumr_split_add [THEN subst], auto)
    1.91 +*)
    1.92 +
    1.93 +subsection{* Infinite Sums, by the Properties of Limits*}
    1.94 +
    1.95 +(*----------------------
    1.96 +   suminf is the sum   
    1.97 + ---------------------*)
    1.98 +lemma sums_summable: "f sums l ==> summable f"
    1.99 +by (simp add: sums_def summable_def, blast)
   1.100 +
   1.101 +lemma summable_sums: "summable f ==> f sums (suminf f)"
   1.102 +apply (simp add: summable_def suminf_def sums_def)
   1.103 +apply (blast intro: theI LIMSEQ_unique)
   1.104 +done
   1.105 +
   1.106 +lemma summable_sumr_LIMSEQ_suminf: 
   1.107 +     "summable f ==> (%n. setsum f {0..<n}) ----> (suminf f)"
   1.108 +by (rule summable_sums [unfolded sums_def])
   1.109 +
   1.110 +(*-------------------
   1.111 +    sum is unique                    
   1.112 + ------------------*)
   1.113 +lemma sums_unique: "f sums s ==> (s = suminf f)"
   1.114 +apply (frule sums_summable [THEN summable_sums])
   1.115 +apply (auto intro!: LIMSEQ_unique simp add: sums_def)
   1.116 +done
   1.117 +
   1.118 +lemma sums_split_initial_segment: "f sums s ==> 
   1.119 +  (%n. f(n + k)) sums (s - (SUM i = 0..< k. f i))"
   1.120 +  apply (unfold sums_def);
   1.121 +  apply (simp add: sumr_offset); 
   1.122 +  apply (rule LIMSEQ_diff_const)
   1.123 +  apply (rule LIMSEQ_ignore_initial_segment)
   1.124 +  apply assumption
   1.125 +done
   1.126 +
   1.127 +lemma summable_ignore_initial_segment: "summable f ==> 
   1.128 +    summable (%n. f(n + k))"
   1.129 +  apply (unfold summable_def)
   1.130 +  apply (auto intro: sums_split_initial_segment)
   1.131 +done
   1.132 +
   1.133 +lemma suminf_minus_initial_segment: "summable f ==>
   1.134 +    suminf f = s ==> suminf (%n. f(n + k)) = s - (SUM i = 0..< k. f i)"
   1.135 +  apply (frule summable_ignore_initial_segment)
   1.136 +  apply (rule sums_unique [THEN sym])
   1.137 +  apply (frule summable_sums)
   1.138 +  apply (rule sums_split_initial_segment)
   1.139 +  apply auto
   1.140 +done
   1.141 +
   1.142 +lemma suminf_split_initial_segment: "summable f ==> 
   1.143 +    suminf f = (SUM i = 0..< k. f i) + suminf (%n. f(n + k))"
   1.144 +by (auto simp add: suminf_minus_initial_segment)
   1.145 +
   1.146 +lemma series_zero: 
   1.147 +     "(\<forall>m. n \<le> m --> f(m) = 0) ==> f sums (setsum f {0..<n})"
   1.148 +apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe)
   1.149 +apply (rule_tac x = n in exI)
   1.150 +apply (clarsimp simp add:setsum_diff[symmetric] cong:setsum_ivl_cong)
   1.151 +done
   1.152 +
   1.153 +lemma sums_zero: "(\<lambda>n. 0) sums 0"
   1.154 +unfolding sums_def by (simp add: LIMSEQ_const)
   1.155 +
   1.156 +lemma summable_zero: "summable (\<lambda>n. 0)"
   1.157 +by (rule sums_zero [THEN sums_summable])
   1.158 +
   1.159 +lemma suminf_zero: "suminf (\<lambda>n. 0) = 0"
   1.160 +by (rule sums_zero [THEN sums_unique, symmetric])
   1.161 +  
   1.162 +lemma (in bounded_linear) sums:
   1.163 +  "(\<lambda>n. X n) sums a \<Longrightarrow> (\<lambda>n. f (X n)) sums (f a)"
   1.164 +unfolding sums_def by (drule LIMSEQ, simp only: setsum)
   1.165 +
   1.166 +lemma (in bounded_linear) summable:
   1.167 +  "summable (\<lambda>n. X n) \<Longrightarrow> summable (\<lambda>n. f (X n))"
   1.168 +unfolding summable_def by (auto intro: sums)
   1.169 +
   1.170 +lemma (in bounded_linear) suminf:
   1.171 +  "summable (\<lambda>n. X n) \<Longrightarrow> f (\<Sum>n. X n) = (\<Sum>n. f (X n))"
   1.172 +by (intro sums_unique sums summable_sums)
   1.173 +
   1.174 +lemma sums_mult:
   1.175 +  fixes c :: "'a::real_normed_algebra"
   1.176 +  shows "f sums a \<Longrightarrow> (\<lambda>n. c * f n) sums (c * a)"
   1.177 +by (rule mult_right.sums)
   1.178 +
   1.179 +lemma summable_mult:
   1.180 +  fixes c :: "'a::real_normed_algebra"
   1.181 +  shows "summable f \<Longrightarrow> summable (%n. c * f n)"
   1.182 +by (rule mult_right.summable)
   1.183 +
   1.184 +lemma suminf_mult:
   1.185 +  fixes c :: "'a::real_normed_algebra"
   1.186 +  shows "summable f \<Longrightarrow> suminf (\<lambda>n. c * f n) = c * suminf f";
   1.187 +by (rule mult_right.suminf [symmetric])
   1.188 +
   1.189 +lemma sums_mult2:
   1.190 +  fixes c :: "'a::real_normed_algebra"
   1.191 +  shows "f sums a \<Longrightarrow> (\<lambda>n. f n * c) sums (a * c)"
   1.192 +by (rule mult_left.sums)
   1.193 +
   1.194 +lemma summable_mult2:
   1.195 +  fixes c :: "'a::real_normed_algebra"
   1.196 +  shows "summable f \<Longrightarrow> summable (\<lambda>n. f n * c)"
   1.197 +by (rule mult_left.summable)
   1.198 +
   1.199 +lemma suminf_mult2:
   1.200 +  fixes c :: "'a::real_normed_algebra"
   1.201 +  shows "summable f \<Longrightarrow> suminf f * c = (\<Sum>n. f n * c)"
   1.202 +by (rule mult_left.suminf)
   1.203 +
   1.204 +lemma sums_divide:
   1.205 +  fixes c :: "'a::real_normed_field"
   1.206 +  shows "f sums a \<Longrightarrow> (\<lambda>n. f n / c) sums (a / c)"
   1.207 +by (rule divide.sums)
   1.208 +
   1.209 +lemma summable_divide:
   1.210 +  fixes c :: "'a::real_normed_field"
   1.211 +  shows "summable f \<Longrightarrow> summable (\<lambda>n. f n / c)"
   1.212 +by (rule divide.summable)
   1.213 +
   1.214 +lemma suminf_divide:
   1.215 +  fixes c :: "'a::real_normed_field"
   1.216 +  shows "summable f \<Longrightarrow> suminf (\<lambda>n. f n / c) = suminf f / c"
   1.217 +by (rule divide.suminf [symmetric])
   1.218 +
   1.219 +lemma sums_add: "\<lbrakk>X sums a; Y sums b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n + Y n) sums (a + b)"
   1.220 +unfolding sums_def by (simp add: setsum_addf LIMSEQ_add)
   1.221 +
   1.222 +lemma summable_add: "\<lbrakk>summable X; summable Y\<rbrakk> \<Longrightarrow> summable (\<lambda>n. X n + Y n)"
   1.223 +unfolding summable_def by (auto intro: sums_add)
   1.224 +
   1.225 +lemma suminf_add:
   1.226 +  "\<lbrakk>summable X; summable Y\<rbrakk> \<Longrightarrow> suminf X + suminf Y = (\<Sum>n. X n + Y n)"
   1.227 +by (intro sums_unique sums_add summable_sums)
   1.228 +
   1.229 +lemma sums_diff: "\<lbrakk>X sums a; Y sums b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n - Y n) sums (a - b)"
   1.230 +unfolding sums_def by (simp add: setsum_subtractf LIMSEQ_diff)
   1.231 +
   1.232 +lemma summable_diff: "\<lbrakk>summable X; summable Y\<rbrakk> \<Longrightarrow> summable (\<lambda>n. X n - Y n)"
   1.233 +unfolding summable_def by (auto intro: sums_diff)
   1.234 +
   1.235 +lemma suminf_diff:
   1.236 +  "\<lbrakk>summable X; summable Y\<rbrakk> \<Longrightarrow> suminf X - suminf Y = (\<Sum>n. X n - Y n)"
   1.237 +by (intro sums_unique sums_diff summable_sums)
   1.238 +
   1.239 +lemma sums_minus: "X sums a ==> (\<lambda>n. - X n) sums (- a)"
   1.240 +unfolding sums_def by (simp add: setsum_negf LIMSEQ_minus)
   1.241 +
   1.242 +lemma summable_minus: "summable X \<Longrightarrow> summable (\<lambda>n. - X n)"
   1.243 +unfolding summable_def by (auto intro: sums_minus)
   1.244 +
   1.245 +lemma suminf_minus: "summable X \<Longrightarrow> (\<Sum>n. - X n) = - (\<Sum>n. X n)"
   1.246 +by (intro sums_unique [symmetric] sums_minus summable_sums)
   1.247 +
   1.248 +lemma sums_group:
   1.249 +     "[|summable f; 0 < k |] ==> (%n. setsum f {n*k..<n*k+k}) sums (suminf f)"
   1.250 +apply (drule summable_sums)
   1.251 +apply (simp only: sums_def sumr_group)
   1.252 +apply (unfold LIMSEQ_def, safe)
   1.253 +apply (drule_tac x="r" in spec, safe)
   1.254 +apply (rule_tac x="no" in exI, safe)
   1.255 +apply (drule_tac x="n*k" in spec)
   1.256 +apply (erule mp)
   1.257 +apply (erule order_trans)
   1.258 +apply simp
   1.259 +done
   1.260 +
   1.261 +text{*A summable series of positive terms has limit that is at least as
   1.262 +great as any partial sum.*}
   1.263 +
   1.264 +lemma series_pos_le:
   1.265 +  fixes f :: "nat \<Rightarrow> real"
   1.266 +  shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 \<le> f m\<rbrakk> \<Longrightarrow> setsum f {0..<n} \<le> suminf f"
   1.267 +apply (drule summable_sums)
   1.268 +apply (simp add: sums_def)
   1.269 +apply (cut_tac k = "setsum f {0..<n}" in LIMSEQ_const)
   1.270 +apply (erule LIMSEQ_le, blast)
   1.271 +apply (rule_tac x="n" in exI, clarify)
   1.272 +apply (rule setsum_mono2)
   1.273 +apply auto
   1.274 +done
   1.275 +
   1.276 +lemma series_pos_less:
   1.277 +  fixes f :: "nat \<Rightarrow> real"
   1.278 +  shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 < f m\<rbrakk> \<Longrightarrow> setsum f {0..<n} < suminf f"
   1.279 +apply (rule_tac y="setsum f {0..<Suc n}" in order_less_le_trans)
   1.280 +apply simp
   1.281 +apply (erule series_pos_le)
   1.282 +apply (simp add: order_less_imp_le)
   1.283 +done
   1.284 +
   1.285 +lemma suminf_gt_zero:
   1.286 +  fixes f :: "nat \<Rightarrow> real"
   1.287 +  shows "\<lbrakk>summable f; \<forall>n. 0 < f n\<rbrakk> \<Longrightarrow> 0 < suminf f"
   1.288 +by (drule_tac n="0" in series_pos_less, simp_all)
   1.289 +
   1.290 +lemma suminf_ge_zero:
   1.291 +  fixes f :: "nat \<Rightarrow> real"
   1.292 +  shows "\<lbrakk>summable f; \<forall>n. 0 \<le> f n\<rbrakk> \<Longrightarrow> 0 \<le> suminf f"
   1.293 +by (drule_tac n="0" in series_pos_le, simp_all)
   1.294 +
   1.295 +lemma sumr_pos_lt_pair:
   1.296 +  fixes f :: "nat \<Rightarrow> real"
   1.297 +  shows "\<lbrakk>summable f;
   1.298 +        \<forall>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\<rbrakk>
   1.299 +      \<Longrightarrow> setsum f {0..<k} < suminf f"
   1.300 +apply (subst suminf_split_initial_segment [where k="k"])
   1.301 +apply assumption
   1.302 +apply simp
   1.303 +apply (drule_tac k="k" in summable_ignore_initial_segment)
   1.304 +apply (drule_tac k="Suc (Suc 0)" in sums_group, simp)
   1.305 +apply simp
   1.306 +apply (frule sums_unique)
   1.307 +apply (drule sums_summable)
   1.308 +apply simp
   1.309 +apply (erule suminf_gt_zero)
   1.310 +apply (simp add: add_ac)
   1.311 +done
   1.312 +
   1.313 +text{*Sum of a geometric progression.*}
   1.314 +
   1.315 +lemmas sumr_geometric = geometric_sum [where 'a = real]
   1.316 +
   1.317 +lemma geometric_sums:
   1.318 +  fixes x :: "'a::{real_normed_field,recpower}"
   1.319 +  shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) sums (1 / (1 - x))"
   1.320 +proof -
   1.321 +  assume less_1: "norm x < 1"
   1.322 +  hence neq_1: "x \<noteq> 1" by auto
   1.323 +  hence neq_0: "x - 1 \<noteq> 0" by simp
   1.324 +  from less_1 have lim_0: "(\<lambda>n. x ^ n) ----> 0"
   1.325 +    by (rule LIMSEQ_power_zero)
   1.326 +  hence "(\<lambda>n. x ^ n / (x - 1) - 1 / (x - 1)) ----> 0 / (x - 1) - 1 / (x - 1)"
   1.327 +    using neq_0 by (intro LIMSEQ_divide LIMSEQ_diff LIMSEQ_const)
   1.328 +  hence "(\<lambda>n. (x ^ n - 1) / (x - 1)) ----> 1 / (1 - x)"
   1.329 +    by (simp add: nonzero_minus_divide_right [OF neq_0] diff_divide_distrib)
   1.330 +  thus "(\<lambda>n. x ^ n) sums (1 / (1 - x))"
   1.331 +    by (simp add: sums_def geometric_sum neq_1)
   1.332 +qed
   1.333 +
   1.334 +lemma summable_geometric:
   1.335 +  fixes x :: "'a::{real_normed_field,recpower}"
   1.336 +  shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)"
   1.337 +by (rule geometric_sums [THEN sums_summable])
   1.338 +
   1.339 +text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
   1.340 +
   1.341 +lemma summable_convergent_sumr_iff:
   1.342 + "summable f = convergent (%n. setsum f {0..<n})"
   1.343 +by (simp add: summable_def sums_def convergent_def)
   1.344 +
   1.345 +lemma summable_LIMSEQ_zero: "summable f \<Longrightarrow> f ----> 0"
   1.346 +apply (drule summable_convergent_sumr_iff [THEN iffD1])
   1.347 +apply (drule convergent_Cauchy)
   1.348 +apply (simp only: Cauchy_def LIMSEQ_def, safe)
   1.349 +apply (drule_tac x="r" in spec, safe)
   1.350 +apply (rule_tac x="M" in exI, safe)
   1.351 +apply (drule_tac x="Suc n" in spec, simp)
   1.352 +apply (drule_tac x="n" in spec, simp)
   1.353 +done
   1.354 +
   1.355 +lemma summable_Cauchy:
   1.356 +     "summable (f::nat \<Rightarrow> 'a::banach) =  
   1.357 +      (\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. norm (setsum f {m..<n}) < e)"
   1.358 +apply (simp only: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_def, safe)
   1.359 +apply (drule spec, drule (1) mp)
   1.360 +apply (erule exE, rule_tac x="M" in exI, clarify)
   1.361 +apply (rule_tac x="m" and y="n" in linorder_le_cases)
   1.362 +apply (frule (1) order_trans)
   1.363 +apply (drule_tac x="n" in spec, drule (1) mp)
   1.364 +apply (drule_tac x="m" in spec, drule (1) mp)
   1.365 +apply (simp add: setsum_diff [symmetric])
   1.366 +apply simp
   1.367 +apply (drule spec, drule (1) mp)
   1.368 +apply (erule exE, rule_tac x="N" in exI, clarify)
   1.369 +apply (rule_tac x="m" and y="n" in linorder_le_cases)
   1.370 +apply (subst norm_minus_commute)
   1.371 +apply (simp add: setsum_diff [symmetric])
   1.372 +apply (simp add: setsum_diff [symmetric])
   1.373 +done
   1.374 +
   1.375 +text{*Comparison test*}
   1.376 +
   1.377 +lemma norm_setsum:
   1.378 +  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   1.379 +  shows "norm (setsum f A) \<le> (\<Sum>i\<in>A. norm (f i))"
   1.380 +apply (case_tac "finite A")
   1.381 +apply (erule finite_induct)
   1.382 +apply simp
   1.383 +apply simp
   1.384 +apply (erule order_trans [OF norm_triangle_ineq add_left_mono])
   1.385 +apply simp
   1.386 +done
   1.387 +
   1.388 +lemma summable_comparison_test:
   1.389 +  fixes f :: "nat \<Rightarrow> 'a::banach"
   1.390 +  shows "\<lbrakk>\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n; summable g\<rbrakk> \<Longrightarrow> summable f"
   1.391 +apply (simp add: summable_Cauchy, safe)
   1.392 +apply (drule_tac x="e" in spec, safe)
   1.393 +apply (rule_tac x = "N + Na" in exI, safe)
   1.394 +apply (rotate_tac 2)
   1.395 +apply (drule_tac x = m in spec)
   1.396 +apply (auto, rotate_tac 2, drule_tac x = n in spec)
   1.397 +apply (rule_tac y = "\<Sum>k=m..<n. norm (f k)" in order_le_less_trans)
   1.398 +apply (rule norm_setsum)
   1.399 +apply (rule_tac y = "setsum g {m..<n}" in order_le_less_trans)
   1.400 +apply (auto intro: setsum_mono simp add: abs_less_iff)
   1.401 +done
   1.402 +
   1.403 +lemma summable_norm_comparison_test:
   1.404 +  fixes f :: "nat \<Rightarrow> 'a::banach"
   1.405 +  shows "\<lbrakk>\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n; summable g\<rbrakk>
   1.406 +         \<Longrightarrow> summable (\<lambda>n. norm (f n))"
   1.407 +apply (rule summable_comparison_test)
   1.408 +apply (auto)
   1.409 +done
   1.410 +
   1.411 +lemma summable_rabs_comparison_test:
   1.412 +  fixes f :: "nat \<Rightarrow> real"
   1.413 +  shows "\<lbrakk>\<exists>N. \<forall>n\<ge>N. \<bar>f n\<bar> \<le> g n; summable g\<rbrakk> \<Longrightarrow> summable (\<lambda>n. \<bar>f n\<bar>)"
   1.414 +apply (rule summable_comparison_test)
   1.415 +apply (auto)
   1.416 +done
   1.417 +
   1.418 +text{*Summability of geometric series for real algebras*}
   1.419 +
   1.420 +lemma complete_algebra_summable_geometric:
   1.421 +  fixes x :: "'a::{real_normed_algebra_1,banach,recpower}"
   1.422 +  shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)"
   1.423 +proof (rule summable_comparison_test)
   1.424 +  show "\<exists>N. \<forall>n\<ge>N. norm (x ^ n) \<le> norm x ^ n"
   1.425 +    by (simp add: norm_power_ineq)
   1.426 +  show "norm x < 1 \<Longrightarrow> summable (\<lambda>n. norm x ^ n)"
   1.427 +    by (simp add: summable_geometric)
   1.428 +qed
   1.429 +
   1.430 +text{*Limit comparison property for series (c.f. jrh)*}
   1.431 +
   1.432 +lemma summable_le:
   1.433 +  fixes f g :: "nat \<Rightarrow> real"
   1.434 +  shows "\<lbrakk>\<forall>n. f n \<le> g n; summable f; summable g\<rbrakk> \<Longrightarrow> suminf f \<le> suminf g"
   1.435 +apply (drule summable_sums)+
   1.436 +apply (simp only: sums_def, erule (1) LIMSEQ_le)
   1.437 +apply (rule exI)
   1.438 +apply (auto intro!: setsum_mono)
   1.439 +done
   1.440 +
   1.441 +lemma summable_le2:
   1.442 +  fixes f g :: "nat \<Rightarrow> real"
   1.443 +  shows "\<lbrakk>\<forall>n. \<bar>f n\<bar> \<le> g n; summable g\<rbrakk> \<Longrightarrow> summable f \<and> suminf f \<le> suminf g"
   1.444 +apply (subgoal_tac "summable f")
   1.445 +apply (auto intro!: summable_le)
   1.446 +apply (simp add: abs_le_iff)
   1.447 +apply (rule_tac g="g" in summable_comparison_test, simp_all)
   1.448 +done
   1.449 +
   1.450 +(* specialisation for the common 0 case *)
   1.451 +lemma suminf_0_le:
   1.452 +  fixes f::"nat\<Rightarrow>real"
   1.453 +  assumes gt0: "\<forall>n. 0 \<le> f n" and sm: "summable f"
   1.454 +  shows "0 \<le> suminf f"
   1.455 +proof -
   1.456 +  let ?g = "(\<lambda>n. (0::real))"
   1.457 +  from gt0 have "\<forall>n. ?g n \<le> f n" by simp
   1.458 +  moreover have "summable ?g" by (rule summable_zero)
   1.459 +  moreover from sm have "summable f" .
   1.460 +  ultimately have "suminf ?g \<le> suminf f" by (rule summable_le)
   1.461 +  then show "0 \<le> suminf f" by (simp add: suminf_zero)
   1.462 +qed 
   1.463 +
   1.464 +
   1.465 +text{*Absolute convergence imples normal convergence*}
   1.466 +lemma summable_norm_cancel:
   1.467 +  fixes f :: "nat \<Rightarrow> 'a::banach"
   1.468 +  shows "summable (\<lambda>n. norm (f n)) \<Longrightarrow> summable f"
   1.469 +apply (simp only: summable_Cauchy, safe)
   1.470 +apply (drule_tac x="e" in spec, safe)
   1.471 +apply (rule_tac x="N" in exI, safe)
   1.472 +apply (drule_tac x="m" in spec, safe)
   1.473 +apply (rule order_le_less_trans [OF norm_setsum])
   1.474 +apply (rule order_le_less_trans [OF abs_ge_self])
   1.475 +apply simp
   1.476 +done
   1.477 +
   1.478 +lemma summable_rabs_cancel:
   1.479 +  fixes f :: "nat \<Rightarrow> real"
   1.480 +  shows "summable (\<lambda>n. \<bar>f n\<bar>) \<Longrightarrow> summable f"
   1.481 +by (rule summable_norm_cancel, simp)
   1.482 +
   1.483 +text{*Absolute convergence of series*}
   1.484 +lemma summable_norm:
   1.485 +  fixes f :: "nat \<Rightarrow> 'a::banach"
   1.486 +  shows "summable (\<lambda>n. norm (f n)) \<Longrightarrow> norm (suminf f) \<le> (\<Sum>n. norm (f n))"
   1.487 +by (auto intro: LIMSEQ_le LIMSEQ_norm summable_norm_cancel
   1.488 +                summable_sumr_LIMSEQ_suminf norm_setsum)
   1.489 +
   1.490 +lemma summable_rabs:
   1.491 +  fixes f :: "nat \<Rightarrow> real"
   1.492 +  shows "summable (\<lambda>n. \<bar>f n\<bar>) \<Longrightarrow> \<bar>suminf f\<bar> \<le> (\<Sum>n. \<bar>f n\<bar>)"
   1.493 +by (fold real_norm_def, rule summable_norm)
   1.494 +
   1.495 +subsection{* The Ratio Test*}
   1.496 +
   1.497 +lemma norm_ratiotest_lemma:
   1.498 +  fixes x y :: "'a::real_normed_vector"
   1.499 +  shows "\<lbrakk>c \<le> 0; norm x \<le> c * norm y\<rbrakk> \<Longrightarrow> x = 0"
   1.500 +apply (subgoal_tac "norm x \<le> 0", simp)
   1.501 +apply (erule order_trans)
   1.502 +apply (simp add: mult_le_0_iff)
   1.503 +done
   1.504 +
   1.505 +lemma rabs_ratiotest_lemma: "[| c \<le> 0; abs x \<le> c * abs y |] ==> x = (0::real)"
   1.506 +by (erule norm_ratiotest_lemma, simp)
   1.507 +
   1.508 +lemma le_Suc_ex: "(k::nat) \<le> l ==> (\<exists>n. l = k + n)"
   1.509 +apply (drule le_imp_less_or_eq)
   1.510 +apply (auto dest: less_imp_Suc_add)
   1.511 +done
   1.512 +
   1.513 +lemma le_Suc_ex_iff: "((k::nat) \<le> l) = (\<exists>n. l = k + n)"
   1.514 +by (auto simp add: le_Suc_ex)
   1.515 +
   1.516 +(*All this trouble just to get 0<c *)
   1.517 +lemma ratio_test_lemma2:
   1.518 +  fixes f :: "nat \<Rightarrow> 'a::banach"
   1.519 +  shows "\<lbrakk>\<forall>n\<ge>N. norm (f (Suc n)) \<le> c * norm (f n)\<rbrakk> \<Longrightarrow> 0 < c \<or> summable f"
   1.520 +apply (simp (no_asm) add: linorder_not_le [symmetric])
   1.521 +apply (simp add: summable_Cauchy)
   1.522 +apply (safe, subgoal_tac "\<forall>n. N < n --> f (n) = 0")
   1.523 + prefer 2
   1.524 + apply clarify
   1.525 + apply(erule_tac x = "n - 1" in allE)
   1.526 + apply (simp add:diff_Suc split:nat.splits)
   1.527 + apply (blast intro: norm_ratiotest_lemma)
   1.528 +apply (rule_tac x = "Suc N" in exI, clarify)
   1.529 +apply(simp cong:setsum_ivl_cong)
   1.530 +done
   1.531 +
   1.532 +lemma ratio_test:
   1.533 +  fixes f :: "nat \<Rightarrow> 'a::banach"
   1.534 +  shows "\<lbrakk>c < 1; \<forall>n\<ge>N. norm (f (Suc n)) \<le> c * norm (f n)\<rbrakk> \<Longrightarrow> summable f"
   1.535 +apply (frule ratio_test_lemma2, auto)
   1.536 +apply (rule_tac g = "%n. (norm (f N) / (c ^ N))*c ^ n" 
   1.537 +       in summable_comparison_test)
   1.538 +apply (rule_tac x = N in exI, safe)
   1.539 +apply (drule le_Suc_ex_iff [THEN iffD1])
   1.540 +apply (auto simp add: power_add field_power_not_zero)
   1.541 +apply (induct_tac "na", auto)
   1.542 +apply (rule_tac y = "c * norm (f (N + n))" in order_trans)
   1.543 +apply (auto intro: mult_right_mono simp add: summable_def)
   1.544 +apply (simp add: mult_ac)
   1.545 +apply (rule_tac x = "norm (f N) * (1/ (1 - c)) / (c ^ N)" in exI)
   1.546 +apply (rule sums_divide) 
   1.547 +apply (rule sums_mult)
   1.548 +apply (auto intro!: geometric_sums)
   1.549 +done
   1.550 +
   1.551 +subsection {* Cauchy Product Formula *}
   1.552 +
   1.553 +(* Proof based on Analysis WebNotes: Chapter 07, Class 41
   1.554 +http://www.math.unl.edu/~webnotes/classes/class41/prp77.htm *)
   1.555 +
   1.556 +lemma setsum_triangle_reindex:
   1.557 +  fixes n :: nat
   1.558 +  shows "(\<Sum>(i,j)\<in>{(i,j). i+j < n}. f i j) = (\<Sum>k=0..<n. \<Sum>i=0..k. f i (k - i))"
   1.559 +proof -
   1.560 +  have "(\<Sum>(i, j)\<in>{(i, j). i + j < n}. f i j) =
   1.561 +    (\<Sum>(k, i)\<in>(SIGMA k:{0..<n}. {0..k}). f i (k - i))"
   1.562 +  proof (rule setsum_reindex_cong)
   1.563 +    show "inj_on (\<lambda>(k,i). (i, k - i)) (SIGMA k:{0..<n}. {0..k})"
   1.564 +      by (rule inj_on_inverseI [where g="\<lambda>(i,j). (i+j, i)"], auto)
   1.565 +    show "{(i,j). i + j < n} = (\<lambda>(k,i). (i, k - i)) ` (SIGMA k:{0..<n}. {0..k})"
   1.566 +      by (safe, rule_tac x="(a+b,a)" in image_eqI, auto)
   1.567 +    show "\<And>a. (\<lambda>(k, i). f i (k - i)) a = split f ((\<lambda>(k, i). (i, k - i)) a)"
   1.568 +      by clarify
   1.569 +  qed
   1.570 +  thus ?thesis by (simp add: setsum_Sigma)
   1.571 +qed
   1.572 +
   1.573 +lemma Cauchy_product_sums:
   1.574 +  fixes a b :: "nat \<Rightarrow> 'a::{real_normed_algebra,banach}"
   1.575 +  assumes a: "summable (\<lambda>k. norm (a k))"
   1.576 +  assumes b: "summable (\<lambda>k. norm (b k))"
   1.577 +  shows "(\<lambda>k. \<Sum>i=0..k. a i * b (k - i)) sums ((\<Sum>k. a k) * (\<Sum>k. b k))"
   1.578 +proof -
   1.579 +  let ?S1 = "\<lambda>n::nat. {0..<n} \<times> {0..<n}"
   1.580 +  let ?S2 = "\<lambda>n::nat. {(i,j). i + j < n}"
   1.581 +  have S1_mono: "\<And>m n. m \<le> n \<Longrightarrow> ?S1 m \<subseteq> ?S1 n" by auto
   1.582 +  have S2_le_S1: "\<And>n. ?S2 n \<subseteq> ?S1 n" by auto
   1.583 +  have S1_le_S2: "\<And>n. ?S1 (n div 2) \<subseteq> ?S2 n" by auto
   1.584 +  have finite_S1: "\<And>n. finite (?S1 n)" by simp
   1.585 +  with S2_le_S1 have finite_S2: "\<And>n. finite (?S2 n)" by (rule finite_subset)
   1.586 +
   1.587 +  let ?g = "\<lambda>(i,j). a i * b j"
   1.588 +  let ?f = "\<lambda>(i,j). norm (a i) * norm (b j)"
   1.589 +  have f_nonneg: "\<And>x. 0 \<le> ?f x"
   1.590 +    by (auto simp add: mult_nonneg_nonneg)
   1.591 +  hence norm_setsum_f: "\<And>A. norm (setsum ?f A) = setsum ?f A"
   1.592 +    unfolding real_norm_def
   1.593 +    by (simp only: abs_of_nonneg setsum_nonneg [rule_format])
   1.594 +
   1.595 +  have "(\<lambda>n. (\<Sum>k=0..<n. a k) * (\<Sum>k=0..<n. b k))
   1.596 +           ----> (\<Sum>k. a k) * (\<Sum>k. b k)"
   1.597 +    by (intro LIMSEQ_mult summable_sumr_LIMSEQ_suminf
   1.598 +        summable_norm_cancel [OF a] summable_norm_cancel [OF b])
   1.599 +  hence 1: "(\<lambda>n. setsum ?g (?S1 n)) ----> (\<Sum>k. a k) * (\<Sum>k. b k)"
   1.600 +    by (simp only: setsum_product setsum_Sigma [rule_format]
   1.601 +                   finite_atLeastLessThan)
   1.602 +
   1.603 +  have "(\<lambda>n. (\<Sum>k=0..<n. norm (a k)) * (\<Sum>k=0..<n. norm (b k)))
   1.604 +       ----> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))"
   1.605 +    using a b by (intro LIMSEQ_mult summable_sumr_LIMSEQ_suminf)
   1.606 +  hence "(\<lambda>n. setsum ?f (?S1 n)) ----> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))"
   1.607 +    by (simp only: setsum_product setsum_Sigma [rule_format]
   1.608 +                   finite_atLeastLessThan)
   1.609 +  hence "convergent (\<lambda>n. setsum ?f (?S1 n))"
   1.610 +    by (rule convergentI)
   1.611 +  hence Cauchy: "Cauchy (\<lambda>n. setsum ?f (?S1 n))"
   1.612 +    by (rule convergent_Cauchy)
   1.613 +  have "Zseq (\<lambda>n. setsum ?f (?S1 n - ?S2 n))"
   1.614 +  proof (rule ZseqI, simp only: norm_setsum_f)
   1.615 +    fix r :: real
   1.616 +    assume r: "0 < r"
   1.617 +    from CauchyD [OF Cauchy r] obtain N
   1.618 +    where "\<forall>m\<ge>N. \<forall>n\<ge>N. norm (setsum ?f (?S1 m) - setsum ?f (?S1 n)) < r" ..
   1.619 +    hence "\<And>m n. \<lbrakk>N \<le> n; n \<le> m\<rbrakk> \<Longrightarrow> norm (setsum ?f (?S1 m - ?S1 n)) < r"
   1.620 +      by (simp only: setsum_diff finite_S1 S1_mono)
   1.621 +    hence N: "\<And>m n. \<lbrakk>N \<le> n; n \<le> m\<rbrakk> \<Longrightarrow> setsum ?f (?S1 m - ?S1 n) < r"
   1.622 +      by (simp only: norm_setsum_f)
   1.623 +    show "\<exists>N. \<forall>n\<ge>N. setsum ?f (?S1 n - ?S2 n) < r"
   1.624 +    proof (intro exI allI impI)
   1.625 +      fix n assume "2 * N \<le> n"
   1.626 +      hence n: "N \<le> n div 2" by simp
   1.627 +      have "setsum ?f (?S1 n - ?S2 n) \<le> setsum ?f (?S1 n - ?S1 (n div 2))"
   1.628 +        by (intro setsum_mono2 finite_Diff finite_S1 f_nonneg
   1.629 +                  Diff_mono subset_refl S1_le_S2)
   1.630 +      also have "\<dots> < r"
   1.631 +        using n div_le_dividend by (rule N)
   1.632 +      finally show "setsum ?f (?S1 n - ?S2 n) < r" .
   1.633 +    qed
   1.634 +  qed
   1.635 +  hence "Zseq (\<lambda>n. setsum ?g (?S1 n - ?S2 n))"
   1.636 +    apply (rule Zseq_le [rule_format])
   1.637 +    apply (simp only: norm_setsum_f)
   1.638 +    apply (rule order_trans [OF norm_setsum setsum_mono])
   1.639 +    apply (auto simp add: norm_mult_ineq)
   1.640 +    done
   1.641 +  hence 2: "(\<lambda>n. setsum ?g (?S1 n) - setsum ?g (?S2 n)) ----> 0"
   1.642 +    by (simp only: LIMSEQ_Zseq_iff setsum_diff finite_S1 S2_le_S1 diff_0_right)
   1.643 +
   1.644 +  with 1 have "(\<lambda>n. setsum ?g (?S2 n)) ----> (\<Sum>k. a k) * (\<Sum>k. b k)"
   1.645 +    by (rule LIMSEQ_diff_approach_zero2)
   1.646 +  thus ?thesis by (simp only: sums_def setsum_triangle_reindex)
   1.647 +qed
   1.648 +
   1.649 +lemma Cauchy_product:
   1.650 +  fixes a b :: "nat \<Rightarrow> 'a::{real_normed_algebra,banach}"
   1.651 +  assumes a: "summable (\<lambda>k. norm (a k))"
   1.652 +  assumes b: "summable (\<lambda>k. norm (b k))"
   1.653 +  shows "(\<Sum>k. a k) * (\<Sum>k. b k) = (\<Sum>k. \<Sum>i=0..k. a i * b (k - i))"
   1.654 +using a b
   1.655 +by (rule Cauchy_product_sums [THEN sums_unique])
   1.656 +
   1.657 +end