--- a/src/HOL/Hyperreal/Series.thy Wed May 23 14:52:12 2007 +0200
+++ b/src/HOL/Hyperreal/Series.thy Wed May 23 19:23:22 2007 +0200
@@ -440,6 +440,18 @@
apply (auto)
done
+text{*Summability of geometric series for real algebras*}
+
+lemma complete_algebra_summable_geometric:
+ fixes x :: "'a::{real_normed_algebra_1,banach,recpower}"
+ shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)"
+proof (rule summable_comparison_test)
+ show "\<exists>N. \<forall>n\<ge>N. norm (x ^ n) \<le> norm x ^ n"
+ by (simp add: norm_power_ineq)
+ show "norm x < 1 \<Longrightarrow> summable (\<lambda>n. norm x ^ n)"
+ by (simp add: summable_geometric)
+qed
+
text{*Limit comparison property for series (c.f. jrh)*}
lemma summable_le: