src/HOL/Series.thy
 changeset 33271 7be66dee1a5a parent 32877 6f09346c7c08 child 33536 fd28b7399f2b
```     1.1 --- a/src/HOL/Series.thy	Tue Oct 27 14:46:03 2009 +0000
1.2 +++ b/src/HOL/Series.thy	Wed Oct 28 11:42:31 2009 +0000
1.3 @@ -10,7 +10,7 @@
1.4  header{*Finite Summation and Infinite Series*}
1.5
1.6  theory Series
1.7 -imports SEQ
1.8 +imports SEQ Deriv
1.9  begin
1.10
1.11  definition
1.12 @@ -285,6 +285,26 @@
1.13  text{*A summable series of positive terms has limit that is at least as
1.14  great as any partial sum.*}
1.15
1.16 +lemma pos_summable:
1.17 +  fixes f:: "nat \<Rightarrow> real"
1.18 +  assumes pos: "!!n. 0 \<le> f n" and le: "!!n. setsum f {0..<n} \<le> x"
1.19 +  shows "summable f"
1.20 +proof -
1.21 +  have "convergent (\<lambda>n. setsum f {0..<n})"
1.22 +    proof (rule Bseq_mono_convergent)
1.23 +      show "Bseq (\<lambda>n. setsum f {0..<n})"
1.24 +	by (rule f_inc_g_dec_Beq_f [of "(\<lambda>n. setsum f {0..<n})" "\<lambda>n. x"])
1.25 +           (auto simp add: le pos)
1.26 +    next
1.27 +      show "\<forall>m n. m \<le> n \<longrightarrow> setsum f {0..<m} \<le> setsum f {0..<n}"
1.28 +	by (auto intro: setsum_mono2 pos)
1.29 +    qed
1.30 +  then obtain L where "(%n. setsum f {0..<n}) ----> L"
1.31 +    by (blast dest: convergentD)
1.32 +  thus ?thesis
1.33 +    by (force simp add: summable_def sums_def)
1.34 +qed
1.35 +
1.36  lemma series_pos_le:
1.37    fixes f :: "nat \<Rightarrow> real"
1.38    shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 \<le> f m\<rbrakk> \<Longrightarrow> setsum f {0..<n} \<le> suminf f"
1.39 @@ -361,6 +381,19 @@
1.40    shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)"
1.41  by (rule geometric_sums [THEN sums_summable])
1.42
1.43 +lemma half: "0 < 1 / (2::'a::{number_ring,division_by_zero,ordered_field})"
1.44 +  by arith
1.45 +
1.46 +lemma power_half_series: "(\<lambda>n. (1/2::real)^Suc n) sums 1"
1.47 +proof -
1.48 +  have 2: "(\<lambda>n. (1/2::real)^n) sums 2" using geometric_sums [of "1/2::real"]
1.49 +    by auto
1.50 +  have "(\<lambda>n. (1/2::real)^Suc n) = (\<lambda>n. (1 / 2) ^ n / 2)"
1.51 +    by simp
1.52 +  thus ?thesis using divide.sums [OF 2, of 2]
1.53 +    by simp
1.54 +qed
1.55 +
1.56  text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
1.57
1.58  lemma summable_convergent_sumr_iff:
```