author | hoelzl |
Mon, 03 Dec 2012 18:19:08 +0100 | |
changeset 50328 | 25b1e8686ce0 |
parent 50087 | 635d73673b5e |
child 50331 | 4b6dc5077e98 |
permissions | -rw-r--r-- |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32877
diff
changeset
|
1 |
(* Title: HOL/SEQ.thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32877
diff
changeset
|
2 |
Author: Jacques D. Fleuriot, University of Cambridge |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32877
diff
changeset
|
3 |
Author: Lawrence C Paulson |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32877
diff
changeset
|
4 |
Author: Jeremy Avigad |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32877
diff
changeset
|
5 |
Author: Brian Huffman |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32877
diff
changeset
|
6 |
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32877
diff
changeset
|
7 |
Convergence of sequences and series. |
15082 | 8 |
*) |
10751 | 9 |
|
22631
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
22629
diff
changeset
|
10 |
header {* Sequences and Convergence *} |
17439 | 11 |
|
15131 | 12 |
theory SEQ |
36822 | 13 |
imports Limits RComplete |
15131 | 14 |
begin |
10751 | 15 |
|
41972 | 16 |
subsection {* Monotone sequences and subsequences *} |
10751 | 17 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21139
diff
changeset
|
18 |
definition |
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
19 |
monoseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where |
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
20 |
--{*Definition of monotonicity. |
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
21 |
The use of disjunction here complicates proofs considerably. |
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
22 |
One alternative is to add a Boolean argument to indicate the direction. |
30730 | 23 |
Another is to develop the notions of increasing and decreasing first.*} |
37767 | 24 |
"monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))" |
10751 | 25 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21139
diff
changeset
|
26 |
definition |
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
27 |
incseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where |
30730 | 28 |
--{*Increasing sequence*} |
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
29 |
"incseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X m \<le> X n)" |
30730 | 30 |
|
31 |
definition |
|
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
32 |
decseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where |
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
33 |
--{*Decreasing sequence*} |
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
34 |
"decseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)" |
30730 | 35 |
|
36 |
definition |
|
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
37 |
subseq :: "(nat \<Rightarrow> nat) \<Rightarrow> bool" where |
15082 | 38 |
--{*Definition of subsequence*} |
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
39 |
"subseq f \<longleftrightarrow> (\<forall>m. \<forall>n>m. f m < f n)" |
10751 | 40 |
|
41972 | 41 |
lemma incseq_mono: "mono f \<longleftrightarrow> incseq f" |
42 |
unfolding mono_def incseq_def by auto |
|
43 |
||
44 |
lemma incseq_SucI: |
|
45 |
"(\<And>n. X n \<le> X (Suc n)) \<Longrightarrow> incseq X" |
|
46 |
using lift_Suc_mono_le[of X] |
|
47 |
by (auto simp: incseq_def) |
|
48 |
||
49 |
lemma incseqD: "\<And>i j. incseq f \<Longrightarrow> i \<le> j \<Longrightarrow> f i \<le> f j" |
|
50 |
by (auto simp: incseq_def) |
|
51 |
||
52 |
lemma incseq_SucD: "incseq A \<Longrightarrow> A i \<le> A (Suc i)" |
|
53 |
using incseqD[of A i "Suc i"] by auto |
|
54 |
||
55 |
lemma incseq_Suc_iff: "incseq f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))" |
|
56 |
by (auto intro: incseq_SucI dest: incseq_SucD) |
|
57 |
||
58 |
lemma incseq_const[simp, intro]: "incseq (\<lambda>x. k)" |
|
59 |
unfolding incseq_def by auto |
|
60 |
||
61 |
lemma decseq_SucI: |
|
62 |
"(\<And>n. X (Suc n) \<le> X n) \<Longrightarrow> decseq X" |
|
63 |
using order.lift_Suc_mono_le[OF dual_order, of X] |
|
64 |
by (auto simp: decseq_def) |
|
65 |
||
66 |
lemma decseqD: "\<And>i j. decseq f \<Longrightarrow> i \<le> j \<Longrightarrow> f j \<le> f i" |
|
67 |
by (auto simp: decseq_def) |
|
68 |
||
69 |
lemma decseq_SucD: "decseq A \<Longrightarrow> A (Suc i) \<le> A i" |
|
70 |
using decseqD[of A i "Suc i"] by auto |
|
71 |
||
72 |
lemma decseq_Suc_iff: "decseq f \<longleftrightarrow> (\<forall>n. f (Suc n) \<le> f n)" |
|
73 |
by (auto intro: decseq_SucI dest: decseq_SucD) |
|
74 |
||
75 |
lemma decseq_const[simp, intro]: "decseq (\<lambda>x. k)" |
|
76 |
unfolding decseq_def by auto |
|
77 |
||
78 |
lemma monoseq_iff: "monoseq X \<longleftrightarrow> incseq X \<or> decseq X" |
|
79 |
unfolding monoseq_def incseq_def decseq_def .. |
|
80 |
||
81 |
lemma monoseq_Suc: |
|
82 |
"monoseq X \<longleftrightarrow> (\<forall>n. X n \<le> X (Suc n)) \<or> (\<forall>n. X (Suc n) \<le> X n)" |
|
83 |
unfolding monoseq_iff incseq_Suc_iff decseq_Suc_iff .. |
|
84 |
||
85 |
lemma monoI1: "\<forall>m. \<forall> n \<ge> m. X m \<le> X n ==> monoseq X" |
|
86 |
by (simp add: monoseq_def) |
|
87 |
||
88 |
lemma monoI2: "\<forall>m. \<forall> n \<ge> m. X n \<le> X m ==> monoseq X" |
|
89 |
by (simp add: monoseq_def) |
|
90 |
||
91 |
lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X" |
|
92 |
by (simp add: monoseq_Suc) |
|
93 |
||
94 |
lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X" |
|
95 |
by (simp add: monoseq_Suc) |
|
96 |
||
97 |
lemma monoseq_minus: |
|
98 |
fixes a :: "nat \<Rightarrow> 'a::ordered_ab_group_add" |
|
99 |
assumes "monoseq a" |
|
100 |
shows "monoseq (\<lambda> n. - a n)" |
|
101 |
proof (cases "\<forall> m. \<forall> n \<ge> m. a m \<le> a n") |
|
102 |
case True |
|
103 |
hence "\<forall> m. \<forall> n \<ge> m. - a n \<le> - a m" by auto |
|
104 |
thus ?thesis by (rule monoI2) |
|
105 |
next |
|
106 |
case False |
|
107 |
hence "\<forall> m. \<forall> n \<ge> m. - a m \<le> - a n" using `monoseq a`[unfolded monoseq_def] by auto |
|
108 |
thus ?thesis by (rule monoI1) |
|
109 |
qed |
|
110 |
||
111 |
text{*Subsequence (alternative definition, (e.g. Hoskins)*} |
|
112 |
||
113 |
lemma subseq_Suc_iff: "subseq f = (\<forall>n. (f n) < (f (Suc n)))" |
|
114 |
apply (simp add: subseq_def) |
|
115 |
apply (auto dest!: less_imp_Suc_add) |
|
116 |
apply (induct_tac k) |
|
117 |
apply (auto intro: less_trans) |
|
118 |
done |
|
119 |
||
120 |
text{* for any sequence, there is a monotonic subsequence *} |
|
121 |
lemma seq_monosub: |
|
122 |
fixes s :: "nat => 'a::linorder" |
|
123 |
shows "\<exists>f. subseq f \<and> monoseq (\<lambda> n. (s (f n)))" |
|
124 |
proof cases |
|
125 |
let "?P p n" = "p > n \<and> (\<forall>m\<ge>p. s m \<le> s p)" |
|
126 |
assume *: "\<forall>n. \<exists>p. ?P p n" |
|
127 |
def f \<equiv> "nat_rec (SOME p. ?P p 0) (\<lambda>_ n. SOME p. ?P p n)" |
|
128 |
have f_0: "f 0 = (SOME p. ?P p 0)" unfolding f_def by simp |
|
129 |
have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc .. |
|
130 |
have P_0: "?P (f 0) 0" unfolding f_0 using *[rule_format] by (rule someI2_ex) auto |
|
131 |
have P_Suc: "\<And>i. ?P (f (Suc i)) (f i)" unfolding f_Suc using *[rule_format] by (rule someI2_ex) auto |
|
132 |
then have "subseq f" unfolding subseq_Suc_iff by auto |
|
133 |
moreover have "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc |
|
134 |
proof (intro disjI2 allI) |
|
135 |
fix n show "s (f (Suc n)) \<le> s (f n)" |
|
136 |
proof (cases n) |
|
137 |
case 0 with P_Suc[of 0] P_0 show ?thesis by auto |
|
138 |
next |
|
139 |
case (Suc m) |
|
140 |
from P_Suc[of n] Suc have "f (Suc m) \<le> f (Suc (Suc m))" by simp |
|
141 |
with P_Suc Suc show ?thesis by simp |
|
142 |
qed |
|
143 |
qed |
|
144 |
ultimately show ?thesis by auto |
|
145 |
next |
|
146 |
let "?P p m" = "m < p \<and> s m < s p" |
|
147 |
assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. s m \<le> s p))" |
|
148 |
then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. s p < s m" by (force simp: not_le le_less) |
|
149 |
def f \<equiv> "nat_rec (SOME p. ?P p (Suc N)) (\<lambda>_ n. SOME p. ?P p n)" |
|
150 |
have f_0: "f 0 = (SOME p. ?P p (Suc N))" unfolding f_def by simp |
|
151 |
have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc .. |
|
152 |
have P_0: "?P (f 0) (Suc N)" |
|
153 |
unfolding f_0 some_eq_ex[of "\<lambda>p. ?P p (Suc N)"] using N[of "Suc N"] by auto |
|
154 |
{ fix i have "N < f i \<Longrightarrow> ?P (f (Suc i)) (f i)" |
|
155 |
unfolding f_Suc some_eq_ex[of "\<lambda>p. ?P p (f i)"] using N[of "f i"] . } |
|
156 |
note P' = this |
|
157 |
{ fix i have "N < f i \<and> ?P (f (Suc i)) (f i)" |
|
158 |
by (induct i) (insert P_0 P', auto) } |
|
159 |
then have "subseq f" "monoseq (\<lambda>x. s (f x))" |
|
160 |
unfolding subseq_Suc_iff monoseq_Suc by (auto simp: not_le intro: less_imp_le) |
|
161 |
then show ?thesis by auto |
|
162 |
qed |
|
163 |
||
164 |
lemma seq_suble: assumes sf: "subseq f" shows "n \<le> f n" |
|
165 |
proof(induct n) |
|
166 |
case 0 thus ?case by simp |
|
167 |
next |
|
168 |
case (Suc n) |
|
169 |
from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps |
|
170 |
have "n < f (Suc n)" by arith |
|
171 |
thus ?case by arith |
|
172 |
qed |
|
173 |
||
50087 | 174 |
lemma subseq_o: "subseq r \<Longrightarrow> subseq s \<Longrightarrow> subseq (r \<circ> s)" |
175 |
unfolding subseq_def by simp |
|
176 |
||
177 |
lemma subseq_mono: assumes "subseq r" "m < n" shows "r m < r n" |
|
178 |
using assms by (auto simp: subseq_def) |
|
179 |
||
41972 | 180 |
lemma incseq_imp_monoseq: "incseq X \<Longrightarrow> monoseq X" |
181 |
by (simp add: incseq_def monoseq_def) |
|
182 |
||
183 |
lemma decseq_imp_monoseq: "decseq X \<Longrightarrow> monoseq X" |
|
184 |
by (simp add: decseq_def monoseq_def) |
|
185 |
||
186 |
lemma decseq_eq_incseq: |
|
187 |
fixes X :: "nat \<Rightarrow> 'a::ordered_ab_group_add" shows "decseq X = incseq (\<lambda>n. - X n)" |
|
188 |
by (simp add: decseq_def incseq_def) |
|
189 |
||
50087 | 190 |
lemma INT_decseq_offset: |
191 |
assumes "decseq F" |
|
192 |
shows "(\<Inter>i. F i) = (\<Inter>i\<in>{n..}. F i)" |
|
193 |
proof safe |
|
194 |
fix x i assume x: "x \<in> (\<Inter>i\<in>{n..}. F i)" |
|
195 |
show "x \<in> F i" |
|
196 |
proof cases |
|
197 |
from x have "x \<in> F n" by auto |
|
198 |
also assume "i \<le> n" with `decseq F` have "F n \<subseteq> F i" |
|
199 |
unfolding decseq_def by simp |
|
200 |
finally show ?thesis . |
|
201 |
qed (insert x, simp) |
|
202 |
qed auto |
|
203 |
||
41972 | 204 |
subsection {* Defintions of limits *} |
205 |
||
44206
5e4a1664106e
locale-ize some constant definitions, so complete_space can inherit from metric_space
huffman
parents:
44205
diff
changeset
|
206 |
abbreviation (in topological_space) |
5e4a1664106e
locale-ize some constant definitions, so complete_space can inherit from metric_space
huffman
parents:
44205
diff
changeset
|
207 |
LIMSEQ :: "[nat \<Rightarrow> 'a, 'a] \<Rightarrow> bool" |
41972 | 208 |
("((_)/ ----> (_))" [60, 60] 60) where |
209 |
"X ----> L \<equiv> (X ---> L) sequentially" |
|
210 |
||
211 |
definition |
|
44205
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44194
diff
changeset
|
212 |
lim :: "(nat \<Rightarrow> 'a::t2_space) \<Rightarrow> 'a" where |
41972 | 213 |
--{*Standard definition of limit using choice operator*} |
214 |
"lim X = (THE L. X ----> L)" |
|
215 |
||
44206
5e4a1664106e
locale-ize some constant definitions, so complete_space can inherit from metric_space
huffman
parents:
44205
diff
changeset
|
216 |
definition (in topological_space) convergent :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where |
41972 | 217 |
"convergent X = (\<exists>L. X ----> L)" |
218 |
||
219 |
definition |
|
220 |
Bseq :: "(nat => 'a::real_normed_vector) => bool" where |
|
221 |
--{*Standard definition for bounded sequence*} |
|
222 |
"Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)" |
|
223 |
||
44206
5e4a1664106e
locale-ize some constant definitions, so complete_space can inherit from metric_space
huffman
parents:
44205
diff
changeset
|
224 |
definition (in metric_space) Cauchy :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where |
37767 | 225 |
"Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)" |
10751 | 226 |
|
15082 | 227 |
|
22608 | 228 |
subsection {* Bounded Sequences *} |
229 |
||
26312 | 230 |
lemma BseqI': assumes K: "\<And>n. norm (X n) \<le> K" shows "Bseq X" |
22608 | 231 |
unfolding Bseq_def |
232 |
proof (intro exI conjI allI) |
|
233 |
show "0 < max K 1" by simp |
|
234 |
next |
|
235 |
fix n::nat |
|
236 |
have "norm (X n) \<le> K" by (rule K) |
|
237 |
thus "norm (X n) \<le> max K 1" by simp |
|
238 |
qed |
|
239 |
||
240 |
lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
|
241 |
unfolding Bseq_def by auto |
|
242 |
||
26312 | 243 |
lemma BseqI2': assumes K: "\<forall>n\<ge>N. norm (X n) \<le> K" shows "Bseq X" |
244 |
proof (rule BseqI') |
|
22608 | 245 |
let ?A = "norm ` X ` {..N}" |
246 |
have 1: "finite ?A" by simp |
|
247 |
fix n::nat |
|
248 |
show "norm (X n) \<le> max K (Max ?A)" |
|
249 |
proof (cases rule: linorder_le_cases) |
|
250 |
assume "n \<ge> N" |
|
251 |
hence "norm (X n) \<le> K" using K by simp |
|
252 |
thus "norm (X n) \<le> max K (Max ?A)" by simp |
|
253 |
next |
|
254 |
assume "n \<le> N" |
|
255 |
hence "norm (X n) \<in> ?A" by simp |
|
26757
e775accff967
thms Max_ge, Min_le: dropped superfluous premise
haftmann
parents:
26312
diff
changeset
|
256 |
with 1 have "norm (X n) \<le> Max ?A" by (rule Max_ge) |
22608 | 257 |
thus "norm (X n) \<le> max K (Max ?A)" by simp |
258 |
qed |
|
259 |
qed |
|
260 |
||
261 |
lemma Bseq_ignore_initial_segment: "Bseq X \<Longrightarrow> Bseq (\<lambda>n. X (n + k))" |
|
262 |
unfolding Bseq_def by auto |
|
263 |
||
264 |
lemma Bseq_offset: "Bseq (\<lambda>n. X (n + k)) \<Longrightarrow> Bseq X" |
|
265 |
apply (erule BseqE) |
|
26312 | 266 |
apply (rule_tac N="k" and K="K" in BseqI2') |
22608 | 267 |
apply clarify |
268 |
apply (drule_tac x="n - k" in spec, simp) |
|
269 |
done |
|
270 |
||
31355 | 271 |
lemma Bseq_conv_Bfun: "Bseq X \<longleftrightarrow> Bfun X sequentially" |
272 |
unfolding Bfun_def eventually_sequentially |
|
273 |
apply (rule iffI) |
|
32064 | 274 |
apply (simp add: Bseq_def) |
275 |
apply (auto intro: BseqI2') |
|
31355 | 276 |
done |
277 |
||
22608 | 278 |
|
20696 | 279 |
subsection {* Limits of Sequences *} |
280 |
||
32877
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
281 |
lemma [trans]: "X=Y ==> Y ----> z ==> X ----> z" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
282 |
by simp |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
283 |
|
36660
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
284 |
lemma LIMSEQ_def: "X ----> L = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)" |
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
285 |
unfolding tendsto_iff eventually_sequentially .. |
31392 | 286 |
|
15082 | 287 |
lemma LIMSEQ_iff: |
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
288 |
fixes L :: "'a::real_normed_vector" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
289 |
shows "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
290 |
unfolding LIMSEQ_def dist_norm .. |
22608 | 291 |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33042
diff
changeset
|
292 |
lemma LIMSEQ_iff_nz: "X ----> L = (\<forall>r>0. \<exists>no>0. \<forall>n\<ge>no. dist (X n) L < r)" |
36660
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
293 |
unfolding LIMSEQ_def by (metis Suc_leD zero_less_Suc) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33042
diff
changeset
|
294 |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
295 |
lemma metric_LIMSEQ_I: |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
296 |
"(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r) \<Longrightarrow> X ----> L" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
297 |
by (simp add: LIMSEQ_def) |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
298 |
|
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
299 |
lemma metric_LIMSEQ_D: |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
300 |
"\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
301 |
by (simp add: LIMSEQ_def) |
15082 | 302 |
|
20751
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
303 |
lemma LIMSEQ_I: |
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
304 |
fixes L :: "'a::real_normed_vector" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
305 |
shows "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r) \<Longrightarrow> X ----> L" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
306 |
by (simp add: LIMSEQ_iff) |
20751
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
307 |
|
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
308 |
lemma LIMSEQ_D: |
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
309 |
fixes L :: "'a::real_normed_vector" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
310 |
shows "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
311 |
by (simp add: LIMSEQ_iff) |
20751
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
312 |
|
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
313 |
lemma LIMSEQ_const_iff: |
44205
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44194
diff
changeset
|
314 |
fixes k l :: "'a::t2_space" |
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
315 |
shows "(\<lambda>n. k) ----> l \<longleftrightarrow> k = l" |
44205
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44194
diff
changeset
|
316 |
using trivial_limit_sequentially by (rule tendsto_const_iff) |
22608 | 317 |
|
22615 | 318 |
lemma LIMSEQ_ignore_initial_segment: |
319 |
"f ----> a \<Longrightarrow> (\<lambda>n. f (n + k)) ----> a" |
|
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
320 |
apply (rule topological_tendstoI) |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
321 |
apply (drule (2) topological_tendstoD) |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
322 |
apply (simp only: eventually_sequentially) |
22615 | 323 |
apply (erule exE, rename_tac N) |
324 |
apply (rule_tac x=N in exI) |
|
325 |
apply simp |
|
326 |
done |
|
20696 | 327 |
|
22615 | 328 |
lemma LIMSEQ_offset: |
329 |
"(\<lambda>n. f (n + k)) ----> a \<Longrightarrow> f ----> a" |
|
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
330 |
apply (rule topological_tendstoI) |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
331 |
apply (drule (2) topological_tendstoD) |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
332 |
apply (simp only: eventually_sequentially) |
22615 | 333 |
apply (erule exE, rename_tac N) |
334 |
apply (rule_tac x="N + k" in exI) |
|
335 |
apply clarify |
|
336 |
apply (drule_tac x="n - k" in spec) |
|
337 |
apply (simp add: le_diff_conv2) |
|
20696 | 338 |
done |
339 |
||
22615 | 340 |
lemma LIMSEQ_Suc: "f ----> l \<Longrightarrow> (\<lambda>n. f (Suc n)) ----> l" |
30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29803
diff
changeset
|
341 |
by (drule_tac k="Suc 0" in LIMSEQ_ignore_initial_segment, simp) |
22615 | 342 |
|
343 |
lemma LIMSEQ_imp_Suc: "(\<lambda>n. f (Suc n)) ----> l \<Longrightarrow> f ----> l" |
|
30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29803
diff
changeset
|
344 |
by (rule_tac k="Suc 0" in LIMSEQ_offset, simp) |
22615 | 345 |
|
346 |
lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) ----> l = f ----> l" |
|
347 |
by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc) |
|
348 |
||
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
349 |
lemma LIMSEQ_linear: "\<lbrakk> X ----> x ; l > 0 \<rbrakk> \<Longrightarrow> (\<lambda> n. X (n * l)) ----> x" |
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
350 |
unfolding tendsto_def eventually_sequentially |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
351 |
by (metis div_le_dividend div_mult_self1_is_m le_trans nat_mult_commute) |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
352 |
|
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
353 |
lemma LIMSEQ_unique: |
44205
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44194
diff
changeset
|
354 |
fixes a b :: "'a::t2_space" |
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
355 |
shows "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b" |
44205
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44194
diff
changeset
|
356 |
using trivial_limit_sequentially by (rule tendsto_unique) |
22608 | 357 |
|
32877
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
358 |
lemma increasing_LIMSEQ: |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
359 |
fixes f :: "nat \<Rightarrow> real" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
360 |
assumes inc: "!!n. f n \<le> f (Suc n)" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
361 |
and bdd: "!!n. f n \<le> l" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
362 |
and en: "!!e. 0 < e \<Longrightarrow> \<exists>n. l \<le> f n + e" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
363 |
shows "f ----> l" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
364 |
proof (auto simp add: LIMSEQ_def) |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
365 |
fix e :: real |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
366 |
assume e: "0 < e" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
367 |
then obtain N where "l \<le> f N + e/2" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
368 |
by (metis half_gt_zero e en that) |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
369 |
hence N: "l < f N + e" using e |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
370 |
by simp |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
371 |
{ fix k |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
372 |
have [simp]: "!!n. \<bar>f n - l\<bar> = l - f n" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
373 |
by (simp add: bdd) |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
374 |
have "\<bar>f (N+k) - l\<bar> < e" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
375 |
proof (induct k) |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
376 |
case 0 show ?case using N |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32877
diff
changeset
|
377 |
by simp |
32877
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
378 |
next |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
379 |
case (Suc k) thus ?case using N inc [of "N+k"] |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32877
diff
changeset
|
380 |
by simp |
32877
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
381 |
qed |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
382 |
} note 1 = this |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
383 |
{ fix n |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
384 |
have "N \<le> n \<Longrightarrow> \<bar>f n - l\<bar> < e" using 1 [of "n-N"] |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
385 |
by simp |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
386 |
} note [intro] = this |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
387 |
show " \<exists>no. \<forall>n\<ge>no. dist (f n) l < e" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
388 |
by (auto simp add: dist_real_def) |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
389 |
qed |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
390 |
|
22608 | 391 |
lemma Bseq_inverse_lemma: |
392 |
fixes x :: "'a::real_normed_div_algebra" |
|
393 |
shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r" |
|
394 |
apply (subst nonzero_norm_inverse, clarsimp) |
|
395 |
apply (erule (1) le_imp_inverse_le) |
|
396 |
done |
|
397 |
||
398 |
lemma Bseq_inverse: |
|
399 |
fixes a :: "'a::real_normed_div_algebra" |
|
31355 | 400 |
shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))" |
36660
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
401 |
unfolding Bseq_conv_Bfun by (rule Bfun_inverse) |
22608 | 402 |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
403 |
lemma LIMSEQ_diff_approach_zero: |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
404 |
fixes L :: "'a::real_normed_vector" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
405 |
shows "g ----> L ==> (%x. f x - g x) ----> 0 ==> f ----> L" |
44313 | 406 |
by (drule (1) tendsto_add, simp) |
22614 | 407 |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
408 |
lemma LIMSEQ_diff_approach_zero2: |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
409 |
fixes L :: "'a::real_normed_vector" |
35292
e4a431b6d9b7
Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
35216
diff
changeset
|
410 |
shows "f ----> L ==> (%x. f x - g x) ----> 0 ==> g ----> L" |
44313 | 411 |
by (drule (1) tendsto_diff, simp) |
22614 | 412 |
|
413 |
text{*An unbounded sequence's inverse tends to 0*} |
|
414 |
||
415 |
lemma LIMSEQ_inverse_zero: |
|
22974 | 416 |
"\<forall>r::real. \<exists>N. \<forall>n\<ge>N. r < X n \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> 0" |
417 |
apply (rule LIMSEQ_I) |
|
418 |
apply (drule_tac x="inverse r" in spec, safe) |
|
419 |
apply (rule_tac x="N" in exI, safe) |
|
420 |
apply (drule_tac x="n" in spec, safe) |
|
22614 | 421 |
apply (frule positive_imp_inverse_positive) |
22974 | 422 |
apply (frule (1) less_imp_inverse_less) |
423 |
apply (subgoal_tac "0 < X n", simp) |
|
424 |
apply (erule (1) order_less_trans) |
|
22614 | 425 |
done |
426 |
||
427 |
text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*} |
|
428 |
||
429 |
lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0" |
|
430 |
apply (rule LIMSEQ_inverse_zero, safe) |
|
22974 | 431 |
apply (cut_tac x = r in reals_Archimedean2) |
22614 | 432 |
apply (safe, rule_tac x = n in exI) |
433 |
apply (auto simp add: real_of_nat_Suc) |
|
434 |
done |
|
435 |
||
436 |
text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to |
|
437 |
infinity is now easily proved*} |
|
438 |
||
439 |
lemma LIMSEQ_inverse_real_of_nat_add: |
|
440 |
"(%n. r + inverse(real(Suc n))) ----> r" |
|
44313 | 441 |
using tendsto_add [OF tendsto_const LIMSEQ_inverse_real_of_nat] by auto |
22614 | 442 |
|
443 |
lemma LIMSEQ_inverse_real_of_nat_add_minus: |
|
444 |
"(%n. r + -inverse(real(Suc n))) ----> r" |
|
44710 | 445 |
using tendsto_add [OF tendsto_const |
446 |
tendsto_minus [OF LIMSEQ_inverse_real_of_nat]] by auto |
|
22614 | 447 |
|
448 |
lemma LIMSEQ_inverse_real_of_nat_add_minus_mult: |
|
449 |
"(%n. r*( 1 + -inverse(real(Suc n)))) ----> r" |
|
44313 | 450 |
using tendsto_mult [OF tendsto_const |
451 |
LIMSEQ_inverse_real_of_nat_add_minus [of 1]] |
|
452 |
by auto |
|
22614 | 453 |
|
22615 | 454 |
lemma LIMSEQ_le_const: |
455 |
"\<lbrakk>X ----> (x::real); \<exists>N. \<forall>n\<ge>N. a \<le> X n\<rbrakk> \<Longrightarrow> a \<le> x" |
|
456 |
apply (rule ccontr, simp only: linorder_not_le) |
|
457 |
apply (drule_tac r="a - x" in LIMSEQ_D, simp) |
|
458 |
apply clarsimp |
|
459 |
apply (drule_tac x="max N no" in spec, drule mp, rule le_maxI1) |
|
460 |
apply (drule_tac x="max N no" in spec, drule mp, rule le_maxI2) |
|
461 |
apply simp |
|
462 |
done |
|
463 |
||
464 |
lemma LIMSEQ_le_const2: |
|
465 |
"\<lbrakk>X ----> (x::real); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a" |
|
466 |
apply (subgoal_tac "- a \<le> - x", simp) |
|
467 |
apply (rule LIMSEQ_le_const) |
|
44313 | 468 |
apply (erule tendsto_minus) |
22615 | 469 |
apply simp |
470 |
done |
|
471 |
||
472 |
lemma LIMSEQ_le: |
|
473 |
"\<lbrakk>X ----> x; Y ----> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::real)" |
|
474 |
apply (subgoal_tac "0 \<le> y - x", simp) |
|
475 |
apply (rule LIMSEQ_le_const) |
|
44313 | 476 |
apply (erule (1) tendsto_diff) |
22615 | 477 |
apply (simp add: le_diff_eq) |
478 |
done |
|
479 |
||
15082 | 480 |
|
20696 | 481 |
subsection {* Convergence *} |
15082 | 482 |
|
483 |
lemma limI: "X ----> L ==> lim X = L" |
|
484 |
apply (simp add: lim_def) |
|
485 |
apply (blast intro: LIMSEQ_unique) |
|
486 |
done |
|
487 |
||
488 |
lemma convergentD: "convergent X ==> \<exists>L. (X ----> L)" |
|
489 |
by (simp add: convergent_def) |
|
490 |
||
491 |
lemma convergentI: "(X ----> L) ==> convergent X" |
|
492 |
by (auto simp add: convergent_def) |
|
493 |
||
494 |
lemma convergent_LIMSEQ_iff: "convergent X = (X ----> lim X)" |
|
20682 | 495 |
by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def) |
15082 | 496 |
|
36625 | 497 |
lemma convergent_const: "convergent (\<lambda>n. c)" |
44313 | 498 |
by (rule convergentI, rule tendsto_const) |
36625 | 499 |
|
500 |
lemma convergent_add: |
|
501 |
fixes X Y :: "nat \<Rightarrow> 'a::real_normed_vector" |
|
502 |
assumes "convergent (\<lambda>n. X n)" |
|
503 |
assumes "convergent (\<lambda>n. Y n)" |
|
504 |
shows "convergent (\<lambda>n. X n + Y n)" |
|
44313 | 505 |
using assms unfolding convergent_def by (fast intro: tendsto_add) |
36625 | 506 |
|
507 |
lemma convergent_setsum: |
|
508 |
fixes X :: "'a \<Rightarrow> nat \<Rightarrow> 'b::real_normed_vector" |
|
36647 | 509 |
assumes "\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)" |
36625 | 510 |
shows "convergent (\<lambda>n. \<Sum>i\<in>A. X i n)" |
36647 | 511 |
proof (cases "finite A") |
36650 | 512 |
case True from this and assms show ?thesis |
36647 | 513 |
by (induct A set: finite) (simp_all add: convergent_const convergent_add) |
514 |
qed (simp add: convergent_const) |
|
36625 | 515 |
|
516 |
lemma (in bounded_linear) convergent: |
|
517 |
assumes "convergent (\<lambda>n. X n)" |
|
518 |
shows "convergent (\<lambda>n. f (X n))" |
|
44313 | 519 |
using assms unfolding convergent_def by (fast intro: tendsto) |
36625 | 520 |
|
521 |
lemma (in bounded_bilinear) convergent: |
|
522 |
assumes "convergent (\<lambda>n. X n)" and "convergent (\<lambda>n. Y n)" |
|
523 |
shows "convergent (\<lambda>n. X n ** Y n)" |
|
44313 | 524 |
using assms unfolding convergent_def by (fast intro: tendsto) |
36625 | 525 |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
526 |
lemma convergent_minus_iff: |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
527 |
fixes X :: "nat \<Rightarrow> 'a::real_normed_vector" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
528 |
shows "convergent X \<longleftrightarrow> convergent (\<lambda>n. - X n)" |
20696 | 529 |
apply (simp add: convergent_def) |
44313 | 530 |
apply (auto dest: tendsto_minus) |
531 |
apply (drule tendsto_minus, auto) |
|
20696 | 532 |
done |
533 |
||
32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
534 |
lemma lim_le: |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
535 |
fixes x :: real |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
536 |
assumes f: "convergent f" and fn_le: "!!n. f n \<le> x" |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
537 |
shows "lim f \<le> x" |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
538 |
proof (rule classical) |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
539 |
assume "\<not> lim f \<le> x" |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
540 |
hence 0: "0 < lim f - x" by arith |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
541 |
have 1: "f----> lim f" |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
542 |
by (metis convergent_LIMSEQ_iff f) |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
543 |
thus ?thesis |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
544 |
proof (simp add: LIMSEQ_iff) |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
545 |
assume "\<forall>r>0. \<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < r" |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
546 |
hence "\<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32877
diff
changeset
|
547 |
by (metis 0) |
32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
548 |
from this obtain no where "\<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32877
diff
changeset
|
549 |
by blast |
32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
550 |
thus "lim f \<le> x" |
37887 | 551 |
by (metis 1 LIMSEQ_le_const2 fn_le) |
32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
552 |
qed |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
553 |
qed |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
554 |
|
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
555 |
lemma monoseq_le: |
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
556 |
fixes a :: "nat \<Rightarrow> real" |
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
557 |
assumes "monoseq a" and "a ----> x" |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
558 |
shows "((\<forall> n. a n \<le> x) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n)) \<or> |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
559 |
((\<forall> n. x \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m))" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
560 |
proof - |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
561 |
{ fix x n fix a :: "nat \<Rightarrow> real" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
562 |
assume "a ----> x" and "\<forall> m. \<forall> n \<ge> m. a m \<le> a n" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
563 |
hence monotone: "\<And> m n. m \<le> n \<Longrightarrow> a m \<le> a n" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
564 |
have "a n \<le> x" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
565 |
proof (rule ccontr) |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
566 |
assume "\<not> a n \<le> x" hence "x < a n" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
567 |
hence "0 < a n - x" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
568 |
from `a ----> x`[THEN LIMSEQ_D, OF this] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
569 |
obtain no where "\<And>n'. no \<le> n' \<Longrightarrow> norm (a n' - x) < a n - x" by blast |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
570 |
hence "norm (a (max no n) - x) < a n - x" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
571 |
moreover |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
572 |
{ fix n' have "n \<le> n' \<Longrightarrow> x < a n'" using monotone[where m=n and n=n'] and `x < a n` by auto } |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
573 |
hence "x < a (max no n)" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
574 |
ultimately |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
575 |
have "a (max no n) < a n" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
576 |
with monotone[where m=n and n="max no n"] |
32436
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32064
diff
changeset
|
577 |
show False by (auto simp:max_def split:split_if_asm) |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
578 |
qed |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
579 |
} note top_down = this |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
580 |
{ fix x n m fix a :: "nat \<Rightarrow> real" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
581 |
assume "a ----> x" and "monoseq a" and "a m < x" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
582 |
have "a n \<le> x \<and> (\<forall> m. \<forall> n \<ge> m. a m \<le> a n)" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
583 |
proof (cases "\<forall> m. \<forall> n \<ge> m. a m \<le> a n") |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
584 |
case True with top_down and `a ----> x` show ?thesis by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
585 |
next |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
586 |
case False with `monoseq a`[unfolded monoseq_def] have "\<forall> m. \<forall> n \<ge> m. - a m \<le> - a n" by auto |
44313 | 587 |
hence "- a m \<le> - x" using top_down[OF tendsto_minus[OF `a ----> x`]] by blast |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
588 |
hence False using `a m < x` by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
589 |
thus ?thesis .. |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
590 |
qed |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
591 |
} note when_decided = this |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
592 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
593 |
show ?thesis |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
594 |
proof (cases "\<exists> m. a m \<noteq> x") |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
595 |
case True then obtain m where "a m \<noteq> x" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
596 |
show ?thesis |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
597 |
proof (cases "a m < x") |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
598 |
case True with when_decided[OF `a ----> x` `monoseq a`, where m2=m] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
599 |
show ?thesis by blast |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
600 |
next |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
601 |
case False hence "- a m < - x" using `a m \<noteq> x` by auto |
44313 | 602 |
with when_decided[OF tendsto_minus[OF `a ----> x`] monoseq_minus[OF `monoseq a`], where m2=m] |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
603 |
show ?thesis by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
604 |
qed |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
605 |
qed auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
606 |
qed |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
607 |
|
30730 | 608 |
lemma LIMSEQ_subseq_LIMSEQ: |
609 |
"\<lbrakk> X ----> L; subseq f \<rbrakk> \<Longrightarrow> (X o f) ----> L" |
|
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
610 |
apply (rule topological_tendstoI) |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
611 |
apply (drule (2) topological_tendstoD) |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
612 |
apply (simp only: eventually_sequentially) |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
613 |
apply (clarify, rule_tac x=N in exI, clarsimp) |
30730 | 614 |
apply (blast intro: seq_suble le_trans dest!: spec) |
615 |
done |
|
616 |
||
44208 | 617 |
lemma convergent_subseq_convergent: |
618 |
"\<lbrakk>convergent X; subseq f\<rbrakk> \<Longrightarrow> convergent (X o f)" |
|
619 |
unfolding convergent_def by (auto intro: LIMSEQ_subseq_LIMSEQ) |
|
620 |
||
621 |
||
30196
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset
|
622 |
subsection {* Bounded Monotonic Sequences *} |
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset
|
623 |
|
20696 | 624 |
text{*Bounded Sequence*} |
15082 | 625 |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
626 |
lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)" |
15082 | 627 |
by (simp add: Bseq_def) |
628 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
629 |
lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X" |
15082 | 630 |
by (auto simp add: Bseq_def) |
631 |
||
632 |
lemma lemma_NBseq_def: |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
633 |
"(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
634 |
(\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))" |
32064 | 635 |
proof auto |
636 |
fix K :: real |
|
637 |
from reals_Archimedean2 obtain n :: nat where "K < real n" .. |
|
638 |
then have "K \<le> real (Suc n)" by auto |
|
639 |
assume "\<forall>m. norm (X m) \<le> K" |
|
640 |
have "\<forall>m. norm (X m) \<le> real (Suc n)" |
|
641 |
proof |
|
642 |
fix m :: 'a |
|
643 |
from `\<forall>m. norm (X m) \<le> K` have "norm (X m) \<le> K" .. |
|
644 |
with `K \<le> real (Suc n)` show "norm (X m) \<le> real (Suc n)" by auto |
|
645 |
qed |
|
646 |
then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" .. |
|
647 |
next |
|
648 |
fix N :: nat |
|
649 |
have "real (Suc N) > 0" by (simp add: real_of_nat_Suc) |
|
650 |
moreover assume "\<forall>n. norm (X n) \<le> real (Suc N)" |
|
651 |
ultimately show "\<exists>K>0. \<forall>n. norm (X n) \<le> K" by blast |
|
652 |
qed |
|
653 |
||
15082 | 654 |
|
655 |
text{* alternative definition for Bseq *} |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
656 |
lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))" |
15082 | 657 |
apply (simp add: Bseq_def) |
658 |
apply (simp (no_asm) add: lemma_NBseq_def) |
|
659 |
done |
|
660 |
||
661 |
lemma lemma_NBseq_def2: |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
662 |
"(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))" |
15082 | 663 |
apply (subst lemma_NBseq_def, auto) |
664 |
apply (rule_tac x = "Suc N" in exI) |
|
665 |
apply (rule_tac [2] x = N in exI) |
|
666 |
apply (auto simp add: real_of_nat_Suc) |
|
667 |
prefer 2 apply (blast intro: order_less_imp_le) |
|
668 |
apply (drule_tac x = n in spec, simp) |
|
669 |
done |
|
670 |
||
671 |
(* yet another definition for Bseq *) |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
672 |
lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))" |
15082 | 673 |
by (simp add: Bseq_def lemma_NBseq_def2) |
674 |
||
20696 | 675 |
subsubsection{*Upper Bounds and Lubs of Bounded Sequences*} |
15082 | 676 |
|
677 |
lemma Bseq_isUb: |
|
678 |
"!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U" |
|
22998 | 679 |
by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff) |
15082 | 680 |
|
681 |
text{* Use completeness of reals (supremum property) |
|
682 |
to show that any bounded sequence has a least upper bound*} |
|
683 |
||
684 |
lemma Bseq_isLub: |
|
685 |
"!!(X::nat=>real). Bseq X ==> |
|
686 |
\<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U" |
|
687 |
by (blast intro: reals_complete Bseq_isUb) |
|
688 |
||
20696 | 689 |
subsubsection{*A Bounded and Monotonic Sequence Converges*} |
15082 | 690 |
|
44714 | 691 |
(* TODO: delete *) |
692 |
(* FIXME: one use in NSA/HSEQ.thy *) |
|
15082 | 693 |
lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)" |
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
694 |
unfolding tendsto_def eventually_sequentially |
15082 | 695 |
apply (rule_tac x = "X m" in exI, safe) |
696 |
apply (rule_tac x = m in exI, safe) |
|
697 |
apply (drule spec, erule impE, auto) |
|
698 |
done |
|
699 |
||
44714 | 700 |
text {* A monotone sequence converges to its least upper bound. *} |
15082 | 701 |
|
44714 | 702 |
lemma isLub_mono_imp_LIMSEQ: |
703 |
fixes X :: "nat \<Rightarrow> real" |
|
704 |
assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *) |
|
705 |
assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n" |
|
706 |
shows "X ----> u" |
|
707 |
proof (rule LIMSEQ_I) |
|
708 |
have 1: "\<forall>n. X n \<le> u" |
|
709 |
using isLubD2 [OF u] by auto |
|
710 |
have "\<forall>y. (\<forall>n. X n \<le> y) \<longrightarrow> u \<le> y" |
|
711 |
using isLub_le_isUb [OF u] by (auto simp add: isUb_def setle_def) |
|
712 |
hence 2: "\<forall>y<u. \<exists>n. y < X n" |
|
713 |
by (metis not_le) |
|
714 |
fix r :: real assume "0 < r" |
|
715 |
hence "u - r < u" by simp |
|
716 |
hence "\<exists>m. u - r < X m" using 2 by simp |
|
717 |
then obtain m where "u - r < X m" .. |
|
718 |
with X have "\<forall>n\<ge>m. u - r < X n" |
|
719 |
by (fast intro: less_le_trans) |
|
720 |
hence "\<exists>m. \<forall>n\<ge>m. u - r < X n" .. |
|
721 |
thus "\<exists>m. \<forall>n\<ge>m. norm (X n - u) < r" |
|
722 |
using 1 by (simp add: diff_less_eq add_commute) |
|
723 |
qed |
|
15082 | 724 |
|
725 |
text{*A standard proof of the theorem for monotone increasing sequence*} |
|
726 |
||
727 |
lemma Bseq_mono_convergent: |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
728 |
"[| Bseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> convergent (X::nat=>real)" |
44714 | 729 |
proof - |
730 |
assume "Bseq X" |
|
731 |
then obtain u where u: "isLub UNIV {x. \<exists>n. X n = x} u" |
|
732 |
using Bseq_isLub by fast |
|
733 |
assume "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n" |
|
734 |
with u have "X ----> u" |
|
735 |
by (rule isLub_mono_imp_LIMSEQ) |
|
736 |
thus "convergent X" |
|
737 |
by (rule convergentI) |
|
738 |
qed |
|
15082 | 739 |
|
740 |
lemma Bseq_minus_iff: "Bseq (%n. -(X n)) = Bseq X" |
|
741 |
by (simp add: Bseq_def) |
|
742 |
||
743 |
text{*Main monotonicity theorem*} |
|
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
744 |
lemma Bseq_monoseq_convergent: "[| Bseq X; monoseq X |] ==> convergent (X::nat\<Rightarrow>real)" |
15082 | 745 |
apply (simp add: monoseq_def, safe) |
746 |
apply (rule_tac [2] convergent_minus_iff [THEN ssubst]) |
|
747 |
apply (drule_tac [2] Bseq_minus_iff [THEN ssubst]) |
|
748 |
apply (auto intro!: Bseq_mono_convergent) |
|
749 |
done |
|
750 |
||
30730 | 751 |
subsubsection{*Increasing and Decreasing Series*} |
752 |
||
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
753 |
lemma incseq_le: |
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
754 |
fixes X :: "nat \<Rightarrow> real" |
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
755 |
assumes inc: "incseq X" and lim: "X ----> L" shows "X n \<le> L" |
30730 | 756 |
using monoseq_le [OF incseq_imp_monoseq [OF inc] lim] |
757 |
proof |
|
758 |
assume "(\<forall>n. X n \<le> L) \<and> (\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n)" |
|
759 |
thus ?thesis by simp |
|
760 |
next |
|
761 |
assume "(\<forall>n. L \<le> X n) \<and> (\<forall>m n. m \<le> n \<longrightarrow> X n \<le> X m)" |
|
762 |
hence const: "(!!m n. m \<le> n \<Longrightarrow> X n = X m)" using inc |
|
763 |
by (auto simp add: incseq_def intro: order_antisym) |
|
764 |
have X: "!!n. X n = X 0" |
|
765 |
by (blast intro: const [of 0]) |
|
766 |
have "X = (\<lambda>n. X 0)" |
|
44568
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44313
diff
changeset
|
767 |
by (blast intro: X) |
44313 | 768 |
hence "L = X 0" using tendsto_const [of "X 0" sequentially] |
769 |
by (auto intro: LIMSEQ_unique lim) |
|
30730 | 770 |
thus ?thesis |
771 |
by (blast intro: eq_refl X) |
|
772 |
qed |
|
773 |
||
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
774 |
lemma decseq_le: |
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
775 |
fixes X :: "nat \<Rightarrow> real" assumes dec: "decseq X" and lim: "X ----> L" shows "L \<le> X n" |
30730 | 776 |
proof - |
777 |
have inc: "incseq (\<lambda>n. - X n)" using dec |
|
778 |
by (simp add: decseq_eq_incseq) |
|
779 |
have "- X n \<le> - L" |
|
44313 | 780 |
by (blast intro: incseq_le [OF inc] tendsto_minus lim) |
30730 | 781 |
thus ?thesis |
782 |
by simp |
|
783 |
qed |
|
784 |
||
20696 | 785 |
subsubsection{*A Few More Equivalence Theorems for Boundedness*} |
15082 | 786 |
|
787 |
text{*alternative formulation for boundedness*} |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
788 |
lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)" |
15082 | 789 |
apply (unfold Bseq_def, safe) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
790 |
apply (rule_tac [2] x = "k + norm x" in exI) |
15360 | 791 |
apply (rule_tac x = K in exI, simp) |
15221 | 792 |
apply (rule exI [where x = 0], auto) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
793 |
apply (erule order_less_le_trans, simp) |
37887 | 794 |
apply (drule_tac x=n in spec, fold diff_minus) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
795 |
apply (drule order_trans [OF norm_triangle_ineq2]) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
796 |
apply simp |
15082 | 797 |
done |
798 |
||
799 |
text{*alternative formulation for boundedness*} |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
800 |
lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)" |
15082 | 801 |
apply safe |
802 |
apply (simp add: Bseq_def, safe) |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
803 |
apply (rule_tac x = "K + norm (X N)" in exI) |
15082 | 804 |
apply auto |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
805 |
apply (erule order_less_le_trans, simp) |
15082 | 806 |
apply (rule_tac x = N in exI, safe) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
807 |
apply (drule_tac x = n in spec) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
808 |
apply (rule order_trans [OF norm_triangle_ineq], simp) |
15082 | 809 |
apply (auto simp add: Bseq_iff2) |
810 |
done |
|
811 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
812 |
lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f" |
15082 | 813 |
apply (simp add: Bseq_def) |
15221 | 814 |
apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto) |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19765
diff
changeset
|
815 |
apply (drule_tac x = n in spec, arith) |
15082 | 816 |
done |
817 |
||
818 |
||
20696 | 819 |
subsection {* Cauchy Sequences *} |
15082 | 820 |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
821 |
lemma metric_CauchyI: |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
822 |
"(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
823 |
by (simp add: Cauchy_def) |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
824 |
|
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
825 |
lemma metric_CauchyD: |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
826 |
"\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e" |
20751
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
827 |
by (simp add: Cauchy_def) |
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
828 |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
829 |
lemma Cauchy_iff: |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
830 |
fixes X :: "nat \<Rightarrow> 'a::real_normed_vector" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
831 |
shows "Cauchy X \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e)" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
832 |
unfolding Cauchy_def dist_norm .. |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
833 |
|
35292
e4a431b6d9b7
Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
35216
diff
changeset
|
834 |
lemma Cauchy_iff2: |
e4a431b6d9b7
Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
35216
diff
changeset
|
835 |
"Cauchy X = |
e4a431b6d9b7
Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
35216
diff
changeset
|
836 |
(\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))" |
e4a431b6d9b7
Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
35216
diff
changeset
|
837 |
apply (simp add: Cauchy_iff, auto) |
e4a431b6d9b7
Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
35216
diff
changeset
|
838 |
apply (drule reals_Archimedean, safe) |
e4a431b6d9b7
Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
35216
diff
changeset
|
839 |
apply (drule_tac x = n in spec, auto) |
e4a431b6d9b7
Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
35216
diff
changeset
|
840 |
apply (rule_tac x = M in exI, auto) |
e4a431b6d9b7
Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
35216
diff
changeset
|
841 |
apply (drule_tac x = m in spec, simp) |
e4a431b6d9b7
Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
35216
diff
changeset
|
842 |
apply (drule_tac x = na in spec, auto) |
e4a431b6d9b7
Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
35216
diff
changeset
|
843 |
done |
e4a431b6d9b7
Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
35216
diff
changeset
|
844 |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
845 |
lemma CauchyI: |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
846 |
fixes X :: "nat \<Rightarrow> 'a::real_normed_vector" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
847 |
shows "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e) \<Longrightarrow> Cauchy X" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
848 |
by (simp add: Cauchy_iff) |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
849 |
|
20751
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
850 |
lemma CauchyD: |
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
851 |
fixes X :: "nat \<Rightarrow> 'a::real_normed_vector" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
852 |
shows "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
853 |
by (simp add: Cauchy_iff) |
20751
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
854 |
|
30730 | 855 |
lemma Cauchy_subseq_Cauchy: |
856 |
"\<lbrakk> Cauchy X; subseq f \<rbrakk> \<Longrightarrow> Cauchy (X o f)" |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
857 |
apply (auto simp add: Cauchy_def) |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
858 |
apply (drule_tac x=e in spec, clarify) |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
859 |
apply (rule_tac x=M in exI, clarify) |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
860 |
apply (blast intro: le_trans [OF _ seq_suble] dest!: spec) |
30730 | 861 |
done |
862 |
||
20696 | 863 |
subsubsection {* Cauchy Sequences are Bounded *} |
864 |
||
15082 | 865 |
text{*A Cauchy sequence is bounded -- this is the standard |
866 |
proof mechanization rather than the nonstandard proof*} |
|
867 |
||
20563 | 868 |
lemma lemmaCauchy: "\<forall>n \<ge> M. norm (X M - X n) < (1::real) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
869 |
==> \<forall>n \<ge> M. norm (X n :: 'a::real_normed_vector) < 1 + norm (X M)" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
870 |
apply (clarify, drule spec, drule (1) mp) |
20563 | 871 |
apply (simp only: norm_minus_commute) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
872 |
apply (drule order_le_less_trans [OF norm_triangle_ineq2]) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
873 |
apply simp |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
874 |
done |
15082 | 875 |
|
876 |
lemma Cauchy_Bseq: "Cauchy X ==> Bseq X" |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
877 |
apply (simp add: Cauchy_iff) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
878 |
apply (drule spec, drule mp, rule zero_less_one, safe) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
879 |
apply (drule_tac x="M" in spec, simp) |
15082 | 880 |
apply (drule lemmaCauchy) |
22608 | 881 |
apply (rule_tac k="M" in Bseq_offset) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
882 |
apply (simp add: Bseq_def) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
883 |
apply (rule_tac x="1 + norm (X M)" in exI) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
884 |
apply (rule conjI, rule order_less_le_trans [OF zero_less_one], simp) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
885 |
apply (simp add: order_less_imp_le) |
15082 | 886 |
done |
887 |
||
20696 | 888 |
subsubsection {* Cauchy Sequences are Convergent *} |
15082 | 889 |
|
44206
5e4a1664106e
locale-ize some constant definitions, so complete_space can inherit from metric_space
huffman
parents:
44205
diff
changeset
|
890 |
class complete_space = metric_space + |
33042 | 891 |
assumes Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X" |
20830
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
892 |
|
33042 | 893 |
class banach = real_normed_vector + complete_space |
31403 | 894 |
|
22629 | 895 |
theorem LIMSEQ_imp_Cauchy: |
896 |
assumes X: "X ----> a" shows "Cauchy X" |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
897 |
proof (rule metric_CauchyI) |
22629 | 898 |
fix e::real assume "0 < e" |
899 |
hence "0 < e/2" by simp |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
900 |
with X have "\<exists>N. \<forall>n\<ge>N. dist (X n) a < e/2" by (rule metric_LIMSEQ_D) |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
901 |
then obtain N where N: "\<forall>n\<ge>N. dist (X n) a < e/2" .. |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
902 |
show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < e" |
22629 | 903 |
proof (intro exI allI impI) |
904 |
fix m assume "N \<le> m" |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
905 |
hence m: "dist (X m) a < e/2" using N by fast |
22629 | 906 |
fix n assume "N \<le> n" |
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
907 |
hence n: "dist (X n) a < e/2" using N by fast |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
908 |
have "dist (X m) (X n) \<le> dist (X m) a + dist (X n) a" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
909 |
by (rule dist_triangle2) |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
910 |
also from m n have "\<dots> < e" by simp |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
911 |
finally show "dist (X m) (X n) < e" . |
22629 | 912 |
qed |
913 |
qed |
|
914 |
||
20691 | 915 |
lemma convergent_Cauchy: "convergent X \<Longrightarrow> Cauchy X" |
22629 | 916 |
unfolding convergent_def |
917 |
by (erule exE, erule LIMSEQ_imp_Cauchy) |
|
20691 | 918 |
|
31403 | 919 |
lemma Cauchy_convergent_iff: |
920 |
fixes X :: "nat \<Rightarrow> 'a::complete_space" |
|
921 |
shows "Cauchy X = convergent X" |
|
922 |
by (fast intro: Cauchy_convergent convergent_Cauchy) |
|
923 |
||
22629 | 924 |
text {* |
925 |
Proof that Cauchy sequences converge based on the one from |
|
926 |
http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html |
|
927 |
*} |
|
928 |
||
929 |
text {* |
|
930 |
If sequence @{term "X"} is Cauchy, then its limit is the lub of |
|
931 |
@{term "{r::real. \<exists>N. \<forall>n\<ge>N. r < X n}"} |
|
932 |
*} |
|
933 |
||
934 |
lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u" |
|
935 |
by (simp add: isUbI setleI) |
|
936 |
||
27681 | 937 |
locale real_Cauchy = |
22629 | 938 |
fixes X :: "nat \<Rightarrow> real" |
939 |
assumes X: "Cauchy X" |
|
940 |
fixes S :: "real set" |
|
941 |
defines S_def: "S \<equiv> {x::real. \<exists>N. \<forall>n\<ge>N. x < X n}" |
|
942 |
||
27681 | 943 |
lemma real_CauchyI: |
944 |
assumes "Cauchy X" |
|
945 |
shows "real_Cauchy X" |
|
28823 | 946 |
proof qed (fact assms) |
27681 | 947 |
|
22629 | 948 |
lemma (in real_Cauchy) mem_S: "\<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S" |
949 |
by (unfold S_def, auto) |
|
950 |
||
951 |
lemma (in real_Cauchy) bound_isUb: |
|
952 |
assumes N: "\<forall>n\<ge>N. X n < x" |
|
953 |
shows "isUb UNIV S x" |
|
954 |
proof (rule isUb_UNIV_I) |
|
955 |
fix y::real assume "y \<in> S" |
|
956 |
hence "\<exists>M. \<forall>n\<ge>M. y < X n" |
|
957 |
by (simp add: S_def) |
|
958 |
then obtain M where "\<forall>n\<ge>M. y < X n" .. |
|
959 |
hence "y < X (max M N)" by simp |
|
960 |
also have "\<dots> < x" using N by simp |
|
961 |
finally show "y \<le> x" |
|
962 |
by (rule order_less_imp_le) |
|
963 |
qed |
|
964 |
||
965 |
lemma (in real_Cauchy) isLub_ex: "\<exists>u. isLub UNIV S u" |
|
966 |
proof (rule reals_complete) |
|
967 |
obtain N where "\<forall>m\<ge>N. \<forall>n\<ge>N. norm (X m - X n) < 1" |
|
32064 | 968 |
using CauchyD [OF X zero_less_one] by auto |
22629 | 969 |
hence N: "\<forall>n\<ge>N. norm (X n - X N) < 1" by simp |
970 |
show "\<exists>x. x \<in> S" |
|
971 |
proof |
|
972 |
from N have "\<forall>n\<ge>N. X N - 1 < X n" |
|
32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
973 |
by (simp add: abs_diff_less_iff) |
22629 | 974 |
thus "X N - 1 \<in> S" by (rule mem_S) |
975 |
qed |
|
976 |
show "\<exists>u. isUb UNIV S u" |
|
977 |
proof |
|
978 |
from N have "\<forall>n\<ge>N. X n < X N + 1" |
|
32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
979 |
by (simp add: abs_diff_less_iff) |
22629 | 980 |
thus "isUb UNIV S (X N + 1)" |
981 |
by (rule bound_isUb) |
|
982 |
qed |
|
983 |
qed |
|
984 |
||
985 |
lemma (in real_Cauchy) isLub_imp_LIMSEQ: |
|
986 |
assumes x: "isLub UNIV S x" |
|
987 |
shows "X ----> x" |
|
988 |
proof (rule LIMSEQ_I) |
|
989 |
fix r::real assume "0 < r" |
|
990 |
hence r: "0 < r/2" by simp |
|
991 |
obtain N where "\<forall>n\<ge>N. \<forall>m\<ge>N. norm (X n - X m) < r/2" |
|
32064 | 992 |
using CauchyD [OF X r] by auto |
22629 | 993 |
hence "\<forall>n\<ge>N. norm (X n - X N) < r/2" by simp |
994 |
hence N: "\<forall>n\<ge>N. X N - r/2 < X n \<and> X n < X N + r/2" |
|
32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
995 |
by (simp only: real_norm_def abs_diff_less_iff) |
22629 | 996 |
|
997 |
from N have "\<forall>n\<ge>N. X N - r/2 < X n" by fast |
|
998 |
hence "X N - r/2 \<in> S" by (rule mem_S) |
|
23482 | 999 |
hence 1: "X N - r/2 \<le> x" using x isLub_isUb isUbD by fast |
22629 | 1000 |
|
1001 |
from N have "\<forall>n\<ge>N. X n < X N + r/2" by fast |
|
1002 |
hence "isUb UNIV S (X N + r/2)" by (rule bound_isUb) |
|
23482 | 1003 |
hence 2: "x \<le> X N + r/2" using x isLub_le_isUb by fast |
22629 | 1004 |
|
1005 |
show "\<exists>N. \<forall>n\<ge>N. norm (X n - x) < r" |
|
1006 |
proof (intro exI allI impI) |
|
1007 |
fix n assume n: "N \<le> n" |
|
23482 | 1008 |
from N n have "X n < X N + r/2" and "X N - r/2 < X n" by simp+ |
1009 |
thus "norm (X n - x) < r" using 1 2 |
|
32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
1010 |
by (simp add: abs_diff_less_iff) |
22629 | 1011 |
qed |
1012 |
qed |
|
1013 |
||
1014 |
lemma (in real_Cauchy) LIMSEQ_ex: "\<exists>x. X ----> x" |
|
1015 |
proof - |
|
1016 |
obtain x where "isLub UNIV S x" |
|
1017 |
using isLub_ex by fast |
|
1018 |
hence "X ----> x" |
|
1019 |
by (rule isLub_imp_LIMSEQ) |
|
1020 |
thus ?thesis .. |
|
1021 |
qed |
|
1022 |
||
20830
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
1023 |
lemma real_Cauchy_convergent: |
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
1024 |
fixes X :: "nat \<Rightarrow> real" |
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
1025 |
shows "Cauchy X \<Longrightarrow> convergent X" |
27681 | 1026 |
unfolding convergent_def |
1027 |
by (rule real_Cauchy.LIMSEQ_ex) |
|
1028 |
(rule real_CauchyI) |
|
20830
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
1029 |
|
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
1030 |
instance real :: banach |
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
1031 |
by intro_classes (rule real_Cauchy_convergent) |
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
1032 |
|
15082 | 1033 |
|
20696 | 1034 |
subsection {* Power Sequences *} |
15082 | 1035 |
|
1036 |
text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term |
|
1037 |
"x<1"}. Proof will use (NS) Cauchy equivalence for convergence and |
|
1038 |
also fact that bounded and monotonic sequence converges.*} |
|
1039 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
1040 |
lemma Bseq_realpow: "[| 0 \<le> (x::real); x \<le> 1 |] ==> Bseq (%n. x ^ n)" |
15082 | 1041 |
apply (simp add: Bseq_def) |
1042 |
apply (rule_tac x = 1 in exI) |
|
1043 |
apply (simp add: power_abs) |
|
22974 | 1044 |
apply (auto dest: power_mono) |
15082 | 1045 |
done |
1046 |
||
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
1047 |
lemma monoseq_realpow: fixes x :: real shows "[| 0 \<le> x; x \<le> 1 |] ==> monoseq (%n. x ^ n)" |
15082 | 1048 |
apply (clarify intro!: mono_SucI2) |
1049 |
apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto) |
|
1050 |
done |
|
1051 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
1052 |
lemma convergent_realpow: |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
1053 |
"[| 0 \<le> (x::real); x \<le> 1 |] ==> convergent (%n. x ^ n)" |
15082 | 1054 |
by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow) |
1055 |
||
22628 | 1056 |
lemma LIMSEQ_inverse_realpow_zero_lemma: |
1057 |
fixes x :: real |
|
1058 |
assumes x: "0 \<le> x" |
|
1059 |
shows "real n * x + 1 \<le> (x + 1) ^ n" |
|
1060 |
apply (induct n) |
|
1061 |
apply simp |
|
1062 |
apply simp |
|
1063 |
apply (rule order_trans) |
|
1064 |
prefer 2 |
|
1065 |
apply (erule mult_left_mono) |
|
1066 |
apply (rule add_increasing [OF x], simp) |
|
1067 |
apply (simp add: real_of_nat_Suc) |
|
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23127
diff
changeset
|
1068 |
apply (simp add: ring_distribs) |
22628 | 1069 |
apply (simp add: mult_nonneg_nonneg x) |
1070 |
done |
|
1071 |
||
1072 |
lemma LIMSEQ_inverse_realpow_zero: |
|
1073 |
"1 < (x::real) \<Longrightarrow> (\<lambda>n. inverse (x ^ n)) ----> 0" |
|
1074 |
proof (rule LIMSEQ_inverse_zero [rule_format]) |
|
1075 |
fix y :: real |
|
1076 |
assume x: "1 < x" |
|
1077 |
hence "0 < x - 1" by simp |
|
1078 |
hence "\<forall>y. \<exists>N::nat. y < real N * (x - 1)" |
|
1079 |
by (rule reals_Archimedean3) |
|
1080 |
hence "\<exists>N::nat. y < real N * (x - 1)" .. |
|
1081 |
then obtain N::nat where "y < real N * (x - 1)" .. |
|
1082 |
also have "\<dots> \<le> real N * (x - 1) + 1" by simp |
|
1083 |
also have "\<dots> \<le> (x - 1 + 1) ^ N" |
|
1084 |
by (rule LIMSEQ_inverse_realpow_zero_lemma, cut_tac x, simp) |
|
1085 |
also have "\<dots> = x ^ N" by simp |
|
1086 |
finally have "y < x ^ N" . |
|
1087 |
hence "\<forall>n\<ge>N. y < x ^ n" |
|
1088 |
apply clarify |
|
1089 |
apply (erule order_less_le_trans) |
|
1090 |
apply (erule power_increasing) |
|
1091 |
apply (rule order_less_imp_le [OF x]) |
|
1092 |
done |
|
1093 |
thus "\<exists>N. \<forall>n\<ge>N. y < x ^ n" .. |
|
1094 |
qed |
|
1095 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
1096 |
lemma LIMSEQ_realpow_zero: |
22628 | 1097 |
"\<lbrakk>0 \<le> (x::real); x < 1\<rbrakk> \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0" |
1098 |
proof (cases) |
|
1099 |
assume "x = 0" |
|
44313 | 1100 |
hence "(\<lambda>n. x ^ Suc n) ----> 0" by (simp add: tendsto_const) |
22628 | 1101 |
thus ?thesis by (rule LIMSEQ_imp_Suc) |
1102 |
next |
|
1103 |
assume "0 \<le> x" and "x \<noteq> 0" |
|
1104 |
hence x0: "0 < x" by simp |
|
1105 |
assume x1: "x < 1" |
|
1106 |
from x0 x1 have "1 < inverse x" |
|
36776
c137ae7673d3
remove a couple of redundant lemmas; simplify some proofs
huffman
parents:
36663
diff
changeset
|
1107 |
by (rule one_less_inverse) |
22628 | 1108 |
hence "(\<lambda>n. inverse (inverse x ^ n)) ----> 0" |
1109 |
by (rule LIMSEQ_inverse_realpow_zero) |
|
1110 |
thus ?thesis by (simp add: power_inverse) |
|
1111 |
qed |
|
15082 | 1112 |
|
20685
fee8c75e3b5d
added lemmas about LIMSEQ and norm; simplified some proofs
huffman
parents:
20682
diff
changeset
|
1113 |
lemma LIMSEQ_power_zero: |
31017 | 1114 |
fixes x :: "'a::{real_normed_algebra_1}" |
20685
fee8c75e3b5d
added lemmas about LIMSEQ and norm; simplified some proofs
huffman
parents:
20682
diff
changeset
|
1115 |
shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0" |
fee8c75e3b5d
added lemmas about LIMSEQ and norm; simplified some proofs
huffman
parents:
20682
diff
changeset
|
1116 |
apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero]) |
44313 | 1117 |
apply (simp only: tendsto_Zfun_iff, erule Zfun_le) |
22974 | 1118 |
apply (simp add: power_abs norm_power_ineq) |
20685
fee8c75e3b5d
added lemmas about LIMSEQ and norm; simplified some proofs
huffman
parents:
20682
diff
changeset
|
1119 |
done |
fee8c75e3b5d
added lemmas about LIMSEQ and norm; simplified some proofs
huffman
parents:
20682
diff
changeset
|
1120 |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
1121 |
lemma LIMSEQ_divide_realpow_zero: |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
1122 |
"1 < (x::real) ==> (%n. a / (x ^ n)) ----> 0" |
44313 | 1123 |
using tendsto_mult [OF tendsto_const [of a] |
1124 |
LIMSEQ_realpow_zero [of "inverse x"]] |
|
15082 | 1125 |
apply (auto simp add: divide_inverse power_inverse) |
1126 |
apply (simp add: inverse_eq_divide pos_divide_less_eq) |
|
1127 |
done |
|
1128 |
||
15102 | 1129 |
text{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*} |
15082 | 1130 |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
1131 |
lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < (1::real) ==> (%n. \<bar>c\<bar> ^ n) ----> 0" |
20685
fee8c75e3b5d
added lemmas about LIMSEQ and norm; simplified some proofs
huffman
parents:
20682
diff
changeset
|
1132 |
by (rule LIMSEQ_realpow_zero [OF abs_ge_zero]) |
15082 | 1133 |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
1134 |
lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) ----> 0" |
44313 | 1135 |
apply (rule tendsto_rabs_zero_cancel) |
15082 | 1136 |
apply (auto intro: LIMSEQ_rabs_realpow_zero simp add: power_abs) |
1137 |
done |
|
1138 |
||
10751 | 1139 |
end |