src/HOL/Transcendental.thy
 changeset 57025 e7fd64f82876 parent 56952 efa2a83d548b child 57129 7edb7550663e
```     1.1 --- a/src/HOL/Transcendental.thy	Tue May 20 16:52:59 2014 +0200
1.2 +++ b/src/HOL/Transcendental.thy	Tue May 20 19:24:39 2014 +0200
1.3 @@ -10,6 +10,32 @@
1.4  imports Fact Series Deriv NthRoot
1.5  begin
1.6
1.7 +lemma root_test_convergence:
1.8 +  fixes f :: "nat \<Rightarrow> 'a::banach"
1.9 +  assumes f: "(\<lambda>n. root n (norm (f n))) ----> x" -- "could be weakened to lim sup"
1.10 +  assumes "x < 1"
1.11 +  shows "summable f"
1.12 +proof -
1.13 +  have "0 \<le> x"
1.14 +    by (rule LIMSEQ_le[OF tendsto_const f]) (auto intro!: exI[of _ 1])
1.15 +  from `x < 1` obtain z where z: "x < z" "z < 1"
1.16 +    by (metis dense)
1.17 +  from f `x < z`
1.18 +  have "eventually (\<lambda>n. root n (norm (f n)) < z) sequentially"
1.19 +    by (rule order_tendstoD)
1.20 +  then have "eventually (\<lambda>n. norm (f n) \<le> z^n) sequentially"
1.21 +    using eventually_ge_at_top
1.22 +  proof eventually_elim
1.23 +    fix n assume less: "root n (norm (f n)) < z" and n: "1 \<le> n"
1.24 +    from power_strict_mono[OF less, of n] n
1.25 +    show "norm (f n) \<le> z ^ n"
1.26 +      by simp
1.27 +  qed
1.28 +  then show "summable f"
1.29 +    unfolding eventually_sequentially
1.30 +    using z `0 \<le> x` by (auto intro!: summable_comparison_test[OF _  summable_geometric])
1.31 +qed
1.32 +
1.33  subsection {* Properties of Power Series *}
1.34
1.35  lemma lemma_realpow_diff:
```