author paulson Thu Mar 26 14:10:48 2009 +0000 (2009-03-26) changeset 30730 4d3565f2cb0e parent 30715 e23e15f52d42 child 30731 da8598ec4e98
New theorems mostly concerning infinite series.
 src/HOL/Power.thy file | annotate | diff | revisions src/HOL/SEQ.thy file | annotate | diff | revisions
```     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.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
```