New lemmas involving the real numbers, especially limits and series
authorpaulson
Fri Sep 25 13:47:28 2009 +0100 (2009-09-25)
changeset 32707836ec9d0a0c8
parent 32649 442e03154ee6
child 32708 224ceb576bc3
New lemmas involving the real numbers, especially limits and series
src/HOL/RComplete.thy
src/HOL/SEQ.thy
src/HOL/Series.thy
     1.1 --- a/src/HOL/RComplete.thy	Wed Sep 23 11:06:32 2009 +0100
     1.2 +++ b/src/HOL/RComplete.thy	Fri Sep 25 13:47:28 2009 +0100
     1.3 @@ -14,6 +14,9 @@
     1.4  lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
     1.5    by simp
     1.6  
     1.7 +lemma abs_diff_less_iff:
     1.8 +  "(\<bar>x - a\<bar> < (r::'a::ordered_idom)) = (a - r < x \<and> x < a + r)"
     1.9 +  by auto
    1.10  
    1.11  subsection {* Completeness of Positive Reals *}
    1.12  
    1.13 @@ -301,6 +304,20 @@
    1.14    qed
    1.15  qed
    1.16  
    1.17 +text{*A version of the same theorem without all those predicates!*}
    1.18 +lemma reals_complete2:
    1.19 +  fixes S :: "(real set)"
    1.20 +  assumes "\<exists>y. y\<in>S" and "\<exists>(x::real). \<forall>y\<in>S. y \<le> x"
    1.21 +  shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) & 
    1.22 +               (\<forall>z. ((\<forall>y\<in>S. y \<le> z) --> x \<le> z))"
    1.23 +proof -
    1.24 +  have "\<exists>x. isLub UNIV S x" 
    1.25 +    by (rule reals_complete)
    1.26 +       (auto simp add: isLub_def isUb_def leastP_def setle_def setge_def prems)
    1.27 +  thus ?thesis
    1.28 +    by (metis UNIV_I isLub_isUb isLub_le_isUb isUbD isUb_def setleI)
    1.29 +qed
    1.30 +
    1.31  
    1.32  subsection {* The Archimedean Property of the Reals *}
    1.33  
     2.1 --- a/src/HOL/SEQ.thy	Wed Sep 23 11:06:32 2009 +0100
     2.2 +++ b/src/HOL/SEQ.thy	Fri Sep 25 13:47:28 2009 +0100
     2.3 @@ -500,6 +500,28 @@
     2.4  apply (drule LIMSEQ_minus, auto)
     2.5  done
     2.6  
     2.7 +lemma lim_le:
     2.8 +  fixes x :: real
     2.9 +  assumes f: "convergent f" and fn_le: "!!n. f n \<le> x"
    2.10 +  shows "lim f \<le> x"
    2.11 +proof (rule classical)
    2.12 +  assume "\<not> lim f \<le> x"
    2.13 +  hence 0: "0 < lim f - x" by arith
    2.14 +  have 1: "f----> lim f"
    2.15 +    by (metis convergent_LIMSEQ_iff f) 
    2.16 +  thus ?thesis
    2.17 +    proof (simp add: LIMSEQ_iff)
    2.18 +      assume "\<forall>r>0. \<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < r"
    2.19 +      hence "\<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x"
    2.20 +	by (metis 0)
    2.21 +      from this obtain no where "\<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x"
    2.22 +	by blast
    2.23 +      thus "lim f \<le> x"
    2.24 +	by (metis add_cancel_end add_minus_cancel diff_def linorder_linear 
    2.25 +                  linorder_not_le minus_diff_eq abs_diff_less_iff fn_le) 
    2.26 +    qed
    2.27 +qed
    2.28 +
    2.29  text{* Given a binary function @{text "f:: nat \<Rightarrow> 'a \<Rightarrow> 'a"}, its values are uniquely determined by a function g *}
    2.30  
    2.31  lemma nat_function_unique: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
    2.32 @@ -1082,10 +1104,6 @@
    2.33  lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u"
    2.34  by (simp add: isUbI setleI)
    2.35  
    2.36 -lemma real_abs_diff_less_iff:
    2.37 -  "(\<bar>x - a\<bar> < (r::real)) = (a - r < x \<and> x < a + r)"
    2.38 -by auto
    2.39 -
    2.40  locale real_Cauchy =
    2.41    fixes X :: "nat \<Rightarrow> real"
    2.42    assumes X: "Cauchy X"
    2.43 @@ -1122,13 +1140,13 @@
    2.44    show "\<exists>x. x \<in> S"
    2.45    proof
    2.46      from N have "\<forall>n\<ge>N. X N - 1 < X n"
    2.47 -      by (simp add: real_abs_diff_less_iff)
    2.48 +      by (simp add: abs_diff_less_iff)
    2.49      thus "X N - 1 \<in> S" by (rule mem_S)
    2.50    qed
    2.51    show "\<exists>u. isUb UNIV S u"
    2.52    proof
    2.53      from N have "\<forall>n\<ge>N. X n < X N + 1"
    2.54 -      by (simp add: real_abs_diff_less_iff)
    2.55 +      by (simp add: abs_diff_less_iff)
    2.56      thus "isUb UNIV S (X N + 1)"
    2.57        by (rule bound_isUb)
    2.58    qed
    2.59 @@ -1144,7 +1162,7 @@
    2.60      using CauchyD [OF X r] by auto
    2.61    hence "\<forall>n\<ge>N. norm (X n - X N) < r/2" by simp
    2.62    hence N: "\<forall>n\<ge>N. X N - r/2 < X n \<and> X n < X N + r/2"
    2.63 -    by (simp only: real_norm_def real_abs_diff_less_iff)
    2.64 +    by (simp only: real_norm_def abs_diff_less_iff)
    2.65  
    2.66    from N have "\<forall>n\<ge>N. X N - r/2 < X n" by fast
    2.67    hence "X N - r/2 \<in> S" by (rule mem_S)
    2.68 @@ -1159,7 +1177,7 @@
    2.69      fix n assume n: "N \<le> n"
    2.70      from N n have "X n < X N + r/2" and "X N - r/2 < X n" by simp+
    2.71      thus "norm (X n - x) < r" using 1 2
    2.72 -      by (simp add: real_abs_diff_less_iff)
    2.73 +      by (simp add: abs_diff_less_iff)
    2.74    qed
    2.75  qed
    2.76  
     3.1 --- a/src/HOL/Series.thy	Wed Sep 23 11:06:32 2009 +0100
     3.2 +++ b/src/HOL/Series.thy	Fri Sep 25 13:47:28 2009 +0100
     3.3 @@ -104,6 +104,9 @@
     3.4       "summable f ==> (%n. setsum f {0..<n}) ----> (suminf f)"
     3.5  by (rule summable_sums [unfolded sums_def])
     3.6  
     3.7 +lemma suminf_eq_lim: "suminf f = lim (%n. setsum f {0..<n})"
     3.8 +  by (simp add: suminf_def sums_def lim_def) 
     3.9 +
    3.10  (*-------------------
    3.11      sum is unique                    
    3.12   ------------------*)
    3.13 @@ -112,6 +115,9 @@
    3.14  apply (auto intro!: LIMSEQ_unique simp add: sums_def)
    3.15  done
    3.16  
    3.17 +lemma sums_iff: "f sums x \<longleftrightarrow> summable f \<and> (suminf f = x)"
    3.18 +  by (metis summable_sums sums_summable sums_unique)
    3.19 +
    3.20  lemma sums_split_initial_segment: "f sums s ==> 
    3.21    (%n. f(n + k)) sums (s - (SUM i = 0..< k. f i))"
    3.22    apply (unfold sums_def);
    3.23 @@ -368,6 +374,11 @@
    3.24  apply (drule_tac x="n" in spec, simp)
    3.25  done
    3.26  
    3.27 +lemma suminf_le:
    3.28 +  fixes x :: real
    3.29 +  shows "summable f \<Longrightarrow> (!!n. setsum f {0..<n} \<le> x) \<Longrightarrow> suminf f \<le> x"
    3.30 +  by (simp add: summable_convergent_sumr_iff suminf_eq_lim lim_le) 
    3.31 +
    3.32  lemma summable_Cauchy:
    3.33       "summable (f::nat \<Rightarrow> 'a::banach) =  
    3.34        (\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. norm (setsum f {m..<n}) < e)"