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: