--- a/src/HOL/Series.thy Wed Sep 23 11:06:32 2009 +0100
+++ b/src/HOL/Series.thy Fri Sep 25 13:47:28 2009 +0100
@@ -104,6 +104,9 @@
"summable f ==> (%n. setsum f {0..<n}) ----> (suminf f)"
by (rule summable_sums [unfolded sums_def])
+lemma suminf_eq_lim: "suminf f = lim (%n. setsum f {0..<n})"
+ by (simp add: suminf_def sums_def lim_def)
+
(*-------------------
sum is unique
------------------*)
@@ -112,6 +115,9 @@
apply (auto intro!: LIMSEQ_unique simp add: sums_def)
done
+lemma sums_iff: "f sums x \<longleftrightarrow> summable f \<and> (suminf f = x)"
+ by (metis summable_sums sums_summable sums_unique)
+
lemma sums_split_initial_segment: "f sums s ==>
(%n. f(n + k)) sums (s - (SUM i = 0..< k. f i))"
apply (unfold sums_def);
@@ -368,6 +374,11 @@
apply (drule_tac x="n" in spec, simp)
done
+lemma suminf_le:
+ fixes x :: real
+ shows "summable f \<Longrightarrow> (!!n. setsum f {0..<n} \<le> x) \<Longrightarrow> suminf f \<le> x"
+ by (simp add: summable_convergent_sumr_iff suminf_eq_lim lim_le)
+
lemma summable_Cauchy:
"summable (f::nat \<Rightarrow> 'a::banach) =
(\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. norm (setsum f {m..<n}) < e)"