equal
deleted
inserted
replaced
26 (binder "\<Sum>" 10) |
26 (binder "\<Sum>" 10) |
27 where "suminf f = (THE s. f sums s)" |
27 where "suminf f = (THE s. f sums s)" |
28 |
28 |
29 text\<open>Variants of the definition\<close> |
29 text\<open>Variants of the definition\<close> |
30 lemma sums_def': "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i = 0..n. f i) \<longlonglongrightarrow> s" |
30 lemma sums_def': "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i = 0..n. f i) \<longlonglongrightarrow> s" |
31 apply (simp add: sums_def) |
31 unfolding sums_def |
32 apply (subst LIMSEQ_Suc_iff [symmetric]) |
32 apply (subst LIMSEQ_Suc_iff [symmetric]) |
33 apply (simp only: lessThan_Suc_atMost atLeast0AtMost) |
33 apply (simp only: lessThan_Suc_atMost atLeast0AtMost) |
34 done |
34 done |
35 |
35 |
36 lemma sums_def_le: "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i\<le>n. f i) \<longlonglongrightarrow> s" |
36 lemma sums_def_le: "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i\<le>n. f i) \<longlonglongrightarrow> s" |
79 lemma summable_zero[simp, intro]: "summable (\<lambda>n. 0)" |
79 lemma summable_zero[simp, intro]: "summable (\<lambda>n. 0)" |
80 by (rule sums_zero [THEN sums_summable]) |
80 by (rule sums_zero [THEN sums_summable]) |
81 |
81 |
82 lemma sums_group: "f sums s \<Longrightarrow> 0 < k \<Longrightarrow> (\<lambda>n. sum f {n * k ..< n * k + k}) sums s" |
82 lemma sums_group: "f sums s \<Longrightarrow> 0 < k \<Longrightarrow> (\<lambda>n. sum f {n * k ..< n * k + k}) sums s" |
83 apply (simp only: sums_def sum_nat_group tendsto_def eventually_sequentially) |
83 apply (simp only: sums_def sum_nat_group tendsto_def eventually_sequentially) |
84 apply safe |
84 apply (erule all_forward imp_forward exE| assumption)+ |
85 apply (erule_tac x=S in allE) |
85 apply (rule_tac x="N" in exI) |
86 apply safe |
86 by (metis le_square mult.commute mult.left_neutral mult_le_cancel2 mult_le_mono) |
87 apply (rule_tac x="N" in exI, safe) |
|
88 apply (drule_tac x="n*k" in spec) |
|
89 apply (erule mp) |
|
90 apply (erule order_trans) |
|
91 apply simp |
|
92 done |
|
93 |
87 |
94 lemma suminf_cong: "(\<And>n. f n = g n) \<Longrightarrow> suminf f = suminf g" |
88 lemma suminf_cong: "(\<And>n. f n = g n) \<Longrightarrow> suminf f = suminf g" |
95 by (rule arg_cong[of f g], rule ext) simp |
89 by (rule arg_cong[of f g], rule ext) simp |
96 |
90 |
97 lemma summable_cong: |
91 lemma summable_cong: |
452 |
446 |
453 lemma summable_LIMSEQ_zero: "summable f \<Longrightarrow> f \<longlonglongrightarrow> 0" |
447 lemma summable_LIMSEQ_zero: "summable f \<Longrightarrow> f \<longlonglongrightarrow> 0" |
454 apply (drule summable_iff_convergent [THEN iffD1]) |
448 apply (drule summable_iff_convergent [THEN iffD1]) |
455 apply (drule convergent_Cauchy) |
449 apply (drule convergent_Cauchy) |
456 apply (simp only: Cauchy_iff LIMSEQ_iff) |
450 apply (simp only: Cauchy_iff LIMSEQ_iff) |
457 apply safe |
451 by (metis add.commute add_diff_cancel_right' diff_zero le_SucI sum_lessThan_Suc) |
458 apply (drule_tac x="r" in spec) |
|
459 apply safe |
|
460 apply (rule_tac x="M" in exI) |
|
461 apply safe |
|
462 apply (drule_tac x="Suc n" in spec) |
|
463 apply simp |
|
464 apply (drule_tac x="n" in spec) |
|
465 apply simp |
|
466 done |
|
467 |
452 |
468 lemma summable_imp_convergent: "summable f \<Longrightarrow> convergent f" |
453 lemma summable_imp_convergent: "summable f \<Longrightarrow> convergent f" |
469 by (force dest!: summable_LIMSEQ_zero simp: convergent_def) |
454 by (force dest!: summable_LIMSEQ_zero simp: convergent_def) |
470 |
455 |
471 lemma summable_imp_Bseq: "summable f \<Longrightarrow> Bseq f" |
456 lemma summable_imp_Bseq: "summable f \<Longrightarrow> Bseq f" |
723 begin |
708 begin |
724 |
709 |
725 text \<open>Absolute convergence imples normal convergence.\<close> |
710 text \<open>Absolute convergence imples normal convergence.\<close> |
726 |
711 |
727 lemma summable_norm_cancel: "summable (\<lambda>n. norm (f n)) \<Longrightarrow> summable f" |
712 lemma summable_norm_cancel: "summable (\<lambda>n. norm (f n)) \<Longrightarrow> summable f" |
728 apply (simp only: summable_Cauchy) |
713 unfolding summable_Cauchy |
729 apply safe |
714 apply (erule all_forward imp_forward ex_forward | assumption)+ |
730 apply (drule_tac x="e" in spec) |
715 apply (fastforce simp add: order_le_less_trans [OF norm_sum] order_le_less_trans [OF abs_ge_self]) |
731 apply safe |
|
732 apply (rule_tac x="N" in exI) |
|
733 apply safe |
|
734 apply (drule_tac x="m" in spec) |
|
735 apply safe |
|
736 apply (rule order_le_less_trans [OF norm_sum]) |
|
737 apply (rule order_le_less_trans [OF abs_ge_self]) |
|
738 apply simp |
|
739 done |
716 done |
740 |
717 |
741 lemma summable_norm: "summable (\<lambda>n. norm (f n)) \<Longrightarrow> norm (suminf f) \<le> (\<Sum>n. norm (f n))" |
718 lemma summable_norm: "summable (\<lambda>n. norm (f n)) \<Longrightarrow> norm (suminf f) \<le> (\<Sum>n. norm (f n))" |
742 by (auto intro: LIMSEQ_le tendsto_norm summable_norm_cancel summable_LIMSEQ norm_sum) |
719 by (auto intro: LIMSEQ_le tendsto_norm summable_norm_cancel summable_LIMSEQ norm_sum) |
743 |
720 |
832 and r0: "r < r0" |
809 and r0: "r < r0" |
833 and M: "\<And>n. norm (a n) * r0^n \<le> M" |
810 and M: "\<And>n. norm (a n) * r0^n \<le> M" |
834 shows "summable (\<lambda>n. norm (a n) * r^n)" |
811 shows "summable (\<lambda>n. norm (a n) * r^n)" |
835 proof (rule summable_comparison_test') |
812 proof (rule summable_comparison_test') |
836 show "summable (\<lambda>n. M * (r / r0) ^ n)" |
813 show "summable (\<lambda>n. M * (r / r0) ^ n)" |
837 using assms |
814 using assms by (auto simp add: summable_mult summable_geometric) |
838 by (auto simp add: summable_mult summable_geometric) |
|
839 show "norm (norm (a n) * r ^ n) \<le> M * (r / r0) ^ n" for n |
815 show "norm (norm (a n) * r ^ n) \<le> M * (r / r0) ^ n" for n |
840 using r r0 M [of n] |
816 using r r0 M [of n] dual_order.order_iff_strict |
841 apply (auto simp add: abs_mult field_simps) |
817 by (fastforce simp add: abs_mult field_simps) |
842 apply (cases "r = 0") |
|
843 apply simp |
|
844 apply (cases n) |
|
845 apply auto |
|
846 done |
|
847 qed |
818 qed |
848 |
819 |
849 |
820 |
850 text \<open>Summability of geometric series for real algebras.\<close> |
821 text \<open>Summability of geometric series for real algebras.\<close> |
851 |
822 |