author | chaieb |
Fri, 30 Jan 2009 12:48:56 +0000 | |
changeset 29693 | 708dcf7dec9f |
parent 29667 | 53103fc8ffa3 |
child 29803 | c56a5571f60a |
permissions | -rw-r--r-- |
10751 | 1 |
(* Title : SEQ.thy |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 1998 University of Cambridge |
|
4 |
Description : Convergence of sequences and series |
|
15082 | 5 |
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
22608 | 6 |
Additional contributions by Jeremy Avigad and Brian Huffman |
15082 | 7 |
*) |
10751 | 8 |
|
22631
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
22629
diff
changeset
|
9 |
header {* Sequences and Convergence *} |
17439 | 10 |
|
15131 | 11 |
theory SEQ |
29197
6d4cb27ed19c
adapted HOL source structure to distribution layout
haftmann
parents:
28952
diff
changeset
|
12 |
imports RealVector RComplete |
15131 | 13 |
begin |
10751 | 14 |
|
19765 | 15 |
definition |
22608 | 16 |
Zseq :: "[nat \<Rightarrow> 'a::real_normed_vector] \<Rightarrow> bool" where |
17 |
--{*Standard definition of sequence converging to zero*} |
|
28562 | 18 |
[code del]: "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)" |
22608 | 19 |
|
20 |
definition |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
21 |
LIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21139
diff
changeset
|
22 |
("((_)/ ----> (_))" [60, 60] 60) where |
15082 | 23 |
--{*Standard definition of convergence of sequence*} |
28562 | 24 |
[code del]: "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n - L) < r))" |
10751 | 25 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21139
diff
changeset
|
26 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21139
diff
changeset
|
27 |
lim :: "(nat => 'a::real_normed_vector) => 'a" where |
15082 | 28 |
--{*Standard definition of limit using choice operator*} |
20682 | 29 |
"lim X = (THE L. X ----> L)" |
10751 | 30 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21139
diff
changeset
|
31 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21139
diff
changeset
|
32 |
convergent :: "(nat => 'a::real_normed_vector) => bool" where |
15082 | 33 |
--{*Standard definition of convergence*} |
20682 | 34 |
"convergent X = (\<exists>L. X ----> L)" |
10751 | 35 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21139
diff
changeset
|
36 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21139
diff
changeset
|
37 |
Bseq :: "(nat => 'a::real_normed_vector) => bool" where |
15082 | 38 |
--{*Standard definition for bounded sequence*} |
28562 | 39 |
[code del]: "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)" |
10751 | 40 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21139
diff
changeset
|
41 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21139
diff
changeset
|
42 |
monoseq :: "(nat=>real)=>bool" where |
15082 | 43 |
--{*Definition for monotonicity*} |
28562 | 44 |
[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))" |
10751 | 45 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21139
diff
changeset
|
46 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21139
diff
changeset
|
47 |
subseq :: "(nat => nat) => bool" where |
15082 | 48 |
--{*Definition of subsequence*} |
28562 | 49 |
[code del]: "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))" |
10751 | 50 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21139
diff
changeset
|
51 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21139
diff
changeset
|
52 |
Cauchy :: "(nat => 'a::real_normed_vector) => bool" where |
15082 | 53 |
--{*Standard definition of the Cauchy condition*} |
28562 | 54 |
[code del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)" |
10751 | 55 |
|
15082 | 56 |
|
22608 | 57 |
subsection {* Bounded Sequences *} |
58 |
||
26312 | 59 |
lemma BseqI': assumes K: "\<And>n. norm (X n) \<le> K" shows "Bseq X" |
22608 | 60 |
unfolding Bseq_def |
61 |
proof (intro exI conjI allI) |
|
62 |
show "0 < max K 1" by simp |
|
63 |
next |
|
64 |
fix n::nat |
|
65 |
have "norm (X n) \<le> K" by (rule K) |
|
66 |
thus "norm (X n) \<le> max K 1" by simp |
|
67 |
qed |
|
68 |
||
69 |
lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
|
70 |
unfolding Bseq_def by auto |
|
71 |
||
26312 | 72 |
lemma BseqI2': assumes K: "\<forall>n\<ge>N. norm (X n) \<le> K" shows "Bseq X" |
73 |
proof (rule BseqI') |
|
22608 | 74 |
let ?A = "norm ` X ` {..N}" |
75 |
have 1: "finite ?A" by simp |
|
76 |
fix n::nat |
|
77 |
show "norm (X n) \<le> max K (Max ?A)" |
|
78 |
proof (cases rule: linorder_le_cases) |
|
79 |
assume "n \<ge> N" |
|
80 |
hence "norm (X n) \<le> K" using K by simp |
|
81 |
thus "norm (X n) \<le> max K (Max ?A)" by simp |
|
82 |
next |
|
83 |
assume "n \<le> N" |
|
84 |
hence "norm (X n) \<in> ?A" by simp |
|
26757
e775accff967
thms Max_ge, Min_le: dropped superfluous premise
haftmann
parents:
26312
diff
changeset
|
85 |
with 1 have "norm (X n) \<le> Max ?A" by (rule Max_ge) |
22608 | 86 |
thus "norm (X n) \<le> max K (Max ?A)" by simp |
87 |
qed |
|
88 |
qed |
|
89 |
||
90 |
lemma Bseq_ignore_initial_segment: "Bseq X \<Longrightarrow> Bseq (\<lambda>n. X (n + k))" |
|
91 |
unfolding Bseq_def by auto |
|
92 |
||
93 |
lemma Bseq_offset: "Bseq (\<lambda>n. X (n + k)) \<Longrightarrow> Bseq X" |
|
94 |
apply (erule BseqE) |
|
26312 | 95 |
apply (rule_tac N="k" and K="K" in BseqI2') |
22608 | 96 |
apply clarify |
97 |
apply (drule_tac x="n - k" in spec, simp) |
|
98 |
done |
|
99 |
||
100 |
||
101 |
subsection {* Sequences That Converge to Zero *} |
|
102 |
||
103 |
lemma ZseqI: |
|
104 |
"(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n) < r) \<Longrightarrow> Zseq X" |
|
105 |
unfolding Zseq_def by simp |
|
106 |
||
107 |
lemma ZseqD: |
|
108 |
"\<lbrakk>Zseq X; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n) < r" |
|
109 |
unfolding Zseq_def by simp |
|
110 |
||
111 |
lemma Zseq_zero: "Zseq (\<lambda>n. 0)" |
|
112 |
unfolding Zseq_def by simp |
|
113 |
||
114 |
lemma Zseq_const_iff: "Zseq (\<lambda>n. k) = (k = 0)" |
|
115 |
unfolding Zseq_def by force |
|
116 |
||
117 |
lemma Zseq_norm_iff: "Zseq (\<lambda>n. norm (X n)) = Zseq (\<lambda>n. X n)" |
|
118 |
unfolding Zseq_def by simp |
|
119 |
||
120 |
lemma Zseq_imp_Zseq: |
|
121 |
assumes X: "Zseq X" |
|
122 |
assumes Y: "\<And>n. norm (Y n) \<le> norm (X n) * K" |
|
123 |
shows "Zseq (\<lambda>n. Y n)" |
|
124 |
proof (cases) |
|
125 |
assume K: "0 < K" |
|
126 |
show ?thesis |
|
127 |
proof (rule ZseqI) |
|
128 |
fix r::real assume "0 < r" |
|
129 |
hence "0 < r / K" |
|
130 |
using K by (rule divide_pos_pos) |
|
131 |
then obtain N where "\<forall>n\<ge>N. norm (X n) < r / K" |
|
132 |
using ZseqD [OF X] by fast |
|
133 |
hence "\<forall>n\<ge>N. norm (X n) * K < r" |
|
134 |
by (simp add: pos_less_divide_eq K) |
|
135 |
hence "\<forall>n\<ge>N. norm (Y n) < r" |
|
136 |
by (simp add: order_le_less_trans [OF Y]) |
|
137 |
thus "\<exists>N. \<forall>n\<ge>N. norm (Y n) < r" .. |
|
138 |
qed |
|
139 |
next |
|
140 |
assume "\<not> 0 < K" |
|
141 |
hence K: "K \<le> 0" by (simp only: linorder_not_less) |
|
142 |
{ |
|
143 |
fix n::nat |
|
144 |
have "norm (Y n) \<le> norm (X n) * K" by (rule Y) |
|
145 |
also have "\<dots> \<le> norm (X n) * 0" |
|
146 |
using K norm_ge_zero by (rule mult_left_mono) |
|
147 |
finally have "norm (Y n) = 0" by simp |
|
148 |
} |
|
149 |
thus ?thesis by (simp add: Zseq_zero) |
|
150 |
qed |
|
151 |
||
152 |
lemma Zseq_le: "\<lbrakk>Zseq Y; \<forall>n. norm (X n) \<le> norm (Y n)\<rbrakk> \<Longrightarrow> Zseq X" |
|
153 |
by (erule_tac K="1" in Zseq_imp_Zseq, simp) |
|
154 |
||
155 |
lemma Zseq_add: |
|
156 |
assumes X: "Zseq X" |
|
157 |
assumes Y: "Zseq Y" |
|
158 |
shows "Zseq (\<lambda>n. X n + Y n)" |
|
159 |
proof (rule ZseqI) |
|
160 |
fix r::real assume "0 < r" |
|
161 |
hence r: "0 < r / 2" by simp |
|
162 |
obtain M where M: "\<forall>n\<ge>M. norm (X n) < r/2" |
|
163 |
using ZseqD [OF X r] by fast |
|
164 |
obtain N where N: "\<forall>n\<ge>N. norm (Y n) < r/2" |
|
165 |
using ZseqD [OF Y r] by fast |
|
166 |
show "\<exists>N. \<forall>n\<ge>N. norm (X n + Y n) < r" |
|
167 |
proof (intro exI allI impI) |
|
168 |
fix n assume n: "max M N \<le> n" |
|
169 |
have "norm (X n + Y n) \<le> norm (X n) + norm (Y n)" |
|
170 |
by (rule norm_triangle_ineq) |
|
171 |
also have "\<dots> < r/2 + r/2" |
|
172 |
proof (rule add_strict_mono) |
|
173 |
from M n show "norm (X n) < r/2" by simp |
|
174 |
from N n show "norm (Y n) < r/2" by simp |
|
175 |
qed |
|
176 |
finally show "norm (X n + Y n) < r" by simp |
|
177 |
qed |
|
178 |
qed |
|
179 |
||
180 |
lemma Zseq_minus: "Zseq X \<Longrightarrow> Zseq (\<lambda>n. - X n)" |
|
181 |
unfolding Zseq_def by simp |
|
182 |
||
183 |
lemma Zseq_diff: "\<lbrakk>Zseq X; Zseq Y\<rbrakk> \<Longrightarrow> Zseq (\<lambda>n. X n - Y n)" |
|
184 |
by (simp only: diff_minus Zseq_add Zseq_minus) |
|
185 |
||
186 |
lemma (in bounded_linear) Zseq: |
|
187 |
assumes X: "Zseq X" |
|
188 |
shows "Zseq (\<lambda>n. f (X n))" |
|
189 |
proof - |
|
190 |
obtain K where "\<And>x. norm (f x) \<le> norm x * K" |
|
191 |
using bounded by fast |
|
192 |
with X show ?thesis |
|
193 |
by (rule Zseq_imp_Zseq) |
|
194 |
qed |
|
195 |
||
23127 | 196 |
lemma (in bounded_bilinear) Zseq: |
22608 | 197 |
assumes X: "Zseq X" |
198 |
assumes Y: "Zseq Y" |
|
199 |
shows "Zseq (\<lambda>n. X n ** Y n)" |
|
200 |
proof (rule ZseqI) |
|
201 |
fix r::real assume r: "0 < r" |
|
202 |
obtain K where K: "0 < K" |
|
203 |
and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K" |
|
204 |
using pos_bounded by fast |
|
205 |
from K have K': "0 < inverse K" |
|
206 |
by (rule positive_imp_inverse_positive) |
|
207 |
obtain M where M: "\<forall>n\<ge>M. norm (X n) < r" |
|
208 |
using ZseqD [OF X r] by fast |
|
209 |
obtain N where N: "\<forall>n\<ge>N. norm (Y n) < inverse K" |
|
210 |
using ZseqD [OF Y K'] by fast |
|
211 |
show "\<exists>N. \<forall>n\<ge>N. norm (X n ** Y n) < r" |
|
212 |
proof (intro exI allI impI) |
|
213 |
fix n assume n: "max M N \<le> n" |
|
214 |
have "norm (X n ** Y n) \<le> norm (X n) * norm (Y n) * K" |
|
215 |
by (rule norm_le) |
|
216 |
also have "norm (X n) * norm (Y n) * K < r * inverse K * K" |
|
217 |
proof (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero K) |
|
218 |
from M n show Xn: "norm (X n) < r" by simp |
|
219 |
from N n show Yn: "norm (Y n) < inverse K" by simp |
|
220 |
qed |
|
221 |
also from K have "r * inverse K * K = r" by simp |
|
222 |
finally show "norm (X n ** Y n) < r" . |
|
223 |
qed |
|
224 |
qed |
|
225 |
||
226 |
lemma (in bounded_bilinear) Zseq_prod_Bseq: |
|
227 |
assumes X: "Zseq X" |
|
228 |
assumes Y: "Bseq Y" |
|
229 |
shows "Zseq (\<lambda>n. X n ** Y n)" |
|
230 |
proof - |
|
231 |
obtain K where K: "0 \<le> K" |
|
232 |
and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K" |
|
233 |
using nonneg_bounded by fast |
|
234 |
obtain B where B: "0 < B" |
|
235 |
and norm_Y: "\<And>n. norm (Y n) \<le> B" |
|
236 |
using Y [unfolded Bseq_def] by fast |
|
237 |
from X show ?thesis |
|
238 |
proof (rule Zseq_imp_Zseq) |
|
239 |
fix n::nat |
|
240 |
have "norm (X n ** Y n) \<le> norm (X n) * norm (Y n) * K" |
|
241 |
by (rule norm_le) |
|
242 |
also have "\<dots> \<le> norm (X n) * B * K" |
|
243 |
by (intro mult_mono' order_refl norm_Y norm_ge_zero |
|
244 |
mult_nonneg_nonneg K) |
|
245 |
also have "\<dots> = norm (X n) * (B * K)" |
|
246 |
by (rule mult_assoc) |
|
247 |
finally show "norm (X n ** Y n) \<le> norm (X n) * (B * K)" . |
|
248 |
qed |
|
249 |
qed |
|
250 |
||
251 |
lemma (in bounded_bilinear) Bseq_prod_Zseq: |
|
252 |
assumes X: "Bseq X" |
|
253 |
assumes Y: "Zseq Y" |
|
254 |
shows "Zseq (\<lambda>n. X n ** Y n)" |
|
255 |
proof - |
|
256 |
obtain K where K: "0 \<le> K" |
|
257 |
and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K" |
|
258 |
using nonneg_bounded by fast |
|
259 |
obtain B where B: "0 < B" |
|
260 |
and norm_X: "\<And>n. norm (X n) \<le> B" |
|
261 |
using X [unfolded Bseq_def] by fast |
|
262 |
from Y show ?thesis |
|
263 |
proof (rule Zseq_imp_Zseq) |
|
264 |
fix n::nat |
|
265 |
have "norm (X n ** Y n) \<le> norm (X n) * norm (Y n) * K" |
|
266 |
by (rule norm_le) |
|
267 |
also have "\<dots> \<le> B * norm (Y n) * K" |
|
268 |
by (intro mult_mono' order_refl norm_X norm_ge_zero |
|
269 |
mult_nonneg_nonneg K) |
|
270 |
also have "\<dots> = norm (Y n) * (B * K)" |
|
271 |
by (simp only: mult_ac) |
|
272 |
finally show "norm (X n ** Y n) \<le> norm (Y n) * (B * K)" . |
|
273 |
qed |
|
274 |
qed |
|
275 |
||
23127 | 276 |
lemma (in bounded_bilinear) Zseq_left: |
22608 | 277 |
"Zseq X \<Longrightarrow> Zseq (\<lambda>n. X n ** a)" |
278 |
by (rule bounded_linear_left [THEN bounded_linear.Zseq]) |
|
279 |
||
23127 | 280 |
lemma (in bounded_bilinear) Zseq_right: |
22608 | 281 |
"Zseq X \<Longrightarrow> Zseq (\<lambda>n. a ** X n)" |
282 |
by (rule bounded_linear_right [THEN bounded_linear.Zseq]) |
|
283 |
||
23127 | 284 |
lemmas Zseq_mult = mult.Zseq |
285 |
lemmas Zseq_mult_right = mult.Zseq_right |
|
286 |
lemmas Zseq_mult_left = mult.Zseq_left |
|
22608 | 287 |
|
288 |
||
20696 | 289 |
subsection {* Limits of Sequences *} |
290 |
||
15082 | 291 |
lemma LIMSEQ_iff: |
20563 | 292 |
"(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)" |
22608 | 293 |
by (rule LIMSEQ_def) |
294 |
||
295 |
lemma LIMSEQ_Zseq_iff: "((\<lambda>n. X n) ----> L) = Zseq (\<lambda>n. X n - L)" |
|
296 |
by (simp only: LIMSEQ_def Zseq_def) |
|
15082 | 297 |
|
20751
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
298 |
lemma LIMSEQ_I: |
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
299 |
"(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r) \<Longrightarrow> X ----> L" |
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
300 |
by (simp add: LIMSEQ_def) |
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
301 |
|
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
302 |
lemma LIMSEQ_D: |
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
303 |
"\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r" |
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
304 |
by (simp add: LIMSEQ_def) |
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
305 |
|
22608 | 306 |
lemma LIMSEQ_const: "(\<lambda>n. k) ----> k" |
20696 | 307 |
by (simp add: LIMSEQ_def) |
308 |
||
22608 | 309 |
lemma LIMSEQ_const_iff: "(\<lambda>n. k) ----> l = (k = l)" |
310 |
by (simp add: LIMSEQ_Zseq_iff Zseq_const_iff) |
|
311 |
||
20696 | 312 |
lemma LIMSEQ_norm: "X ----> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----> norm a" |
313 |
apply (simp add: LIMSEQ_def, safe) |
|
314 |
apply (drule_tac x="r" in spec, safe) |
|
315 |
apply (rule_tac x="no" in exI, safe) |
|
316 |
apply (drule_tac x="n" in spec, safe) |
|
317 |
apply (erule order_le_less_trans [OF norm_triangle_ineq3]) |
|
318 |
done |
|
319 |
||
22615 | 320 |
lemma LIMSEQ_ignore_initial_segment: |
321 |
"f ----> a \<Longrightarrow> (\<lambda>n. f (n + k)) ----> a" |
|
322 |
apply (rule LIMSEQ_I) |
|
323 |
apply (drule (1) LIMSEQ_D) |
|
324 |
apply (erule exE, rename_tac N) |
|
325 |
apply (rule_tac x=N in exI) |
|
326 |
apply simp |
|
327 |
done |
|
20696 | 328 |
|
22615 | 329 |
lemma LIMSEQ_offset: |
330 |
"(\<lambda>n. f (n + k)) ----> a \<Longrightarrow> f ----> a" |
|
331 |
apply (rule LIMSEQ_I) |
|
332 |
apply (drule (1) LIMSEQ_D) |
|
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" |
341 |
by (drule_tac k="1" in LIMSEQ_ignore_initial_segment, simp) |
|
342 |
||
343 |
lemma LIMSEQ_imp_Suc: "(\<lambda>n. f (Suc n)) ----> l \<Longrightarrow> f ----> l" |
|
344 |
by (rule_tac k="1" in LIMSEQ_offset, simp) |
|
345 |
||
346 |
lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) ----> l = f ----> l" |
|
347 |
by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc) |
|
348 |
||
22608 | 349 |
lemma add_diff_add: |
350 |
fixes a b c d :: "'a::ab_group_add" |
|
351 |
shows "(a + c) - (b + d) = (a - b) + (c - d)" |
|
352 |
by simp |
|
353 |
||
354 |
lemma minus_diff_minus: |
|
355 |
fixes a b :: "'a::ab_group_add" |
|
356 |
shows "(- a) - (- b) = - (a - b)" |
|
357 |
by simp |
|
358 |
||
359 |
lemma LIMSEQ_add: "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n + Y n) ----> a + b" |
|
360 |
by (simp only: LIMSEQ_Zseq_iff add_diff_add Zseq_add) |
|
361 |
||
362 |
lemma LIMSEQ_minus: "X ----> a \<Longrightarrow> (\<lambda>n. - X n) ----> - a" |
|
363 |
by (simp only: LIMSEQ_Zseq_iff minus_diff_minus Zseq_minus) |
|
364 |
||
365 |
lemma LIMSEQ_minus_cancel: "(\<lambda>n. - X n) ----> - a \<Longrightarrow> X ----> a" |
|
366 |
by (drule LIMSEQ_minus, simp) |
|
367 |
||
368 |
lemma LIMSEQ_diff: "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n - Y n) ----> a - b" |
|
369 |
by (simp add: diff_minus LIMSEQ_add LIMSEQ_minus) |
|
370 |
||
371 |
lemma LIMSEQ_unique: "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b" |
|
372 |
by (drule (1) LIMSEQ_diff, simp add: LIMSEQ_const_iff) |
|
373 |
||
374 |
lemma (in bounded_linear) LIMSEQ: |
|
375 |
"X ----> a \<Longrightarrow> (\<lambda>n. f (X n)) ----> f a" |
|
376 |
by (simp only: LIMSEQ_Zseq_iff diff [symmetric] Zseq) |
|
377 |
||
378 |
lemma (in bounded_bilinear) LIMSEQ: |
|
379 |
"\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n ** Y n) ----> a ** b" |
|
380 |
by (simp only: LIMSEQ_Zseq_iff prod_diff_prod |
|
23127 | 381 |
Zseq_add Zseq Zseq_left Zseq_right) |
22608 | 382 |
|
383 |
lemma LIMSEQ_mult: |
|
384 |
fixes a b :: "'a::real_normed_algebra" |
|
385 |
shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b" |
|
23127 | 386 |
by (rule mult.LIMSEQ) |
22608 | 387 |
|
388 |
lemma inverse_diff_inverse: |
|
389 |
"\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk> |
|
390 |
\<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)" |
|
29667 | 391 |
by (simp add: algebra_simps) |
22608 | 392 |
|
393 |
lemma Bseq_inverse_lemma: |
|
394 |
fixes x :: "'a::real_normed_div_algebra" |
|
395 |
shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r" |
|
396 |
apply (subst nonzero_norm_inverse, clarsimp) |
|
397 |
apply (erule (1) le_imp_inverse_le) |
|
398 |
done |
|
399 |
||
400 |
lemma Bseq_inverse: |
|
401 |
fixes a :: "'a::real_normed_div_algebra" |
|
402 |
assumes X: "X ----> a" |
|
403 |
assumes a: "a \<noteq> 0" |
|
404 |
shows "Bseq (\<lambda>n. inverse (X n))" |
|
405 |
proof - |
|
406 |
from a have "0 < norm a" by simp |
|
407 |
hence "\<exists>r>0. r < norm a" by (rule dense) |
|
408 |
then obtain r where r1: "0 < r" and r2: "r < norm a" by fast |
|
409 |
obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> norm (X n - a) < r" |
|
410 |
using LIMSEQ_D [OF X r1] by fast |
|
411 |
show ?thesis |
|
26312 | 412 |
proof (rule BseqI2' [rule_format]) |
22608 | 413 |
fix n assume n: "N \<le> n" |
414 |
hence 1: "norm (X n - a) < r" by (rule N) |
|
415 |
hence 2: "X n \<noteq> 0" using r2 by auto |
|
416 |
hence "norm (inverse (X n)) = inverse (norm (X n))" |
|
417 |
by (rule nonzero_norm_inverse) |
|
418 |
also have "\<dots> \<le> inverse (norm a - r)" |
|
419 |
proof (rule le_imp_inverse_le) |
|
420 |
show "0 < norm a - r" using r2 by simp |
|
421 |
next |
|
422 |
have "norm a - norm (X n) \<le> norm (a - X n)" |
|
423 |
by (rule norm_triangle_ineq2) |
|
424 |
also have "\<dots> = norm (X n - a)" |
|
425 |
by (rule norm_minus_commute) |
|
426 |
also have "\<dots> < r" using 1 . |
|
427 |
finally show "norm a - r \<le> norm (X n)" by simp |
|
428 |
qed |
|
429 |
finally show "norm (inverse (X n)) \<le> inverse (norm a - r)" . |
|
430 |
qed |
|
431 |
qed |
|
432 |
||
433 |
lemma LIMSEQ_inverse_lemma: |
|
434 |
fixes a :: "'a::real_normed_div_algebra" |
|
435 |
shows "\<lbrakk>X ----> a; a \<noteq> 0; \<forall>n. X n \<noteq> 0\<rbrakk> |
|
436 |
\<Longrightarrow> (\<lambda>n. inverse (X n)) ----> inverse a" |
|
437 |
apply (subst LIMSEQ_Zseq_iff) |
|
438 |
apply (simp add: inverse_diff_inverse nonzero_imp_inverse_nonzero) |
|
439 |
apply (rule Zseq_minus) |
|
440 |
apply (rule Zseq_mult_left) |
|
23127 | 441 |
apply (rule mult.Bseq_prod_Zseq) |
22608 | 442 |
apply (erule (1) Bseq_inverse) |
443 |
apply (simp add: LIMSEQ_Zseq_iff) |
|
444 |
done |
|
445 |
||
446 |
lemma LIMSEQ_inverse: |
|
447 |
fixes a :: "'a::real_normed_div_algebra" |
|
448 |
assumes X: "X ----> a" |
|
449 |
assumes a: "a \<noteq> 0" |
|
450 |
shows "(\<lambda>n. inverse (X n)) ----> inverse a" |
|
451 |
proof - |
|
452 |
from a have "0 < norm a" by simp |
|
453 |
then obtain k where "\<forall>n\<ge>k. norm (X n - a) < norm a" |
|
454 |
using LIMSEQ_D [OF X] by fast |
|
455 |
hence "\<forall>n\<ge>k. X n \<noteq> 0" by auto |
|
456 |
hence k: "\<forall>n. X (n + k) \<noteq> 0" by simp |
|
457 |
||
458 |
from X have "(\<lambda>n. X (n + k)) ----> a" |
|
459 |
by (rule LIMSEQ_ignore_initial_segment) |
|
460 |
hence "(\<lambda>n. inverse (X (n + k))) ----> inverse a" |
|
461 |
using a k by (rule LIMSEQ_inverse_lemma) |
|
462 |
thus "(\<lambda>n. inverse (X n)) ----> inverse a" |
|
463 |
by (rule LIMSEQ_offset) |
|
464 |
qed |
|
465 |
||
466 |
lemma LIMSEQ_divide: |
|
467 |
fixes a b :: "'a::real_normed_field" |
|
468 |
shows "\<lbrakk>X ----> a; Y ----> b; b \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>n. X n / Y n) ----> a / b" |
|
469 |
by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse) |
|
470 |
||
471 |
lemma LIMSEQ_pow: |
|
472 |
fixes a :: "'a::{real_normed_algebra,recpower}" |
|
473 |
shows "X ----> a \<Longrightarrow> (\<lambda>n. (X n) ^ m) ----> a ^ m" |
|
474 |
by (induct m) (simp_all add: power_Suc LIMSEQ_const LIMSEQ_mult) |
|
475 |
||
476 |
lemma LIMSEQ_setsum: |
|
477 |
assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n" |
|
478 |
shows "(\<lambda>m. \<Sum>n\<in>S. X n m) ----> (\<Sum>n\<in>S. L n)" |
|
479 |
proof (cases "finite S") |
|
480 |
case True |
|
481 |
thus ?thesis using n |
|
482 |
proof (induct) |
|
483 |
case empty |
|
484 |
show ?case |
|
485 |
by (simp add: LIMSEQ_const) |
|
486 |
next |
|
487 |
case insert |
|
488 |
thus ?case |
|
489 |
by (simp add: LIMSEQ_add) |
|
490 |
qed |
|
491 |
next |
|
492 |
case False |
|
493 |
thus ?thesis |
|
494 |
by (simp add: LIMSEQ_const) |
|
495 |
qed |
|
496 |
||
497 |
lemma LIMSEQ_setprod: |
|
498 |
fixes L :: "'a \<Rightarrow> 'b::{real_normed_algebra,comm_ring_1}" |
|
499 |
assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n" |
|
500 |
shows "(\<lambda>m. \<Prod>n\<in>S. X n m) ----> (\<Prod>n\<in>S. L n)" |
|
501 |
proof (cases "finite S") |
|
502 |
case True |
|
503 |
thus ?thesis using n |
|
504 |
proof (induct) |
|
505 |
case empty |
|
506 |
show ?case |
|
507 |
by (simp add: LIMSEQ_const) |
|
508 |
next |
|
509 |
case insert |
|
510 |
thus ?case |
|
511 |
by (simp add: LIMSEQ_mult) |
|
512 |
qed |
|
513 |
next |
|
514 |
case False |
|
515 |
thus ?thesis |
|
516 |
by (simp add: setprod_def LIMSEQ_const) |
|
517 |
qed |
|
518 |
||
22614 | 519 |
lemma LIMSEQ_add_const: "f ----> a ==> (%n.(f n + b)) ----> a + b" |
520 |
by (simp add: LIMSEQ_add LIMSEQ_const) |
|
521 |
||
522 |
(* FIXME: delete *) |
|
523 |
lemma LIMSEQ_add_minus: |
|
524 |
"[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b" |
|
525 |
by (simp only: LIMSEQ_add LIMSEQ_minus) |
|
526 |
||
527 |
lemma LIMSEQ_diff_const: "f ----> a ==> (%n.(f n - b)) ----> a - b" |
|
528 |
by (simp add: LIMSEQ_diff LIMSEQ_const) |
|
529 |
||
530 |
lemma LIMSEQ_diff_approach_zero: |
|
531 |
"g ----> L ==> (%x. f x - g x) ----> 0 ==> |
|
532 |
f ----> L" |
|
533 |
apply (drule LIMSEQ_add) |
|
534 |
apply assumption |
|
535 |
apply simp |
|
536 |
done |
|
537 |
||
538 |
lemma LIMSEQ_diff_approach_zero2: |
|
539 |
"f ----> L ==> (%x. f x - g x) ----> 0 ==> |
|
540 |
g ----> L"; |
|
541 |
apply (drule LIMSEQ_diff) |
|
542 |
apply assumption |
|
543 |
apply simp |
|
544 |
done |
|
545 |
||
546 |
text{*A sequence tends to zero iff its abs does*} |
|
547 |
lemma LIMSEQ_norm_zero: "((\<lambda>n. norm (X n)) ----> 0) = (X ----> 0)" |
|
548 |
by (simp add: LIMSEQ_def) |
|
549 |
||
550 |
lemma LIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----> 0) = (f ----> (0::real))" |
|
551 |
by (simp add: LIMSEQ_def) |
|
552 |
||
553 |
lemma LIMSEQ_imp_rabs: "f ----> (l::real) ==> (%n. \<bar>f n\<bar>) ----> \<bar>l\<bar>" |
|
554 |
by (drule LIMSEQ_norm, simp) |
|
555 |
||
556 |
text{*An unbounded sequence's inverse tends to 0*} |
|
557 |
||
558 |
lemma LIMSEQ_inverse_zero: |
|
22974 | 559 |
"\<forall>r::real. \<exists>N. \<forall>n\<ge>N. r < X n \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> 0" |
560 |
apply (rule LIMSEQ_I) |
|
561 |
apply (drule_tac x="inverse r" in spec, safe) |
|
562 |
apply (rule_tac x="N" in exI, safe) |
|
563 |
apply (drule_tac x="n" in spec, safe) |
|
22614 | 564 |
apply (frule positive_imp_inverse_positive) |
22974 | 565 |
apply (frule (1) less_imp_inverse_less) |
566 |
apply (subgoal_tac "0 < X n", simp) |
|
567 |
apply (erule (1) order_less_trans) |
|
22614 | 568 |
done |
569 |
||
570 |
text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*} |
|
571 |
||
572 |
lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0" |
|
573 |
apply (rule LIMSEQ_inverse_zero, safe) |
|
22974 | 574 |
apply (cut_tac x = r in reals_Archimedean2) |
22614 | 575 |
apply (safe, rule_tac x = n in exI) |
576 |
apply (auto simp add: real_of_nat_Suc) |
|
577 |
done |
|
578 |
||
579 |
text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to |
|
580 |
infinity is now easily proved*} |
|
581 |
||
582 |
lemma LIMSEQ_inverse_real_of_nat_add: |
|
583 |
"(%n. r + inverse(real(Suc n))) ----> r" |
|
584 |
by (cut_tac LIMSEQ_add [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto) |
|
585 |
||
586 |
lemma LIMSEQ_inverse_real_of_nat_add_minus: |
|
587 |
"(%n. r + -inverse(real(Suc n))) ----> r" |
|
588 |
by (cut_tac LIMSEQ_add_minus [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto) |
|
589 |
||
590 |
lemma LIMSEQ_inverse_real_of_nat_add_minus_mult: |
|
591 |
"(%n. r*( 1 + -inverse(real(Suc n)))) ----> r" |
|
592 |
by (cut_tac b=1 in |
|
593 |
LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat_add_minus], auto) |
|
594 |
||
22615 | 595 |
lemma LIMSEQ_le_const: |
596 |
"\<lbrakk>X ----> (x::real); \<exists>N. \<forall>n\<ge>N. a \<le> X n\<rbrakk> \<Longrightarrow> a \<le> x" |
|
597 |
apply (rule ccontr, simp only: linorder_not_le) |
|
598 |
apply (drule_tac r="a - x" in LIMSEQ_D, simp) |
|
599 |
apply clarsimp |
|
600 |
apply (drule_tac x="max N no" in spec, drule mp, rule le_maxI1) |
|
601 |
apply (drule_tac x="max N no" in spec, drule mp, rule le_maxI2) |
|
602 |
apply simp |
|
603 |
done |
|
604 |
||
605 |
lemma LIMSEQ_le_const2: |
|
606 |
"\<lbrakk>X ----> (x::real); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a" |
|
607 |
apply (subgoal_tac "- a \<le> - x", simp) |
|
608 |
apply (rule LIMSEQ_le_const) |
|
609 |
apply (erule LIMSEQ_minus) |
|
610 |
apply simp |
|
611 |
done |
|
612 |
||
613 |
lemma LIMSEQ_le: |
|
614 |
"\<lbrakk>X ----> x; Y ----> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::real)" |
|
615 |
apply (subgoal_tac "0 \<le> y - x", simp) |
|
616 |
apply (rule LIMSEQ_le_const) |
|
617 |
apply (erule (1) LIMSEQ_diff) |
|
618 |
apply (simp add: le_diff_eq) |
|
619 |
done |
|
620 |
||
15082 | 621 |
|
20696 | 622 |
subsection {* Convergence *} |
15082 | 623 |
|
624 |
lemma limI: "X ----> L ==> lim X = L" |
|
625 |
apply (simp add: lim_def) |
|
626 |
apply (blast intro: LIMSEQ_unique) |
|
627 |
done |
|
628 |
||
629 |
lemma convergentD: "convergent X ==> \<exists>L. (X ----> L)" |
|
630 |
by (simp add: convergent_def) |
|
631 |
||
632 |
lemma convergentI: "(X ----> L) ==> convergent X" |
|
633 |
by (auto simp add: convergent_def) |
|
634 |
||
635 |
lemma convergent_LIMSEQ_iff: "convergent X = (X ----> lim X)" |
|
20682 | 636 |
by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def) |
15082 | 637 |
|
20696 | 638 |
lemma convergent_minus_iff: "(convergent X) = (convergent (%n. -(X n)))" |
639 |
apply (simp add: convergent_def) |
|
640 |
apply (auto dest: LIMSEQ_minus) |
|
641 |
apply (drule LIMSEQ_minus, auto) |
|
642 |
done |
|
643 |
||
644 |
||
645 |
subsection {* Bounded Monotonic Sequences *} |
|
646 |
||
15082 | 647 |
text{*Subsequence (alternative definition, (e.g. Hoskins)*} |
648 |
||
649 |
lemma subseq_Suc_iff: "subseq f = (\<forall>n. (f n) < (f (Suc n)))" |
|
650 |
apply (simp add: subseq_def) |
|
651 |
apply (auto dest!: less_imp_Suc_add) |
|
652 |
apply (induct_tac k) |
|
653 |
apply (auto intro: less_trans) |
|
654 |
done |
|
655 |
||
656 |
lemma monoseq_Suc: |
|
657 |
"monoseq X = ((\<forall>n. X n \<le> X (Suc n)) |
|
658 |
| (\<forall>n. X (Suc n) \<le> X n))" |
|
659 |
apply (simp add: monoseq_def) |
|
660 |
apply (auto dest!: le_imp_less_or_eq) |
|
661 |
apply (auto intro!: lessI [THEN less_imp_le] dest!: less_imp_Suc_add) |
|
662 |
apply (induct_tac "ka") |
|
663 |
apply (auto intro: order_trans) |
|
18585 | 664 |
apply (erule contrapos_np) |
15082 | 665 |
apply (induct_tac "k") |
666 |
apply (auto intro: order_trans) |
|
667 |
done |
|
668 |
||
15360 | 669 |
lemma monoI1: "\<forall>m. \<forall> n \<ge> m. X m \<le> X n ==> monoseq X" |
15082 | 670 |
by (simp add: monoseq_def) |
671 |
||
15360 | 672 |
lemma monoI2: "\<forall>m. \<forall> n \<ge> m. X n \<le> X m ==> monoseq X" |
15082 | 673 |
by (simp add: monoseq_def) |
674 |
||
675 |
lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X" |
|
676 |
by (simp add: monoseq_Suc) |
|
677 |
||
678 |
lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X" |
|
679 |
by (simp add: monoseq_Suc) |
|
680 |
||
20696 | 681 |
text{*Bounded Sequence*} |
15082 | 682 |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
683 |
lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)" |
15082 | 684 |
by (simp add: Bseq_def) |
685 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
686 |
lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X" |
15082 | 687 |
by (auto simp add: Bseq_def) |
688 |
||
689 |
lemma lemma_NBseq_def: |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
690 |
"(\<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
|
691 |
(\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))" |
15082 | 692 |
apply auto |
693 |
prefer 2 apply force |
|
694 |
apply (cut_tac x = K in reals_Archimedean2, clarify) |
|
695 |
apply (rule_tac x = n in exI, clarify) |
|
696 |
apply (drule_tac x = na in spec) |
|
697 |
apply (auto simp add: real_of_nat_Suc) |
|
698 |
done |
|
699 |
||
700 |
text{* alternative definition for Bseq *} |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
701 |
lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))" |
15082 | 702 |
apply (simp add: Bseq_def) |
703 |
apply (simp (no_asm) add: lemma_NBseq_def) |
|
704 |
done |
|
705 |
||
706 |
lemma lemma_NBseq_def2: |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
707 |
"(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))" |
15082 | 708 |
apply (subst lemma_NBseq_def, auto) |
709 |
apply (rule_tac x = "Suc N" in exI) |
|
710 |
apply (rule_tac [2] x = N in exI) |
|
711 |
apply (auto simp add: real_of_nat_Suc) |
|
712 |
prefer 2 apply (blast intro: order_less_imp_le) |
|
713 |
apply (drule_tac x = n in spec, simp) |
|
714 |
done |
|
715 |
||
716 |
(* yet another definition for Bseq *) |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
717 |
lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))" |
15082 | 718 |
by (simp add: Bseq_def lemma_NBseq_def2) |
719 |
||
20696 | 720 |
subsubsection{*Upper Bounds and Lubs of Bounded Sequences*} |
15082 | 721 |
|
722 |
lemma Bseq_isUb: |
|
723 |
"!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U" |
|
22998 | 724 |
by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff) |
15082 | 725 |
|
726 |
||
727 |
text{* Use completeness of reals (supremum property) |
|
728 |
to show that any bounded sequence has a least upper bound*} |
|
729 |
||
730 |
lemma Bseq_isLub: |
|
731 |
"!!(X::nat=>real). Bseq X ==> |
|
732 |
\<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U" |
|
733 |
by (blast intro: reals_complete Bseq_isUb) |
|
734 |
||
20696 | 735 |
subsubsection{*A Bounded and Monotonic Sequence Converges*} |
15082 | 736 |
|
737 |
lemma lemma_converg1: |
|
15360 | 738 |
"!!(X::nat=>real). [| \<forall>m. \<forall> n \<ge> m. X m \<le> X n; |
15082 | 739 |
isLub (UNIV::real set) {x. \<exists>n. X n = x} (X ma) |
15360 | 740 |
|] ==> \<forall>n \<ge> ma. X n = X ma" |
15082 | 741 |
apply safe |
742 |
apply (drule_tac y = "X n" in isLubD2) |
|
743 |
apply (blast dest: order_antisym)+ |
|
744 |
done |
|
745 |
||
746 |
text{* The best of both worlds: Easier to prove this result as a standard |
|
747 |
theorem and then use equivalence to "transfer" it into the |
|
748 |
equivalent nonstandard form if needed!*} |
|
749 |
||
750 |
lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)" |
|
751 |
apply (simp add: LIMSEQ_def) |
|
752 |
apply (rule_tac x = "X m" in exI, safe) |
|
753 |
apply (rule_tac x = m in exI, safe) |
|
754 |
apply (drule spec, erule impE, auto) |
|
755 |
done |
|
756 |
||
757 |
lemma lemma_converg2: |
|
758 |
"!!(X::nat=>real). |
|
759 |
[| \<forall>m. X m ~= U; isLub UNIV {x. \<exists>n. X n = x} U |] ==> \<forall>m. X m < U" |
|
760 |
apply safe |
|
761 |
apply (drule_tac y = "X m" in isLubD2) |
|
762 |
apply (auto dest!: order_le_imp_less_or_eq) |
|
763 |
done |
|
764 |
||
765 |
lemma lemma_converg3: "!!(X ::nat=>real). \<forall>m. X m \<le> U ==> isUb UNIV {x. \<exists>n. X n = x} U" |
|
766 |
by (rule setleI [THEN isUbI], auto) |
|
767 |
||
768 |
text{* FIXME: @{term "U - T < U"} is redundant *} |
|
769 |
lemma lemma_converg4: "!!(X::nat=> real). |
|
770 |
[| \<forall>m. X m ~= U; |
|
771 |
isLub UNIV {x. \<exists>n. X n = x} U; |
|
772 |
0 < T; |
|
773 |
U + - T < U |
|
774 |
|] ==> \<exists>m. U + -T < X m & X m < U" |
|
775 |
apply (drule lemma_converg2, assumption) |
|
776 |
apply (rule ccontr, simp) |
|
777 |
apply (simp add: linorder_not_less) |
|
778 |
apply (drule lemma_converg3) |
|
779 |
apply (drule isLub_le_isUb, assumption) |
|
780 |
apply (auto dest: order_less_le_trans) |
|
781 |
done |
|
782 |
||
783 |
text{*A standard proof of the theorem for monotone increasing sequence*} |
|
784 |
||
785 |
lemma Bseq_mono_convergent: |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
786 |
"[| Bseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> convergent (X::nat=>real)" |
15082 | 787 |
apply (simp add: convergent_def) |
788 |
apply (frule Bseq_isLub, safe) |
|
789 |
apply (case_tac "\<exists>m. X m = U", auto) |
|
790 |
apply (blast dest: lemma_converg1 Bmonoseq_LIMSEQ) |
|
791 |
(* second case *) |
|
792 |
apply (rule_tac x = U in exI) |
|
793 |
apply (subst LIMSEQ_iff, safe) |
|
794 |
apply (frule lemma_converg2, assumption) |
|
795 |
apply (drule lemma_converg4, auto) |
|
796 |
apply (rule_tac x = m in exI, safe) |
|
797 |
apply (subgoal_tac "X m \<le> X n") |
|
798 |
prefer 2 apply blast |
|
799 |
apply (drule_tac x=n and P="%m. X m < U" in spec, arith) |
|
800 |
done |
|
801 |
||
802 |
lemma Bseq_minus_iff: "Bseq (%n. -(X n)) = Bseq X" |
|
803 |
by (simp add: Bseq_def) |
|
804 |
||
805 |
text{*Main monotonicity theorem*} |
|
806 |
lemma Bseq_monoseq_convergent: "[| Bseq X; monoseq X |] ==> convergent X" |
|
807 |
apply (simp add: monoseq_def, safe) |
|
808 |
apply (rule_tac [2] convergent_minus_iff [THEN ssubst]) |
|
809 |
apply (drule_tac [2] Bseq_minus_iff [THEN ssubst]) |
|
810 |
apply (auto intro!: Bseq_mono_convergent) |
|
811 |
done |
|
812 |
||
20696 | 813 |
subsubsection{*A Few More Equivalence Theorems for Boundedness*} |
15082 | 814 |
|
815 |
text{*alternative formulation for boundedness*} |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
816 |
lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)" |
15082 | 817 |
apply (unfold Bseq_def, safe) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
818 |
apply (rule_tac [2] x = "k + norm x" in exI) |
15360 | 819 |
apply (rule_tac x = K in exI, simp) |
15221 | 820 |
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
|
821 |
apply (erule order_less_le_trans, simp) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
822 |
apply (drule_tac x=n in spec, fold diff_def) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
823 |
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
|
824 |
apply simp |
15082 | 825 |
done |
826 |
||
827 |
text{*alternative formulation for boundedness*} |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
828 |
lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)" |
15082 | 829 |
apply safe |
830 |
apply (simp add: Bseq_def, safe) |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
831 |
apply (rule_tac x = "K + norm (X N)" in exI) |
15082 | 832 |
apply auto |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
833 |
apply (erule order_less_le_trans, simp) |
15082 | 834 |
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
|
835 |
apply (drule_tac x = n in spec) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
836 |
apply (rule order_trans [OF norm_triangle_ineq], simp) |
15082 | 837 |
apply (auto simp add: Bseq_iff2) |
838 |
done |
|
839 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
840 |
lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f" |
15082 | 841 |
apply (simp add: Bseq_def) |
15221 | 842 |
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
|
843 |
apply (drule_tac x = n in spec, arith) |
15082 | 844 |
done |
845 |
||
846 |
||
20696 | 847 |
subsection {* Cauchy Sequences *} |
15082 | 848 |
|
20751
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
849 |
lemma CauchyI: |
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
850 |
"(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e) \<Longrightarrow> Cauchy X" |
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
851 |
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
|
852 |
|
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
853 |
lemma CauchyD: |
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
854 |
"\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e" |
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
855 |
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
|
856 |
|
20696 | 857 |
subsubsection {* Cauchy Sequences are Bounded *} |
858 |
||
15082 | 859 |
text{*A Cauchy sequence is bounded -- this is the standard |
860 |
proof mechanization rather than the nonstandard proof*} |
|
861 |
||
20563 | 862 |
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
|
863 |
==> \<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
|
864 |
apply (clarify, drule spec, drule (1) mp) |
20563 | 865 |
apply (simp only: norm_minus_commute) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
866 |
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
|
867 |
apply simp |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
868 |
done |
15082 | 869 |
|
870 |
lemma Cauchy_Bseq: "Cauchy X ==> Bseq X" |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
871 |
apply (simp add: Cauchy_def) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
872 |
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
|
873 |
apply (drule_tac x="M" in spec, simp) |
15082 | 874 |
apply (drule lemmaCauchy) |
22608 | 875 |
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
|
876 |
apply (simp add: Bseq_def) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
877 |
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
|
878 |
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
|
879 |
apply (simp add: order_less_imp_le) |
15082 | 880 |
done |
881 |
||
20696 | 882 |
subsubsection {* Cauchy Sequences are Convergent *} |
15082 | 883 |
|
20830
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
884 |
axclass banach \<subseteq> real_normed_vector |
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
885 |
Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X" |
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
886 |
|
22629 | 887 |
theorem LIMSEQ_imp_Cauchy: |
888 |
assumes X: "X ----> a" shows "Cauchy X" |
|
889 |
proof (rule CauchyI) |
|
890 |
fix e::real assume "0 < e" |
|
891 |
hence "0 < e/2" by simp |
|
892 |
with X have "\<exists>N. \<forall>n\<ge>N. norm (X n - a) < e/2" by (rule LIMSEQ_D) |
|
893 |
then obtain N where N: "\<forall>n\<ge>N. norm (X n - a) < e/2" .. |
|
894 |
show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. norm (X m - X n) < e" |
|
895 |
proof (intro exI allI impI) |
|
896 |
fix m assume "N \<le> m" |
|
897 |
hence m: "norm (X m - a) < e/2" using N by fast |
|
898 |
fix n assume "N \<le> n" |
|
899 |
hence n: "norm (X n - a) < e/2" using N by fast |
|
900 |
have "norm (X m - X n) = norm ((X m - a) - (X n - a))" by simp |
|
901 |
also have "\<dots> \<le> norm (X m - a) + norm (X n - a)" |
|
902 |
by (rule norm_triangle_ineq4) |
|
23482 | 903 |
also from m n have "\<dots> < e" by(simp add:field_simps) |
22629 | 904 |
finally show "norm (X m - X n) < e" . |
905 |
qed |
|
906 |
qed |
|
907 |
||
20691 | 908 |
lemma convergent_Cauchy: "convergent X \<Longrightarrow> Cauchy X" |
22629 | 909 |
unfolding convergent_def |
910 |
by (erule exE, erule LIMSEQ_imp_Cauchy) |
|
20691 | 911 |
|
22629 | 912 |
text {* |
913 |
Proof that Cauchy sequences converge based on the one from |
|
914 |
http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html |
|
915 |
*} |
|
916 |
||
917 |
text {* |
|
918 |
If sequence @{term "X"} is Cauchy, then its limit is the lub of |
|
919 |
@{term "{r::real. \<exists>N. \<forall>n\<ge>N. r < X n}"} |
|
920 |
*} |
|
921 |
||
922 |
lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u" |
|
923 |
by (simp add: isUbI setleI) |
|
924 |
||
925 |
lemma real_abs_diff_less_iff: |
|
926 |
"(\<bar>x - a\<bar> < (r::real)) = (a - r < x \<and> x < a + r)" |
|
927 |
by auto |
|
928 |
||
27681 | 929 |
locale real_Cauchy = |
22629 | 930 |
fixes X :: "nat \<Rightarrow> real" |
931 |
assumes X: "Cauchy X" |
|
932 |
fixes S :: "real set" |
|
933 |
defines S_def: "S \<equiv> {x::real. \<exists>N. \<forall>n\<ge>N. x < X n}" |
|
934 |
||
27681 | 935 |
lemma real_CauchyI: |
936 |
assumes "Cauchy X" |
|
937 |
shows "real_Cauchy X" |
|
28823 | 938 |
proof qed (fact assms) |
27681 | 939 |
|
22629 | 940 |
lemma (in real_Cauchy) mem_S: "\<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S" |
941 |
by (unfold S_def, auto) |
|
942 |
||
943 |
lemma (in real_Cauchy) bound_isUb: |
|
944 |
assumes N: "\<forall>n\<ge>N. X n < x" |
|
945 |
shows "isUb UNIV S x" |
|
946 |
proof (rule isUb_UNIV_I) |
|
947 |
fix y::real assume "y \<in> S" |
|
948 |
hence "\<exists>M. \<forall>n\<ge>M. y < X n" |
|
949 |
by (simp add: S_def) |
|
950 |
then obtain M where "\<forall>n\<ge>M. y < X n" .. |
|
951 |
hence "y < X (max M N)" by simp |
|
952 |
also have "\<dots> < x" using N by simp |
|
953 |
finally show "y \<le> x" |
|
954 |
by (rule order_less_imp_le) |
|
955 |
qed |
|
956 |
||
957 |
lemma (in real_Cauchy) isLub_ex: "\<exists>u. isLub UNIV S u" |
|
958 |
proof (rule reals_complete) |
|
959 |
obtain N where "\<forall>m\<ge>N. \<forall>n\<ge>N. norm (X m - X n) < 1" |
|
960 |
using CauchyD [OF X zero_less_one] by fast |
|
961 |
hence N: "\<forall>n\<ge>N. norm (X n - X N) < 1" by simp |
|
962 |
show "\<exists>x. x \<in> S" |
|
963 |
proof |
|
964 |
from N have "\<forall>n\<ge>N. X N - 1 < X n" |
|
965 |
by (simp add: real_abs_diff_less_iff) |
|
966 |
thus "X N - 1 \<in> S" by (rule mem_S) |
|
967 |
qed |
|
968 |
show "\<exists>u. isUb UNIV S u" |
|
969 |
proof |
|
970 |
from N have "\<forall>n\<ge>N. X n < X N + 1" |
|
971 |
by (simp add: real_abs_diff_less_iff) |
|
972 |
thus "isUb UNIV S (X N + 1)" |
|
973 |
by (rule bound_isUb) |
|
974 |
qed |
|
975 |
qed |
|
976 |
||
977 |
lemma (in real_Cauchy) isLub_imp_LIMSEQ: |
|
978 |
assumes x: "isLub UNIV S x" |
|
979 |
shows "X ----> x" |
|
980 |
proof (rule LIMSEQ_I) |
|
981 |
fix r::real assume "0 < r" |
|
982 |
hence r: "0 < r/2" by simp |
|
983 |
obtain N where "\<forall>n\<ge>N. \<forall>m\<ge>N. norm (X n - X m) < r/2" |
|
984 |
using CauchyD [OF X r] by fast |
|
985 |
hence "\<forall>n\<ge>N. norm (X n - X N) < r/2" by simp |
|
986 |
hence N: "\<forall>n\<ge>N. X N - r/2 < X n \<and> X n < X N + r/2" |
|
987 |
by (simp only: real_norm_def real_abs_diff_less_iff) |
|
988 |
||
989 |
from N have "\<forall>n\<ge>N. X N - r/2 < X n" by fast |
|
990 |
hence "X N - r/2 \<in> S" by (rule mem_S) |
|
23482 | 991 |
hence 1: "X N - r/2 \<le> x" using x isLub_isUb isUbD by fast |
22629 | 992 |
|
993 |
from N have "\<forall>n\<ge>N. X n < X N + r/2" by fast |
|
994 |
hence "isUb UNIV S (X N + r/2)" by (rule bound_isUb) |
|
23482 | 995 |
hence 2: "x \<le> X N + r/2" using x isLub_le_isUb by fast |
22629 | 996 |
|
997 |
show "\<exists>N. \<forall>n\<ge>N. norm (X n - x) < r" |
|
998 |
proof (intro exI allI impI) |
|
999 |
fix n assume n: "N \<le> n" |
|
23482 | 1000 |
from N n have "X n < X N + r/2" and "X N - r/2 < X n" by simp+ |
1001 |
thus "norm (X n - x) < r" using 1 2 |
|
22629 | 1002 |
by (simp add: real_abs_diff_less_iff) |
1003 |
qed |
|
1004 |
qed |
|
1005 |
||
1006 |
lemma (in real_Cauchy) LIMSEQ_ex: "\<exists>x. X ----> x" |
|
1007 |
proof - |
|
1008 |
obtain x where "isLub UNIV S x" |
|
1009 |
using isLub_ex by fast |
|
1010 |
hence "X ----> x" |
|
1011 |
by (rule isLub_imp_LIMSEQ) |
|
1012 |
thus ?thesis .. |
|
1013 |
qed |
|
1014 |
||
20830
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
1015 |
lemma real_Cauchy_convergent: |
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
1016 |
fixes X :: "nat \<Rightarrow> real" |
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
1017 |
shows "Cauchy X \<Longrightarrow> convergent X" |
27681 | 1018 |
unfolding convergent_def |
1019 |
by (rule real_Cauchy.LIMSEQ_ex) |
|
1020 |
(rule real_CauchyI) |
|
20830
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
1021 |
|
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
1022 |
instance real :: banach |
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
1023 |
by intro_classes (rule real_Cauchy_convergent) |
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
1024 |
|
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
1025 |
lemma Cauchy_convergent_iff: |
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
1026 |
fixes X :: "nat \<Rightarrow> 'a::banach" |
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
1027 |
shows "Cauchy X = convergent X" |
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
1028 |
by (fast intro: Cauchy_convergent convergent_Cauchy) |
15082 | 1029 |
|
1030 |
||
20696 | 1031 |
subsection {* Power Sequences *} |
15082 | 1032 |
|
1033 |
text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term |
|
1034 |
"x<1"}. Proof will use (NS) Cauchy equivalence for convergence and |
|
1035 |
also fact that bounded and monotonic sequence converges.*} |
|
1036 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
1037 |
lemma Bseq_realpow: "[| 0 \<le> (x::real); x \<le> 1 |] ==> Bseq (%n. x ^ n)" |
15082 | 1038 |
apply (simp add: Bseq_def) |
1039 |
apply (rule_tac x = 1 in exI) |
|
1040 |
apply (simp add: power_abs) |
|
22974 | 1041 |
apply (auto dest: power_mono) |
15082 | 1042 |
done |
1043 |
||
1044 |
lemma monoseq_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> monoseq (%n. x ^ n)" |
|
1045 |
apply (clarify intro!: mono_SucI2) |
|
1046 |
apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto) |
|
1047 |
done |
|
1048 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
1049 |
lemma convergent_realpow: |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
1050 |
"[| 0 \<le> (x::real); x \<le> 1 |] ==> convergent (%n. x ^ n)" |
15082 | 1051 |
by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow) |
1052 |
||
22628 | 1053 |
lemma LIMSEQ_inverse_realpow_zero_lemma: |
1054 |
fixes x :: real |
|
1055 |
assumes x: "0 \<le> x" |
|
1056 |
shows "real n * x + 1 \<le> (x + 1) ^ n" |
|
1057 |
apply (induct n) |
|
1058 |
apply simp |
|
1059 |
apply simp |
|
1060 |
apply (rule order_trans) |
|
1061 |
prefer 2 |
|
1062 |
apply (erule mult_left_mono) |
|
1063 |
apply (rule add_increasing [OF x], simp) |
|
1064 |
apply (simp add: real_of_nat_Suc) |
|
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23127
diff
changeset
|
1065 |
apply (simp add: ring_distribs) |
22628 | 1066 |
apply (simp add: mult_nonneg_nonneg x) |
1067 |
done |
|
1068 |
||
1069 |
lemma LIMSEQ_inverse_realpow_zero: |
|
1070 |
"1 < (x::real) \<Longrightarrow> (\<lambda>n. inverse (x ^ n)) ----> 0" |
|
1071 |
proof (rule LIMSEQ_inverse_zero [rule_format]) |
|
1072 |
fix y :: real |
|
1073 |
assume x: "1 < x" |
|
1074 |
hence "0 < x - 1" by simp |
|
1075 |
hence "\<forall>y. \<exists>N::nat. y < real N * (x - 1)" |
|
1076 |
by (rule reals_Archimedean3) |
|
1077 |
hence "\<exists>N::nat. y < real N * (x - 1)" .. |
|
1078 |
then obtain N::nat where "y < real N * (x - 1)" .. |
|
1079 |
also have "\<dots> \<le> real N * (x - 1) + 1" by simp |
|
1080 |
also have "\<dots> \<le> (x - 1 + 1) ^ N" |
|
1081 |
by (rule LIMSEQ_inverse_realpow_zero_lemma, cut_tac x, simp) |
|
1082 |
also have "\<dots> = x ^ N" by simp |
|
1083 |
finally have "y < x ^ N" . |
|
1084 |
hence "\<forall>n\<ge>N. y < x ^ n" |
|
1085 |
apply clarify |
|
1086 |
apply (erule order_less_le_trans) |
|
1087 |
apply (erule power_increasing) |
|
1088 |
apply (rule order_less_imp_le [OF x]) |
|
1089 |
done |
|
1090 |
thus "\<exists>N. \<forall>n\<ge>N. y < x ^ n" .. |
|
1091 |
qed |
|
1092 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
1093 |
lemma LIMSEQ_realpow_zero: |
22628 | 1094 |
"\<lbrakk>0 \<le> (x::real); x < 1\<rbrakk> \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0" |
1095 |
proof (cases) |
|
1096 |
assume "x = 0" |
|
1097 |
hence "(\<lambda>n. x ^ Suc n) ----> 0" by (simp add: LIMSEQ_const) |
|
1098 |
thus ?thesis by (rule LIMSEQ_imp_Suc) |
|
1099 |
next |
|
1100 |
assume "0 \<le> x" and "x \<noteq> 0" |
|
1101 |
hence x0: "0 < x" by simp |
|
1102 |
assume x1: "x < 1" |
|
1103 |
from x0 x1 have "1 < inverse x" |
|
1104 |
by (rule real_inverse_gt_one) |
|
1105 |
hence "(\<lambda>n. inverse (inverse x ^ n)) ----> 0" |
|
1106 |
by (rule LIMSEQ_inverse_realpow_zero) |
|
1107 |
thus ?thesis by (simp add: power_inverse) |
|
1108 |
qed |
|
15082 | 1109 |
|
20685
fee8c75e3b5d
added lemmas about LIMSEQ and norm; simplified some proofs
huffman
parents:
20682
diff
changeset
|
1110 |
lemma LIMSEQ_power_zero: |
22974 | 1111 |
fixes x :: "'a::{real_normed_algebra_1,recpower}" |
20685
fee8c75e3b5d
added lemmas about LIMSEQ and norm; simplified some proofs
huffman
parents:
20682
diff
changeset
|
1112 |
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
|
1113 |
apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero]) |
22974 | 1114 |
apply (simp only: LIMSEQ_Zseq_iff, erule Zseq_le) |
1115 |
apply (simp add: power_abs norm_power_ineq) |
|
20685
fee8c75e3b5d
added lemmas about LIMSEQ and norm; simplified some proofs
huffman
parents:
20682
diff
changeset
|
1116 |
done |
fee8c75e3b5d
added lemmas about LIMSEQ and norm; simplified some proofs
huffman
parents:
20682
diff
changeset
|
1117 |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
1118 |
lemma LIMSEQ_divide_realpow_zero: |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
1119 |
"1 < (x::real) ==> (%n. a / (x ^ n)) ----> 0" |
15082 | 1120 |
apply (cut_tac a = a and x1 = "inverse x" in |
1121 |
LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_realpow_zero]) |
|
1122 |
apply (auto simp add: divide_inverse power_inverse) |
|
1123 |
apply (simp add: inverse_eq_divide pos_divide_less_eq) |
|
1124 |
done |
|
1125 |
||
15102 | 1126 |
text{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*} |
15082 | 1127 |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
1128 |
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
|
1129 |
by (rule LIMSEQ_realpow_zero [OF abs_ge_zero]) |
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_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) ----> 0" |
15082 | 1132 |
apply (rule LIMSEQ_rabs_zero [THEN iffD1]) |
1133 |
apply (auto intro: LIMSEQ_rabs_realpow_zero simp add: power_abs) |
|
1134 |
done |
|
1135 |
||
10751 | 1136 |
end |