137 done |
137 done |
138 |
138 |
139 lemma suminf_split_initial_segment: "summable f ==> |
139 lemma suminf_split_initial_segment: "summable f ==> |
140 suminf f = (SUM i = 0..< k. f i) + suminf (%n. f(n + k))" |
140 suminf f = (SUM i = 0..< k. f i) + suminf (%n. f(n + k))" |
141 by (auto simp add: suminf_minus_initial_segment) |
141 by (auto simp add: suminf_minus_initial_segment) |
|
142 |
|
143 lemma suminf_exist_split: fixes r :: real assumes "0 < r" and "summable a" |
|
144 shows "\<exists> N. \<forall> n \<ge> N. \<bar> \<Sum> i. a (i + n) \<bar> < r" |
|
145 proof - |
|
146 from LIMSEQ_D[OF summable_sumr_LIMSEQ_suminf[OF `summable a`] `0 < r`] |
|
147 obtain N :: nat where "\<forall> n \<ge> N. norm (setsum a {0..<n} - suminf a) < r" by auto |
|
148 thus ?thesis unfolding suminf_minus_initial_segment[OF `summable a` refl] abs_minus_commute real_norm_def |
|
149 by auto |
|
150 qed |
|
151 |
|
152 lemma sums_Suc: assumes sumSuc: "(\<lambda> n. f (Suc n)) sums l" shows "f sums (l + f 0)" |
|
153 proof - |
|
154 from sumSuc[unfolded sums_def] |
|
155 have "(\<lambda>i. \<Sum>n = Suc 0..<Suc i. f n) ----> l" unfolding setsum_reindex[OF inj_Suc] image_Suc_atLeastLessThan[symmetric] comp_def . |
|
156 from LIMSEQ_add_const[OF this, where b="f 0"] |
|
157 have "(\<lambda>i. \<Sum>n = 0..<Suc i. f n) ----> l + f 0" unfolding add_commute setsum_head_upt_Suc[OF zero_less_Suc] . |
|
158 thus ?thesis unfolding sums_def by (rule LIMSEQ_imp_Suc) |
|
159 qed |
142 |
160 |
143 lemma series_zero: |
161 lemma series_zero: |
144 "(\<forall>m. n \<le> m --> f(m) = 0) ==> f sums (setsum f {0..<n})" |
162 "(\<forall>m. n \<le> m --> f(m) = 0) ==> f sums (setsum f {0..<n})" |
145 apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe) |
163 apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe) |
146 apply (rule_tac x = n in exI) |
164 apply (rule_tac x = n in exI) |