src/HOL/Series.thy
changeset 59000 6eb0725503fc
parent 58889 5b7a9633cfa8
child 59025 d885cff91200
--- a/src/HOL/Series.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Series.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -666,4 +666,14 @@
 lemma summable_rabs: "summable (\<lambda>n. \<bar>f n :: real\<bar>) \<Longrightarrow> \<bar>suminf f\<bar> \<le> (\<Sum>n. \<bar>f n\<bar>)"
   by (fold real_norm_def) (rule summable_norm)
 
+lemma summable_power_series:
+  fixes z :: real
+  assumes le_1: "\<And>i. f i \<le> 1" and nonneg: "\<And>i. 0 \<le> f i" and z: "0 \<le> z" "z < 1"
+  shows "summable (\<lambda>i. f i * z^i)"
+proof (rule summable_comparison_test[OF _ summable_geometric])
+  show "norm z < 1" using z by (auto simp: less_imp_le)
+  show "\<And>n. \<exists>N. \<forall>na\<ge>N. norm (f na * z ^ na) \<le> z ^ na"
+    using z by (auto intro!: exI[of _ 0] mult_left_le_one_le simp: abs_mult nonneg power_abs less_imp_le le_1)
+qed
+
 end