src/HOL/Series.thy
changeset 50999 3de230ed0547
parent 50331 4b6dc5077e98
child 51477 2990382dc066
     1.1 --- a/src/HOL/Series.thy	Thu Jan 31 11:31:22 2013 +0100
     1.2 +++ b/src/HOL/Series.thy	Thu Jan 31 11:31:27 2013 +0100
     1.3 @@ -367,7 +367,7 @@
     1.4  
     1.5  lemma pos_summable:
     1.6    fixes f:: "nat \<Rightarrow> real"
     1.7 -  assumes pos: "!!n. 0 \<le> f n" and le: "!!n. setsum f {0..<n} \<le> x"
     1.8 +  assumes pos: "\<And>n. 0 \<le> f n" and le: "\<And>n. setsum f {0..<n} \<le> x"
     1.9    shows "summable f"
    1.10  proof -
    1.11    have "convergent (\<lambda>n. setsum f {0..<n})"
    1.12 @@ -386,35 +386,65 @@
    1.13  qed
    1.14  
    1.15  lemma series_pos_le:
    1.16 -  fixes f :: "nat \<Rightarrow> real"
    1.17 +  fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
    1.18    shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 \<le> f m\<rbrakk> \<Longrightarrow> setsum f {0..<n} \<le> suminf f"
    1.19 -apply (drule summable_sums)
    1.20 -apply (simp add: sums_def)
    1.21 -apply (cut_tac k = "setsum f {0..<n}" in tendsto_const)
    1.22 -apply (erule LIMSEQ_le, blast)
    1.23 -apply (rule_tac x="n" in exI, clarify)
    1.24 -apply (rule setsum_mono2)
    1.25 -apply auto
    1.26 -done
    1.27 +  apply (drule summable_sums)
    1.28 +  apply (simp add: sums_def)
    1.29 +  apply (rule LIMSEQ_le_const)
    1.30 +  apply assumption
    1.31 +  apply (intro exI[of _ n])
    1.32 +  apply (auto intro!: setsum_mono2)
    1.33 +  done
    1.34  
    1.35  lemma series_pos_less:
    1.36 -  fixes f :: "nat \<Rightarrow> real"
    1.37 +  fixes f :: "nat \<Rightarrow> 'a::{ordered_ab_semigroup_add_imp_le, ordered_comm_monoid_add, linorder_topology}"
    1.38    shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 < f m\<rbrakk> \<Longrightarrow> setsum f {0..<n} < suminf f"
    1.39 -apply (rule_tac y="setsum f {0..<Suc n}" in order_less_le_trans)
    1.40 -apply simp
    1.41 -apply (erule series_pos_le)
    1.42 -apply (simp add: order_less_imp_le)
    1.43 -done
    1.44 +  apply (rule_tac y="setsum f {0..<Suc n}" in order_less_le_trans)
    1.45 +  using add_less_cancel_left [of "setsum f {0..<n}" 0 "f n"]
    1.46 +  apply simp
    1.47 +  apply (erule series_pos_le)
    1.48 +  apply (simp add: order_less_imp_le)
    1.49 +  done
    1.50 +
    1.51 +lemma suminf_eq_zero_iff:
    1.52 +  fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
    1.53 +  shows "\<lbrakk>summable f; \<forall>n. 0 \<le> f n\<rbrakk> \<Longrightarrow> suminf f = 0 \<longleftrightarrow> (\<forall>n. f n = 0)"
    1.54 +proof
    1.55 +  assume "summable f" "suminf f = 0" and pos: "\<forall>n. 0 \<le> f n"
    1.56 +  then have "f sums 0"
    1.57 +    by (simp add: sums_iff)
    1.58 +  then have f: "(\<lambda>n. \<Sum>i<n. f i) ----> 0"
    1.59 +    by (simp add: sums_def atLeast0LessThan)
    1.60 +  have "\<And>i. (\<Sum>n\<in>{i}. f n) \<le> 0"
    1.61 +  proof (rule LIMSEQ_le_const[OF f])
    1.62 +    fix i show "\<exists>N. \<forall>n\<ge>N. (\<Sum>n\<in>{i}. f n) \<le> setsum f {..<n}"
    1.63 +      using pos by (intro exI[of _ "Suc i"] allI impI setsum_mono2) auto
    1.64 +  qed
    1.65 +  with pos show "\<forall>n. f n = 0"
    1.66 +    by (auto intro!: antisym)
    1.67 +next
    1.68 +  assume "\<forall>n. f n = 0"
    1.69 +  then have "f = (\<lambda>n. 0)"
    1.70 +    by auto
    1.71 +  then show "suminf f = 0"
    1.72 +    by simp
    1.73 +qed
    1.74 +
    1.75 +lemma suminf_gt_zero_iff:
    1.76 +  fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
    1.77 +  shows "\<lbrakk>summable f; \<forall>n. 0 \<le> f n\<rbrakk> \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
    1.78 +  using series_pos_le[of f 0] suminf_eq_zero_iff[of f]
    1.79 +  by (simp add: less_le)
    1.80  
    1.81  lemma suminf_gt_zero:
    1.82 -  fixes f :: "nat \<Rightarrow> real"
    1.83 +  fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
    1.84    shows "\<lbrakk>summable f; \<forall>n. 0 < f n\<rbrakk> \<Longrightarrow> 0 < suminf f"
    1.85 -by (drule_tac n="0" in series_pos_less, simp_all)
    1.86 +  using suminf_gt_zero_iff[of f] by (simp add: less_imp_le)
    1.87  
    1.88  lemma suminf_ge_zero:
    1.89 -  fixes f :: "nat \<Rightarrow> real"
    1.90 +  fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
    1.91    shows "\<lbrakk>summable f; \<forall>n. 0 \<le> f n\<rbrakk> \<Longrightarrow> 0 \<le> suminf f"
    1.92 -by (drule_tac n="0" in series_pos_le, simp_all)
    1.93 +  by (drule_tac n="0" in series_pos_le, simp_all)
    1.94  
    1.95  lemma sumr_pos_lt_pair:
    1.96    fixes f :: "nat \<Rightarrow> real"
    1.97 @@ -493,9 +523,14 @@
    1.98  done
    1.99  
   1.100  lemma suminf_le:
   1.101 -  fixes x :: real
   1.102 +  fixes x :: "'a :: {ordered_comm_monoid_add, linorder_topology}"
   1.103    shows "summable f \<Longrightarrow> (!!n. setsum f {0..<n} \<le> x) \<Longrightarrow> suminf f \<le> x"
   1.104 -  by (simp add: summable_convergent_sumr_iff suminf_eq_lim lim_le)
   1.105 +  apply (drule summable_sums)
   1.106 +  apply (simp add: sums_def)
   1.107 +  apply (rule LIMSEQ_le_const2)
   1.108 +  apply assumption
   1.109 +  apply auto
   1.110 +  done
   1.111  
   1.112  lemma summable_Cauchy:
   1.113       "summable (f::nat \<Rightarrow> 'a::banach) =
   1.114 @@ -575,7 +610,7 @@
   1.115  text{*Limit comparison property for series (c.f. jrh)*}
   1.116  
   1.117  lemma summable_le:
   1.118 -  fixes f g :: "nat \<Rightarrow> real"
   1.119 +  fixes f g :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
   1.120    shows "\<lbrakk>\<forall>n. f n \<le> g n; summable f; summable g\<rbrakk> \<Longrightarrow> suminf f \<le> suminf g"
   1.121  apply (drule summable_sums)+
   1.122  apply (simp only: sums_def, erule (1) LIMSEQ_le)
   1.123 @@ -597,15 +632,7 @@
   1.124    fixes f::"nat\<Rightarrow>real"
   1.125    assumes gt0: "\<forall>n. 0 \<le> f n" and sm: "summable f"
   1.126    shows "0 \<le> suminf f"
   1.127 -proof -
   1.128 -  let ?g = "(\<lambda>n. (0::real))"
   1.129 -  from gt0 have "\<forall>n. ?g n \<le> f n" by simp
   1.130 -  moreover have "summable ?g" by (rule summable_zero)
   1.131 -  moreover from sm have "summable f" .
   1.132 -  ultimately have "suminf ?g \<le> suminf f" by (rule summable_le)
   1.133 -  then show "0 \<le> suminf f" by simp
   1.134 -qed
   1.135 -
   1.136 +  using suminf_ge_zero[OF sm gt0] by simp
   1.137  
   1.138  text{*Absolute convergence imples normal convergence*}
   1.139  lemma summable_norm_cancel: