New theorems mostly concerning infinite series.
authorpaulson
Thu Mar 26 14:10:48 2009 +0000 (2009-03-26)
changeset 307304d3565f2cb0e
parent 30715 e23e15f52d42
child 30731 da8598ec4e98
New theorems mostly concerning infinite series.
src/HOL/Power.thy
src/HOL/SEQ.thy
     1.1 --- a/src/HOL/Power.thy	Wed Mar 25 14:47:08 2009 +0100
     1.2 +++ b/src/HOL/Power.thy	Thu Mar 26 14:10:48 2009 +0000
     1.3 @@ -186,6 +186,10 @@
     1.4  apply (auto simp add: abs_mult)
     1.5  done
     1.6  
     1.7 +lemma abs_power_minus [simp]:
     1.8 +  fixes a:: "'a::{ordered_idom,recpower}" shows "abs((-a) ^ n) = abs(a ^ n)"
     1.9 +  by (simp add: abs_minus_cancel power_abs) 
    1.10 +
    1.11  lemma zero_less_power_abs_iff [simp,noatp]:
    1.12       "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_idom,recpower}) | n=0)"
    1.13  proof (induct "n")
     2.1 --- a/src/HOL/SEQ.thy	Wed Mar 25 14:47:08 2009 +0100
     2.2 +++ b/src/HOL/SEQ.thy	Thu Mar 26 14:10:48 2009 +0000
     2.3 @@ -40,10 +40,23 @@
     2.4  
     2.5  definition
     2.6    monoseq :: "(nat=>real)=>bool" where
     2.7 -    --{*Definition for monotonicity*}
     2.8 +    --{*Definition of monotonicity. 
     2.9 +        The use of disjunction here complicates proofs considerably. 
    2.10 +        One alternative is to add a Boolean argument to indicate the direction. 
    2.11 +        Another is to develop the notions of increasing and decreasing first.*}
    2.12    [code del]: "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
    2.13  
    2.14  definition
    2.15 +  incseq :: "(nat=>real)=>bool" where
    2.16 +    --{*Increasing sequence*}
    2.17 +  [code del]: "incseq X = (\<forall>m. \<forall>n\<ge>m. X m \<le> X n)"
    2.18 +
    2.19 +definition
    2.20 +  decseq :: "(nat=>real)=>bool" where
    2.21 +    --{*Increasing sequence*}
    2.22 +  [code del]: "decseq X = (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
    2.23 +
    2.24 +definition
    2.25    subseq :: "(nat => nat) => bool" where
    2.26      --{*Definition of subsequence*}
    2.27    [code del]:   "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
    2.28 @@ -886,6 +899,14 @@
    2.29    thus ?case by arith
    2.30  qed
    2.31  
    2.32 +lemma LIMSEQ_subseq_LIMSEQ:
    2.33 +  "\<lbrakk> X ----> L; subseq f \<rbrakk> \<Longrightarrow> (X o f) ----> L"
    2.34 +apply (auto simp add: LIMSEQ_def) 
    2.35 +apply (drule_tac x=r in spec, clarify)  
    2.36 +apply (rule_tac x=no in exI, clarify) 
    2.37 +apply (blast intro: seq_suble le_trans dest!: spec) 
    2.38 +done
    2.39 +
    2.40  subsection {* Bounded Monotonic Sequences *}
    2.41  
    2.42  
    2.43 @@ -1021,6 +1042,47 @@
    2.44  apply (auto intro!: Bseq_mono_convergent)
    2.45  done
    2.46  
    2.47 +subsubsection{*Increasing and Decreasing Series*}
    2.48 +
    2.49 +lemma incseq_imp_monoseq:  "incseq X \<Longrightarrow> monoseq X"
    2.50 +  by (simp add: incseq_def monoseq_def) 
    2.51 +
    2.52 +lemma incseq_le: assumes inc: "incseq X" and lim: "X ----> L" shows "X n \<le> L"
    2.53 +  using monoseq_le [OF incseq_imp_monoseq [OF inc] lim]
    2.54 +proof
    2.55 +  assume "(\<forall>n. X n \<le> L) \<and> (\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n)"
    2.56 +  thus ?thesis by simp
    2.57 +next
    2.58 +  assume "(\<forall>n. L \<le> X n) \<and> (\<forall>m n. m \<le> n \<longrightarrow> X n \<le> X m)"
    2.59 +  hence const: "(!!m n. m \<le> n \<Longrightarrow> X n = X m)" using inc
    2.60 +    by (auto simp add: incseq_def intro: order_antisym)
    2.61 +  have X: "!!n. X n = X 0"
    2.62 +    by (blast intro: const [of 0]) 
    2.63 +  have "X = (\<lambda>n. X 0)"
    2.64 +    by (blast intro: ext X)
    2.65 +  hence "L = X 0" using LIMSEQ_const [of "X 0"]
    2.66 +    by (auto intro: LIMSEQ_unique lim) 
    2.67 +  thus ?thesis
    2.68 +    by (blast intro: eq_refl X)
    2.69 +qed
    2.70 +
    2.71 +lemma decseq_imp_monoseq:  "decseq X \<Longrightarrow> monoseq X"
    2.72 +  by (simp add: decseq_def monoseq_def)
    2.73 +
    2.74 +lemma decseq_eq_incseq: "decseq X = incseq (\<lambda>n. - X n)" 
    2.75 +  by (simp add: decseq_def incseq_def)
    2.76 +
    2.77 +
    2.78 +lemma decseq_le: assumes dec: "decseq X" and lim: "X ----> L" shows "L \<le> X n"
    2.79 +proof -
    2.80 +  have inc: "incseq (\<lambda>n. - X n)" using dec
    2.81 +    by (simp add: decseq_eq_incseq)
    2.82 +  have "- X n \<le> - L" 
    2.83 +    by (blast intro: incseq_le [OF inc] LIMSEQ_minus lim) 
    2.84 +  thus ?thesis
    2.85 +    by simp
    2.86 +qed
    2.87 +
    2.88  subsubsection{*A Few More Equivalence Theorems for Boundedness*}
    2.89  
    2.90  text{*alternative formulation for boundedness*}
    2.91 @@ -1065,6 +1127,14 @@
    2.92    "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e"
    2.93  by (simp add: Cauchy_def)
    2.94  
    2.95 +lemma Cauchy_subseq_Cauchy:
    2.96 +  "\<lbrakk> Cauchy X; subseq f \<rbrakk> \<Longrightarrow> Cauchy (X o f)"
    2.97 +apply (auto simp add: Cauchy_def) 
    2.98 +apply (drule_tac x=e in spec, clarify)  
    2.99 +apply (rule_tac x=M in exI, clarify) 
   2.100 +apply (blast intro: seq_suble le_trans dest!: spec) 
   2.101 +done
   2.102 +
   2.103  subsubsection {* Cauchy Sequences are Bounded *}
   2.104  
   2.105  text{*A Cauchy sequence is bounded -- this is the standard
   2.106 @@ -1238,6 +1308,11 @@
   2.107    shows "Cauchy X = convergent X"
   2.108  by (fast intro: Cauchy_convergent convergent_Cauchy)
   2.109  
   2.110 +lemma convergent_subseq_convergent:
   2.111 +  fixes X :: "nat \<Rightarrow> 'a::banach"
   2.112 +  shows "\<lbrakk> convergent X; subseq f \<rbrakk> \<Longrightarrow> convergent (X o f)"
   2.113 +  by (simp add: Cauchy_subseq_Cauchy Cauchy_convergent_iff [symmetric]) 
   2.114 +
   2.115  
   2.116  subsection {* Power Sequences *}
   2.117