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:
```