src/HOL/Series.thy
changeset 56369 2704ca85be98
parent 56217 dc429a5b13c4
child 56536 aefb4a8da31f
     1.1 --- a/src/HOL/Series.thy	Wed Apr 02 17:47:56 2014 +0200
     1.2 +++ b/src/HOL/Series.thy	Wed Apr 02 18:35:01 2014 +0200
     1.3 @@ -463,7 +463,7 @@
     1.4  
     1.5  (*A better argument order*)
     1.6  lemma summable_comparison_test': "summable g \<Longrightarrow> (\<And>n. n \<ge> N \<Longrightarrow> norm(f n) \<le> g n) \<Longrightarrow> summable f"
     1.7 -by (rule summable_comparison_test) auto
     1.8 +  by (rule summable_comparison_test) auto
     1.9  
    1.10  subsection {* The Ratio Test*}
    1.11  
    1.12 @@ -502,6 +502,27 @@
    1.13  
    1.14  end
    1.15  
    1.16 +text{*Relations among convergence and absolute convergence for power series.*}
    1.17 +
    1.18 +lemma abel_lemma:
    1.19 +  fixes a :: "nat \<Rightarrow> 'a::real_normed_vector"
    1.20 +  assumes r: "0 \<le> r" and r0: "r < r0" and M: "\<And>n. norm (a n) * r0^n \<le> M"
    1.21 +    shows "summable (\<lambda>n. norm (a n) * r^n)"
    1.22 +proof (rule summable_comparison_test')
    1.23 +  show "summable (\<lambda>n. M * (r / r0) ^ n)"
    1.24 +    using assms 
    1.25 +    by (auto simp add: summable_mult summable_geometric)
    1.26 +next
    1.27 +  fix n
    1.28 +  show "norm (norm (a n) * r ^ n) \<le> M * (r / r0) ^ n"
    1.29 +    using r r0 M [of n]
    1.30 +    apply (auto simp add: abs_mult field_simps power_divide)
    1.31 +    apply (cases "r=0", simp)
    1.32 +    apply (cases n, auto)
    1.33 +    done
    1.34 +qed
    1.35 +
    1.36 +
    1.37  text{*Summability of geometric series for real algebras*}
    1.38  
    1.39  lemma complete_algebra_summable_geometric: