generalize some lemmas
authorhuffman
Mon Sep 05 16:07:40 2011 -0700 (2011-09-05)
changeset 447268478eab380e9
parent 44725 d3bf0e33c98a
child 44727 d45acd50a894
generalize some lemmas
src/HOL/Series.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Series.thy	Mon Sep 05 12:19:04 2011 -0700
     1.2 +++ b/src/HOL/Series.thy	Mon Sep 05 16:07:40 2011 -0700
     1.3 @@ -435,7 +435,7 @@
     1.4  by (simp add: summable_def sums_def convergent_def)
     1.5  
     1.6  lemma summable_LIMSEQ_zero:
     1.7 -  fixes f :: "nat \<Rightarrow> 'a::real_normed_field"
     1.8 +  fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
     1.9    shows "summable f \<Longrightarrow> f ----> 0"
    1.10  apply (drule summable_convergent_sumr_iff [THEN iffD1])
    1.11  apply (drule convergent_Cauchy)
     2.1 --- a/src/HOL/Transcendental.thy	Mon Sep 05 12:19:04 2011 -0700
     2.2 +++ b/src/HOL/Transcendental.thy	Mon Sep 05 16:07:40 2011 -0700
     2.3 @@ -54,7 +54,7 @@
     2.4  x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}
     2.5  
     2.6  lemma powser_insidea:
     2.7 -  fixes x z :: "'a::{real_normed_field,banach}"
     2.8 +  fixes x z :: "'a::real_normed_field"
     2.9    assumes 1: "summable (\<lambda>n. f n * x ^ n)"
    2.10    assumes 2: "norm z < norm x"
    2.11    shows "summable (\<lambda>n. norm (f n * z ^ n))"
    2.12 @@ -65,7 +65,7 @@
    2.13    hence "convergent (\<lambda>n. f n * x ^ n)"
    2.14      by (rule convergentI)
    2.15    hence "Cauchy (\<lambda>n. f n * x ^ n)"
    2.16 -    by (simp add: Cauchy_convergent_iff)
    2.17 +    by (rule convergent_Cauchy)
    2.18    hence "Bseq (\<lambda>n. f n * x ^ n)"
    2.19      by (rule Cauchy_Bseq)
    2.20    then obtain K where 3: "0 < K" and 4: "\<forall>n. norm (f n * x ^ n) \<le> K"