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: