src/HOL/Series.thy
changeset 29803 c56a5571f60a
parent 29197 6d4cb27ed19c
child 30082 43c5b7bfc791
     1.1 --- a/src/HOL/Series.thy	Wed Feb 04 18:10:07 2009 +0100
     1.2 +++ b/src/HOL/Series.thy	Thu Feb 05 11:34:42 2009 +0100
     1.3 @@ -140,6 +140,24 @@
     1.4      suminf f = (SUM i = 0..< k. f i) + suminf (%n. f(n + k))"
     1.5  by (auto simp add: suminf_minus_initial_segment)
     1.6  
     1.7 +lemma suminf_exist_split: fixes r :: real assumes "0 < r" and "summable a"
     1.8 +  shows "\<exists> N. \<forall> n \<ge> N. \<bar> \<Sum> i. a (i + n) \<bar> < r"
     1.9 +proof -
    1.10 +  from LIMSEQ_D[OF summable_sumr_LIMSEQ_suminf[OF `summable a`] `0 < r`]
    1.11 +  obtain N :: nat where "\<forall> n \<ge> N. norm (setsum a {0..<n} - suminf a) < r" by auto
    1.12 +  thus ?thesis unfolding suminf_minus_initial_segment[OF `summable a` refl] abs_minus_commute real_norm_def
    1.13 +    by auto
    1.14 +qed
    1.15 +
    1.16 +lemma sums_Suc: assumes sumSuc: "(\<lambda> n. f (Suc n)) sums l" shows "f sums (l + f 0)"
    1.17 +proof -
    1.18 +  from sumSuc[unfolded sums_def]
    1.19 +  have "(\<lambda>i. \<Sum>n = Suc 0..<Suc i. f n) ----> l" unfolding setsum_reindex[OF inj_Suc] image_Suc_atLeastLessThan[symmetric] comp_def .
    1.20 +  from LIMSEQ_add_const[OF this, where b="f 0"] 
    1.21 +  have "(\<lambda>i. \<Sum>n = 0..<Suc i. f n) ----> l + f 0" unfolding add_commute setsum_head_upt_Suc[OF zero_less_Suc] .
    1.22 +  thus ?thesis unfolding sums_def by (rule LIMSEQ_imp_Suc)
    1.23 +qed
    1.24 +
    1.25  lemma series_zero: 
    1.26       "(\<forall>m. n \<le> m --> f(m) = 0) ==> f sums (setsum f {0..<n})"
    1.27  apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe)