145 apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe) |
145 apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe) |
146 apply (rule_tac x = n in exI) |
146 apply (rule_tac x = n in exI) |
147 apply (clarsimp simp add:setsum_diff[symmetric] cong:setsum_ivl_cong) |
147 apply (clarsimp simp add:setsum_diff[symmetric] cong:setsum_ivl_cong) |
148 done |
148 done |
149 |
149 |
150 lemma sums_zero: "(%n. 0) sums 0"; |
150 lemma sums_zero: "(\<lambda>n. 0) sums 0" |
151 apply (unfold sums_def); |
151 unfolding sums_def by (simp add: LIMSEQ_const) |
152 apply simp; |
152 |
153 apply (rule LIMSEQ_const); |
153 lemma summable_zero: "summable (\<lambda>n. 0)" |
154 done; |
154 by (rule sums_zero [THEN sums_summable]) |
155 |
155 |
156 lemma summable_zero: "summable (%n. 0)"; |
156 lemma suminf_zero: "suminf (\<lambda>n. 0) = 0" |
157 apply (rule sums_summable); |
157 by (rule sums_zero [THEN sums_unique, symmetric]) |
158 apply (rule sums_zero); |
|
159 done; |
|
160 |
|
161 lemma suminf_zero: "suminf (%n. 0) = 0"; |
|
162 apply (rule sym); |
|
163 apply (rule sums_unique); |
|
164 apply (rule sums_zero); |
|
165 done; |
|
166 |
158 |
167 lemma (in bounded_linear) sums: |
159 lemma (in bounded_linear) sums: |
168 "(\<lambda>n. X n) sums a \<Longrightarrow> (\<lambda>n. f (X n)) sums (f a)" |
160 "(\<lambda>n. X n) sums a \<Longrightarrow> (\<lambda>n. f (X n)) sums (f a)" |
169 unfolding sums_def by (drule LIMSEQ, simp only: setsum) |
161 unfolding sums_def by (drule LIMSEQ, simp only: setsum) |
170 |
162 |
172 "summable (\<lambda>n. X n) \<Longrightarrow> summable (\<lambda>n. f (X n))" |
164 "summable (\<lambda>n. X n) \<Longrightarrow> summable (\<lambda>n. f (X n))" |
173 unfolding summable_def by (auto intro: sums) |
165 unfolding summable_def by (auto intro: sums) |
174 |
166 |
175 lemma (in bounded_linear) suminf: |
167 lemma (in bounded_linear) suminf: |
176 "summable (\<lambda>n. X n) \<Longrightarrow> f (\<Sum>n. X n) = (\<Sum>n. f (X n))" |
168 "summable (\<lambda>n. X n) \<Longrightarrow> f (\<Sum>n. X n) = (\<Sum>n. f (X n))" |
177 by (rule summable_sums [THEN sums, THEN sums_unique]) |
169 by (intro sums_unique sums summable_sums) |
178 |
170 |
179 lemma sums_mult: |
171 lemma sums_mult: |
180 fixes c :: "'a::real_normed_algebra" |
172 fixes c :: "'a::real_normed_algebra" |
181 shows "f sums a \<Longrightarrow> (\<lambda>n. c * f n) sums (c * a)" |
173 shows "f sums a \<Longrightarrow> (\<lambda>n. c * f n) sums (c * a)" |
182 by (auto simp add: sums_def setsum_right_distrib [symmetric] |
174 by (rule bounded_linear_mult_right.sums) |
183 intro!: LIMSEQ_mult intro: LIMSEQ_const) |
|
184 |
175 |
185 lemma summable_mult: |
176 lemma summable_mult: |
186 fixes c :: "'a::real_normed_algebra" |
177 fixes c :: "'a::real_normed_algebra" |
187 shows "summable f \<Longrightarrow> summable (%n. c * f n)"; |
178 shows "summable f \<Longrightarrow> summable (%n. c * f n)" |
188 apply (unfold summable_def); |
179 by (rule bounded_linear_mult_right.summable) |
189 apply (auto intro: sums_mult); |
|
190 done; |
|
191 |
180 |
192 lemma suminf_mult: |
181 lemma suminf_mult: |
193 fixes c :: "'a::real_normed_algebra" |
182 fixes c :: "'a::real_normed_algebra" |
194 shows "summable f \<Longrightarrow> suminf (\<lambda>n. c * f n) = c * suminf f"; |
183 shows "summable f \<Longrightarrow> suminf (\<lambda>n. c * f n) = c * suminf f"; |
195 apply (rule sym); |
184 by (rule bounded_linear_mult_right.suminf [symmetric]) |
196 apply (rule sums_unique); |
|
197 apply (rule sums_mult); |
|
198 apply (erule summable_sums); |
|
199 done; |
|
200 |
185 |
201 lemma sums_mult2: |
186 lemma sums_mult2: |
202 fixes c :: "'a::real_normed_algebra" |
187 fixes c :: "'a::real_normed_algebra" |
203 shows "f sums a \<Longrightarrow> (\<lambda>n. f n * c) sums (a * c)" |
188 shows "f sums a \<Longrightarrow> (\<lambda>n. f n * c) sums (a * c)" |
204 by (auto simp add: sums_def setsum_left_distrib [symmetric] |
189 by (rule bounded_linear_mult_left.sums) |
205 intro!: LIMSEQ_mult LIMSEQ_const) |
|
206 |
190 |
207 lemma summable_mult2: |
191 lemma summable_mult2: |
208 fixes c :: "'a::real_normed_algebra" |
192 fixes c :: "'a::real_normed_algebra" |
209 shows "summable f \<Longrightarrow> summable (\<lambda>n. f n * c)" |
193 shows "summable f \<Longrightarrow> summable (\<lambda>n. f n * c)" |
210 apply (unfold summable_def) |
194 by (rule bounded_linear_mult_left.summable) |
211 apply (auto intro: sums_mult2) |
|
212 done |
|
213 |
195 |
214 lemma suminf_mult2: |
196 lemma suminf_mult2: |
215 fixes c :: "'a::real_normed_algebra" |
197 fixes c :: "'a::real_normed_algebra" |
216 shows "summable f \<Longrightarrow> suminf f * c = (\<Sum>n. f n * c)" |
198 shows "summable f \<Longrightarrow> suminf f * c = (\<Sum>n. f n * c)" |
217 by (auto intro!: sums_unique sums_mult2 summable_sums) |
199 by (rule bounded_linear_mult_left.suminf) |
218 |
200 |
219 lemma sums_divide: |
201 lemma sums_divide: |
220 fixes c :: "'a::real_normed_field" |
202 fixes c :: "'a::real_normed_field" |
221 shows "f sums a \<Longrightarrow> (\<lambda>n. f n / c) sums (a / c)" |
203 shows "f sums a \<Longrightarrow> (\<lambda>n. f n / c) sums (a / c)" |
222 by (simp add: divide_inverse sums_mult2) |
204 by (rule bounded_linear_divide.sums) |
223 |
205 |
224 lemma summable_divide: |
206 lemma summable_divide: |
225 fixes c :: "'a::real_normed_field" |
207 fixes c :: "'a::real_normed_field" |
226 shows "summable f \<Longrightarrow> summable (\<lambda>n. f n / c)" |
208 shows "summable f \<Longrightarrow> summable (\<lambda>n. f n / c)" |
227 apply (unfold summable_def); |
209 by (rule bounded_linear_divide.summable) |
228 apply (auto intro: sums_divide); |
|
229 done; |
|
230 |
210 |
231 lemma suminf_divide: |
211 lemma suminf_divide: |
232 fixes c :: "'a::real_normed_field" |
212 fixes c :: "'a::real_normed_field" |
233 shows "summable f \<Longrightarrow> suminf (\<lambda>n. f n / c) = suminf f / c" |
213 shows "summable f \<Longrightarrow> suminf (\<lambda>n. f n / c) = suminf f / c" |
234 apply (rule sym); |
214 by (rule bounded_linear_divide.suminf [symmetric]) |
235 apply (rule sums_unique); |
215 |
236 apply (rule sums_divide); |
216 lemma sums_add: "\<lbrakk>X sums a; Y sums b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n + Y n) sums (a + b)" |
237 apply (erule summable_sums); |
217 unfolding sums_def by (simp add: setsum_addf LIMSEQ_add) |
238 done; |
218 |
239 |
219 lemma summable_add: "\<lbrakk>summable X; summable Y\<rbrakk> \<Longrightarrow> summable (\<lambda>n. X n + Y n)" |
240 lemma sums_add: "[| x sums x0; y sums y0 |] ==> (%n. x n + y n) sums (x0+y0)" |
220 unfolding summable_def by (auto intro: sums_add) |
241 by (auto simp add: sums_def setsum_addf intro: LIMSEQ_add) |
|
242 |
|
243 lemma summable_add: "summable f ==> summable g ==> summable (%x. f x + g x)"; |
|
244 apply (unfold summable_def); |
|
245 apply clarify; |
|
246 apply (rule exI); |
|
247 apply (erule sums_add); |
|
248 apply assumption; |
|
249 done; |
|
250 |
221 |
251 lemma suminf_add: |
222 lemma suminf_add: |
252 "[| summable f; summable g |] |
223 "\<lbrakk>summable X; summable Y\<rbrakk> \<Longrightarrow> suminf X + suminf Y = (\<Sum>n. X n + Y n)" |
253 ==> suminf f + suminf g = (\<Sum>n. f n + g n)" |
224 by (intro sums_unique sums_add summable_sums) |
254 by (auto intro!: sums_add sums_unique summable_sums) |
225 |
255 |
226 lemma sums_diff: "\<lbrakk>X sums a; Y sums b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n - Y n) sums (a - b)" |
256 lemma sums_diff: "[| x sums x0; y sums y0 |] ==> (%n. x n - y n) sums (x0-y0)" |
227 unfolding sums_def by (simp add: setsum_subtractf LIMSEQ_diff) |
257 by (auto simp add: sums_def setsum_subtractf intro: LIMSEQ_diff) |
228 |
258 |
229 lemma summable_diff: "\<lbrakk>summable X; summable Y\<rbrakk> \<Longrightarrow> summable (\<lambda>n. X n - Y n)" |
259 lemma summable_diff: "summable f ==> summable g ==> summable (%x. f x - g x)"; |
230 unfolding summable_def by (auto intro: sums_diff) |
260 apply (unfold summable_def); |
|
261 apply clarify; |
|
262 apply (rule exI); |
|
263 apply (erule sums_diff); |
|
264 apply assumption; |
|
265 done; |
|
266 |
231 |
267 lemma suminf_diff: |
232 lemma suminf_diff: |
268 "[| summable f; summable g |] |
233 "\<lbrakk>summable X; summable Y\<rbrakk> \<Longrightarrow> suminf X - suminf Y = (\<Sum>n. X n - Y n)" |
269 ==> suminf f - suminf g = (\<Sum>n. f n - g n)" |
234 by (intro sums_unique sums_diff summable_sums) |
270 by (auto intro!: sums_diff sums_unique summable_sums) |
235 |
271 |
236 lemma sums_minus: "X sums a ==> (\<lambda>n. - X n) sums (- a)" |
272 lemma sums_minus: "f sums s ==> (%x. - f x) sums (- s)"; |
237 unfolding sums_def by (simp add: setsum_negf LIMSEQ_minus) |
273 by (simp add: sums_def setsum_negf LIMSEQ_minus); |
238 |
274 |
239 lemma summable_minus: "summable X \<Longrightarrow> summable (\<lambda>n. - X n)" |
275 lemma summable_minus: "summable f ==> summable (%x. - f x)"; |
240 unfolding summable_def by (auto intro: sums_minus) |
276 by (auto simp add: summable_def intro: sums_minus); |
241 |
277 |
242 lemma suminf_minus: "summable X \<Longrightarrow> (\<Sum>n. - X n) = - (\<Sum>n. X n)" |
278 lemma suminf_minus: "summable f ==> suminf (%x. - f x) = - (suminf f)"; |
243 by (intro sums_unique [symmetric] sums_minus summable_sums) |
279 apply (rule sym); |
|
280 apply (rule sums_unique); |
|
281 apply (rule sums_minus); |
|
282 apply (erule summable_sums); |
|
283 done; |
|
284 |
244 |
285 lemma sums_group: |
245 lemma sums_group: |
286 "[|summable f; 0 < k |] ==> (%n. setsum f {n*k..<n*k+k}) sums (suminf f)" |
246 "[|summable f; 0 < k |] ==> (%n. setsum f {n*k..<n*k+k}) sums (suminf f)" |
287 apply (drule summable_sums) |
247 apply (drule summable_sums) |
288 apply (simp only: sums_def sumr_group) |
248 apply (simp only: sums_def sumr_group) |