1.1 --- a/src/HOL/Series.thy	Thu Nov 13 14:40:06 2014 +0100
     1.2 +++ b/src/HOL/Series.thy	Thu Nov 13 17:19:52 2014 +0100
     1.3 @@ -666,4 +666,14 @@
     1.4  lemma summable_rabs: "summable (\<lambda>n. \<bar>f n :: real\<bar>) \<Longrightarrow> \<bar>suminf f\<bar> \<le> (\<Sum>n. \<bar>f n\<bar>)"
     1.5    by (fold real_norm_def) (rule summable_norm)
     1.6  
     1.7 +lemma summable_power_series:
     1.8 +  fixes z :: real
     1.9 +  assumes le_1: "\<And>i. f i \<le> 1" and nonneg: "\<And>i. 0 \<le> f i" and z: "0 \<le> z" "z < 1"
    1.10 +  shows "summable (\<lambda>i. f i * z^i)"
    1.11 +proof (rule summable_comparison_test[OF _ summable_geometric])
    1.12 +  show "norm z < 1" using z by (auto simp: less_imp_le)
    1.13 +  show "\<And>n. \<exists>N. \<forall>na\<ge>N. norm (f na * z ^ na) \<le> z ^ na"
    1.14 +    using z by (auto intro!: exI[of _ 0] mult_left_le_one_le simp: abs_mult nonneg power_abs less_imp_le le_1)
    1.15 +qed
    1.16 +
    1.17  end