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"