181 note setsum_const = this |
181 note setsum_const = this |
182 show ?thesis |
182 show ?thesis |
183 unfolding sums_def |
183 unfolding sums_def |
184 apply (rule LIMSEQ_offset[of _ n]) |
184 apply (rule LIMSEQ_offset[of _ n]) |
185 unfolding setsum_const |
185 unfolding setsum_const |
186 apply (rule LIMSEQ_const) |
186 apply (rule tendsto_const) |
187 done |
187 done |
188 qed |
188 qed |
189 |
189 |
190 lemma sums_zero[simp, intro]: "(\<lambda>n. 0) sums 0" |
190 lemma sums_zero[simp, intro]: "(\<lambda>n. 0) sums 0" |
191 unfolding sums_def by (simp add: LIMSEQ_const) |
191 unfolding sums_def by (simp add: tendsto_const) |
192 |
192 |
193 lemma summable_zero[simp, intro]: "summable (\<lambda>n. 0)" |
193 lemma summable_zero[simp, intro]: "summable (\<lambda>n. 0)" |
194 by (rule sums_zero [THEN sums_summable]) |
194 by (rule sums_zero [THEN sums_summable]) |
195 |
195 |
196 lemma suminf_zero[simp]: "suminf (\<lambda>n. 0::'a::{t2_space, comm_monoid_add}) = 0" |
196 lemma suminf_zero[simp]: "suminf (\<lambda>n. 0::'a::{t2_space, comm_monoid_add}) = 0" |
197 by (rule sums_zero [THEN sums_unique, symmetric]) |
197 by (rule sums_zero [THEN sums_unique, symmetric]) |
198 |
198 |
199 lemma (in bounded_linear) sums: |
199 lemma (in bounded_linear) sums: |
200 "(\<lambda>n. X n) sums a \<Longrightarrow> (\<lambda>n. f (X n)) sums (f a)" |
200 "(\<lambda>n. X n) sums a \<Longrightarrow> (\<lambda>n. f (X n)) sums (f a)" |
201 unfolding sums_def by (drule LIMSEQ, simp only: setsum) |
201 unfolding sums_def by (drule tendsto, simp only: setsum) |
202 |
202 |
203 lemma (in bounded_linear) summable: |
203 lemma (in bounded_linear) summable: |
204 "summable (\<lambda>n. X n) \<Longrightarrow> summable (\<lambda>n. f (X n))" |
204 "summable (\<lambda>n. X n) \<Longrightarrow> summable (\<lambda>n. f (X n))" |
205 unfolding summable_def by (auto intro: sums) |
205 unfolding summable_def by (auto intro: sums) |
206 |
206 |
258 by (rule bounded_linear.suminf [OF bounded_linear_divide, symmetric]) |
258 by (rule bounded_linear.suminf [OF bounded_linear_divide, symmetric]) |
259 |
259 |
260 lemma sums_add: |
260 lemma sums_add: |
261 fixes a b :: "'a::real_normed_field" |
261 fixes a b :: "'a::real_normed_field" |
262 shows "\<lbrakk>X sums a; Y sums b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n + Y n) sums (a + b)" |
262 shows "\<lbrakk>X sums a; Y sums b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n + Y n) sums (a + b)" |
263 unfolding sums_def by (simp add: setsum_addf LIMSEQ_add) |
263 unfolding sums_def by (simp add: setsum_addf tendsto_add) |
264 |
264 |
265 lemma summable_add: |
265 lemma summable_add: |
266 fixes X Y :: "nat \<Rightarrow> 'a::real_normed_field" |
266 fixes X Y :: "nat \<Rightarrow> 'a::real_normed_field" |
267 shows "\<lbrakk>summable X; summable Y\<rbrakk> \<Longrightarrow> summable (\<lambda>n. X n + Y n)" |
267 shows "\<lbrakk>summable X; summable Y\<rbrakk> \<Longrightarrow> summable (\<lambda>n. X n + Y n)" |
268 unfolding summable_def by (auto intro: sums_add) |
268 unfolding summable_def by (auto intro: sums_add) |
273 by (intro sums_unique sums_add summable_sums) |
273 by (intro sums_unique sums_add summable_sums) |
274 |
274 |
275 lemma sums_diff: |
275 lemma sums_diff: |
276 fixes X Y :: "nat \<Rightarrow> 'a::real_normed_field" |
276 fixes X Y :: "nat \<Rightarrow> 'a::real_normed_field" |
277 shows "\<lbrakk>X sums a; Y sums b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n - Y n) sums (a - b)" |
277 shows "\<lbrakk>X sums a; Y sums b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n - Y n) sums (a - b)" |
278 unfolding sums_def by (simp add: setsum_subtractf LIMSEQ_diff) |
278 unfolding sums_def by (simp add: setsum_subtractf tendsto_diff) |
279 |
279 |
280 lemma summable_diff: |
280 lemma summable_diff: |
281 fixes X Y :: "nat \<Rightarrow> 'a::real_normed_field" |
281 fixes X Y :: "nat \<Rightarrow> 'a::real_normed_field" |
282 shows "\<lbrakk>summable X; summable Y\<rbrakk> \<Longrightarrow> summable (\<lambda>n. X n - Y n)" |
282 shows "\<lbrakk>summable X; summable Y\<rbrakk> \<Longrightarrow> summable (\<lambda>n. X n - Y n)" |
283 unfolding summable_def by (auto intro: sums_diff) |
283 unfolding summable_def by (auto intro: sums_diff) |
288 by (intro sums_unique sums_diff summable_sums) |
288 by (intro sums_unique sums_diff summable_sums) |
289 |
289 |
290 lemma sums_minus: |
290 lemma sums_minus: |
291 fixes X :: "nat \<Rightarrow> 'a::real_normed_field" |
291 fixes X :: "nat \<Rightarrow> 'a::real_normed_field" |
292 shows "X sums a ==> (\<lambda>n. - X n) sums (- a)" |
292 shows "X sums a ==> (\<lambda>n. - X n) sums (- a)" |
293 unfolding sums_def by (simp add: setsum_negf LIMSEQ_minus) |
293 unfolding sums_def by (simp add: setsum_negf tendsto_minus) |
294 |
294 |
295 lemma summable_minus: |
295 lemma summable_minus: |
296 fixes X :: "nat \<Rightarrow> 'a::real_normed_field" |
296 fixes X :: "nat \<Rightarrow> 'a::real_normed_field" |
297 shows "summable X \<Longrightarrow> summable (\<lambda>n. - X n)" |
297 shows "summable X \<Longrightarrow> summable (\<lambda>n. - X n)" |
298 unfolding summable_def by (auto intro: sums_minus) |
298 unfolding summable_def by (auto intro: sums_minus) |
342 lemma series_pos_le: |
342 lemma series_pos_le: |
343 fixes f :: "nat \<Rightarrow> real" |
343 fixes f :: "nat \<Rightarrow> real" |
344 shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 \<le> f m\<rbrakk> \<Longrightarrow> setsum f {0..<n} \<le> suminf f" |
344 shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 \<le> f m\<rbrakk> \<Longrightarrow> setsum f {0..<n} \<le> suminf f" |
345 apply (drule summable_sums) |
345 apply (drule summable_sums) |
346 apply (simp add: sums_def) |
346 apply (simp add: sums_def) |
347 apply (cut_tac k = "setsum f {0..<n}" in LIMSEQ_const) |
347 apply (cut_tac k = "setsum f {0..<n}" in tendsto_const) |
348 apply (erule LIMSEQ_le, blast) |
348 apply (erule LIMSEQ_le, blast) |
349 apply (rule_tac x="n" in exI, clarify) |
349 apply (rule_tac x="n" in exI, clarify) |
350 apply (rule setsum_mono2) |
350 apply (rule setsum_mono2) |
351 apply auto |
351 apply auto |
352 done |
352 done |
401 hence neq_1: "x \<noteq> 1" by auto |
401 hence neq_1: "x \<noteq> 1" by auto |
402 hence neq_0: "x - 1 \<noteq> 0" by simp |
402 hence neq_0: "x - 1 \<noteq> 0" by simp |
403 from less_1 have lim_0: "(\<lambda>n. x ^ n) ----> 0" |
403 from less_1 have lim_0: "(\<lambda>n. x ^ n) ----> 0" |
404 by (rule LIMSEQ_power_zero) |
404 by (rule LIMSEQ_power_zero) |
405 hence "(\<lambda>n. x ^ n / (x - 1) - 1 / (x - 1)) ----> 0 / (x - 1) - 1 / (x - 1)" |
405 hence "(\<lambda>n. x ^ n / (x - 1) - 1 / (x - 1)) ----> 0 / (x - 1) - 1 / (x - 1)" |
406 using neq_0 by (intro LIMSEQ_divide LIMSEQ_diff LIMSEQ_const) |
406 using neq_0 by (intro tendsto_intros) |
407 hence "(\<lambda>n. (x ^ n - 1) / (x - 1)) ----> 1 / (1 - x)" |
407 hence "(\<lambda>n. (x ^ n - 1) / (x - 1)) ----> 1 / (1 - x)" |
408 by (simp add: nonzero_minus_divide_right [OF neq_0] diff_divide_distrib) |
408 by (simp add: nonzero_minus_divide_right [OF neq_0] diff_divide_distrib) |
409 thus "(\<lambda>n. x ^ n) sums (1 / (1 - x))" |
409 thus "(\<lambda>n. x ^ n) sums (1 / (1 - x))" |
410 by (simp add: sums_def geometric_sum neq_1) |
410 by (simp add: sums_def geometric_sum neq_1) |
411 qed |
411 qed |
581 |
581 |
582 text{*Absolute convergence of series*} |
582 text{*Absolute convergence of series*} |
583 lemma summable_norm: |
583 lemma summable_norm: |
584 fixes f :: "nat \<Rightarrow> 'a::banach" |
584 fixes f :: "nat \<Rightarrow> 'a::banach" |
585 shows "summable (\<lambda>n. norm (f n)) \<Longrightarrow> norm (suminf f) \<le> (\<Sum>n. norm (f n))" |
585 shows "summable (\<lambda>n. norm (f n)) \<Longrightarrow> norm (suminf f) \<le> (\<Sum>n. norm (f n))" |
586 by (auto intro: LIMSEQ_le LIMSEQ_norm summable_norm_cancel |
586 by (auto intro: LIMSEQ_le tendsto_norm summable_norm_cancel |
587 summable_sumr_LIMSEQ_suminf norm_setsum) |
587 summable_sumr_LIMSEQ_suminf norm_setsum) |
588 |
588 |
589 lemma summable_rabs: |
589 lemma summable_rabs: |
590 fixes f :: "nat \<Rightarrow> real" |
590 fixes f :: "nat \<Rightarrow> real" |
591 shows "summable (\<lambda>n. \<bar>f n\<bar>) \<Longrightarrow> \<bar>suminf f\<bar> \<le> (\<Sum>n. \<bar>f n\<bar>)" |
591 shows "summable (\<lambda>n. \<bar>f n\<bar>) \<Longrightarrow> \<bar>suminf f\<bar> \<le> (\<Sum>n. \<bar>f n\<bar>)" |
690 unfolding real_norm_def |
690 unfolding real_norm_def |
691 by (simp only: abs_of_nonneg setsum_nonneg [rule_format]) |
691 by (simp only: abs_of_nonneg setsum_nonneg [rule_format]) |
692 |
692 |
693 have "(\<lambda>n. (\<Sum>k=0..<n. a k) * (\<Sum>k=0..<n. b k)) |
693 have "(\<lambda>n. (\<Sum>k=0..<n. a k) * (\<Sum>k=0..<n. b k)) |
694 ----> (\<Sum>k. a k) * (\<Sum>k. b k)" |
694 ----> (\<Sum>k. a k) * (\<Sum>k. b k)" |
695 by (intro LIMSEQ_mult summable_sumr_LIMSEQ_suminf |
695 by (intro tendsto_mult summable_sumr_LIMSEQ_suminf |
696 summable_norm_cancel [OF a] summable_norm_cancel [OF b]) |
696 summable_norm_cancel [OF a] summable_norm_cancel [OF b]) |
697 hence 1: "(\<lambda>n. setsum ?g (?S1 n)) ----> (\<Sum>k. a k) * (\<Sum>k. b k)" |
697 hence 1: "(\<lambda>n. setsum ?g (?S1 n)) ----> (\<Sum>k. a k) * (\<Sum>k. b k)" |
698 by (simp only: setsum_product setsum_Sigma [rule_format] |
698 by (simp only: setsum_product setsum_Sigma [rule_format] |
699 finite_atLeastLessThan) |
699 finite_atLeastLessThan) |
700 |
700 |
701 have "(\<lambda>n. (\<Sum>k=0..<n. norm (a k)) * (\<Sum>k=0..<n. norm (b k))) |
701 have "(\<lambda>n. (\<Sum>k=0..<n. norm (a k)) * (\<Sum>k=0..<n. norm (b k))) |
702 ----> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))" |
702 ----> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))" |
703 using a b by (intro LIMSEQ_mult summable_sumr_LIMSEQ_suminf) |
703 using a b by (intro tendsto_mult summable_sumr_LIMSEQ_suminf) |
704 hence "(\<lambda>n. setsum ?f (?S1 n)) ----> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))" |
704 hence "(\<lambda>n. setsum ?f (?S1 n)) ----> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))" |
705 by (simp only: setsum_product setsum_Sigma [rule_format] |
705 by (simp only: setsum_product setsum_Sigma [rule_format] |
706 finite_atLeastLessThan) |
706 finite_atLeastLessThan) |
707 hence "convergent (\<lambda>n. setsum ?f (?S1 n))" |
707 hence "convergent (\<lambda>n. setsum ?f (?S1 n))" |
708 by (rule convergentI) |
708 by (rule convergentI) |