src/HOL/Series.thy
 changeset 31017 2c227493ea56 parent 30649 57753e0ec1d4 child 31336 e17f13cd1280
```     1.1 --- a/src/HOL/Series.thy	Tue Apr 28 15:50:30 2009 +0200
1.2 +++ b/src/HOL/Series.thy	Tue Apr 28 15:50:30 2009 +0200
1.3 @@ -331,7 +331,7 @@
1.4  lemmas sumr_geometric = geometric_sum [where 'a = real]
1.5
1.6  lemma geometric_sums:
1.7 -  fixes x :: "'a::{real_normed_field,recpower}"
1.8 +  fixes x :: "'a::{real_normed_field}"
1.9    shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) sums (1 / (1 - x))"
1.10  proof -
1.11    assume less_1: "norm x < 1"
1.12 @@ -348,7 +348,7 @@
1.13  qed
1.14
1.15  lemma summable_geometric:
1.16 -  fixes x :: "'a::{real_normed_field,recpower}"
1.17 +  fixes x :: "'a::{real_normed_field}"
1.18    shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)"
1.19  by (rule geometric_sums [THEN sums_summable])
1.20
1.21 @@ -434,7 +434,7 @@
1.22  text{*Summability of geometric series for real algebras*}
1.23
1.24  lemma complete_algebra_summable_geometric:
1.25 -  fixes x :: "'a::{real_normed_algebra_1,banach,recpower}"
1.26 +  fixes x :: "'a::{real_normed_algebra_1,banach}"
1.27    shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)"
1.28  proof (rule summable_comparison_test)
1.29    show "\<exists>N. \<forall>n\<ge>N. norm (x ^ n) \<le> norm x ^ n"
```