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)"
```