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)
```