src/HOL/Series.thy
changeset 32707 836ec9d0a0c8
parent 31336 e17f13cd1280
child 32877 6f09346c7c08
     1.1 --- a/src/HOL/Series.thy	Wed Sep 23 11:06:32 2009 +0100
     1.2 +++ b/src/HOL/Series.thy	Fri Sep 25 13:47:28 2009 +0100
     1.3 @@ -104,6 +104,9 @@
     1.4       "summable f ==> (%n. setsum f {0..<n}) ----> (suminf f)"
     1.5  by (rule summable_sums [unfolded sums_def])
     1.6  
     1.7 +lemma suminf_eq_lim: "suminf f = lim (%n. setsum f {0..<n})"
     1.8 +  by (simp add: suminf_def sums_def lim_def) 
     1.9 +
    1.10  (*-------------------
    1.11      sum is unique                    
    1.12   ------------------*)
    1.13 @@ -112,6 +115,9 @@
    1.14  apply (auto intro!: LIMSEQ_unique simp add: sums_def)
    1.15  done
    1.16  
    1.17 +lemma sums_iff: "f sums x \<longleftrightarrow> summable f \<and> (suminf f = x)"
    1.18 +  by (metis summable_sums sums_summable sums_unique)
    1.19 +
    1.20  lemma sums_split_initial_segment: "f sums s ==> 
    1.21    (%n. f(n + k)) sums (s - (SUM i = 0..< k. f i))"
    1.22    apply (unfold sums_def);
    1.23 @@ -368,6 +374,11 @@
    1.24  apply (drule_tac x="n" in spec, simp)
    1.25  done
    1.26  
    1.27 +lemma suminf_le:
    1.28 +  fixes x :: real
    1.29 +  shows "summable f \<Longrightarrow> (!!n. setsum f {0..<n} \<le> x) \<Longrightarrow> suminf f \<le> x"
    1.30 +  by (simp add: summable_convergent_sumr_iff suminf_eq_lim lim_le) 
    1.31 +
    1.32  lemma summable_Cauchy:
    1.33       "summable (f::nat \<Rightarrow> 'a::banach) =  
    1.34        (\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. norm (setsum f {m..<n}) < e)"