# HG changeset patch
# User huffman
# Date 1179941002 -7200
# Node ID bc000fc64fcec2084ffbf0b801523f20d36ff80a
# Parent  e692e0a38bad68dd2b25652cd8b89b160fbe5d3b
add lemma complete_algebra_summable_geometric

diff -r e692e0a38bad -r bc000fc64fce src/HOL/Hyperreal/Series.thy
--- 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: