|
1 (* Title : SEQ.thy |
|
2 Author : Jacques D. Fleuriot |
|
3 Copyright : 1998 University of Cambridge |
|
4 Description : Convergence of sequences and series |
|
5 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
|
6 Additional contributions by Jeremy Avigad and Brian Huffman |
|
7 *) |
|
8 |
|
9 header {* Sequences and Convergence *} |
|
10 |
|
11 theory SEQ |
|
12 imports RealVector RComplete |
|
13 begin |
|
14 |
|
15 definition |
|
16 Zseq :: "[nat \<Rightarrow> 'a::real_normed_vector] \<Rightarrow> bool" where |
|
17 --{*Standard definition of sequence converging to zero*} |
|
18 [code del]: "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)" |
|
19 |
|
20 definition |
|
21 LIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool" |
|
22 ("((_)/ ----> (_))" [60, 60] 60) where |
|
23 --{*Standard definition of convergence of sequence*} |
|
24 [code del]: "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n - L) < r))" |
|
25 |
|
26 definition |
|
27 lim :: "(nat => 'a::real_normed_vector) => 'a" where |
|
28 --{*Standard definition of limit using choice operator*} |
|
29 "lim X = (THE L. X ----> L)" |
|
30 |
|
31 definition |
|
32 convergent :: "(nat => 'a::real_normed_vector) => bool" where |
|
33 --{*Standard definition of convergence*} |
|
34 "convergent X = (\<exists>L. X ----> L)" |
|
35 |
|
36 definition |
|
37 Bseq :: "(nat => 'a::real_normed_vector) => bool" where |
|
38 --{*Standard definition for bounded sequence*} |
|
39 [code del]: "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)" |
|
40 |
|
41 definition |
|
42 monoseq :: "(nat=>real)=>bool" where |
|
43 --{*Definition for monotonicity*} |
|
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))" |
|
45 |
|
46 definition |
|
47 subseq :: "(nat => nat) => bool" where |
|
48 --{*Definition of subsequence*} |
|
49 [code del]: "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))" |
|
50 |
|
51 definition |
|
52 Cauchy :: "(nat => 'a::real_normed_vector) => bool" where |
|
53 --{*Standard definition of the Cauchy condition*} |
|
54 [code del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)" |
|
55 |
|
56 |
|
57 subsection {* Bounded Sequences *} |
|
58 |
|
59 lemma BseqI': assumes K: "\<And>n. norm (X n) \<le> K" shows "Bseq X" |
|
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 |
|
72 lemma BseqI2': assumes K: "\<forall>n\<ge>N. norm (X n) \<le> K" shows "Bseq X" |
|
73 proof (rule BseqI') |
|
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 |
|
85 with 1 have "norm (X n) \<le> Max ?A" by (rule Max_ge) |
|
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) |
|
95 apply (rule_tac N="k" and K="K" in BseqI2') |
|
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 |
|
196 lemma (in bounded_bilinear) Zseq: |
|
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 |
|
276 lemma (in bounded_bilinear) Zseq_left: |
|
277 "Zseq X \<Longrightarrow> Zseq (\<lambda>n. X n ** a)" |
|
278 by (rule bounded_linear_left [THEN bounded_linear.Zseq]) |
|
279 |
|
280 lemma (in bounded_bilinear) Zseq_right: |
|
281 "Zseq X \<Longrightarrow> Zseq (\<lambda>n. a ** X n)" |
|
282 by (rule bounded_linear_right [THEN bounded_linear.Zseq]) |
|
283 |
|
284 lemmas Zseq_mult = mult.Zseq |
|
285 lemmas Zseq_mult_right = mult.Zseq_right |
|
286 lemmas Zseq_mult_left = mult.Zseq_left |
|
287 |
|
288 |
|
289 subsection {* Limits of Sequences *} |
|
290 |
|
291 lemma LIMSEQ_iff: |
|
292 "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)" |
|
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) |
|
297 |
|
298 lemma LIMSEQ_I: |
|
299 "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r) \<Longrightarrow> X ----> L" |
|
300 by (simp add: LIMSEQ_def) |
|
301 |
|
302 lemma LIMSEQ_D: |
|
303 "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r" |
|
304 by (simp add: LIMSEQ_def) |
|
305 |
|
306 lemma LIMSEQ_const: "(\<lambda>n. k) ----> k" |
|
307 by (simp add: LIMSEQ_def) |
|
308 |
|
309 lemma LIMSEQ_const_iff: "(\<lambda>n. k) ----> l = (k = l)" |
|
310 by (simp add: LIMSEQ_Zseq_iff Zseq_const_iff) |
|
311 |
|
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 |
|
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 |
|
328 |
|
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) |
|
338 done |
|
339 |
|
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 |
|
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 |
|
381 Zseq_add Zseq Zseq_left Zseq_right) |
|
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" |
|
386 by (rule mult.LIMSEQ) |
|
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)" |
|
391 by (simp add: ring_simps) |
|
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 |
|
412 proof (rule BseqI2' [rule_format]) |
|
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) |
|
441 apply (rule mult.Bseq_prod_Zseq) |
|
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 |
|
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: |
|
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) |
|
564 apply (frule positive_imp_inverse_positive) |
|
565 apply (frule (1) less_imp_inverse_less) |
|
566 apply (subgoal_tac "0 < X n", simp) |
|
567 apply (erule (1) order_less_trans) |
|
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) |
|
574 apply (cut_tac x = r in reals_Archimedean2) |
|
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 |
|
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 |
|
621 |
|
622 subsection {* Convergence *} |
|
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)" |
|
636 by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def) |
|
637 |
|
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 |
|
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) |
|
664 apply (erule contrapos_np) |
|
665 apply (induct_tac "k") |
|
666 apply (auto intro: order_trans) |
|
667 done |
|
668 |
|
669 lemma monoI1: "\<forall>m. \<forall> n \<ge> m. X m \<le> X n ==> monoseq X" |
|
670 by (simp add: monoseq_def) |
|
671 |
|
672 lemma monoI2: "\<forall>m. \<forall> n \<ge> m. X n \<le> X m ==> monoseq X" |
|
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 |
|
681 text{*Bounded Sequence*} |
|
682 |
|
683 lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)" |
|
684 by (simp add: Bseq_def) |
|
685 |
|
686 lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X" |
|
687 by (auto simp add: Bseq_def) |
|
688 |
|
689 lemma lemma_NBseq_def: |
|
690 "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = |
|
691 (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))" |
|
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 *} |
|
701 lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))" |
|
702 apply (simp add: Bseq_def) |
|
703 apply (simp (no_asm) add: lemma_NBseq_def) |
|
704 done |
|
705 |
|
706 lemma lemma_NBseq_def2: |
|
707 "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))" |
|
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 *) |
|
717 lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))" |
|
718 by (simp add: Bseq_def lemma_NBseq_def2) |
|
719 |
|
720 subsubsection{*Upper Bounds and Lubs of Bounded Sequences*} |
|
721 |
|
722 lemma Bseq_isUb: |
|
723 "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U" |
|
724 by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff) |
|
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 |
|
735 subsubsection{*A Bounded and Monotonic Sequence Converges*} |
|
736 |
|
737 lemma lemma_converg1: |
|
738 "!!(X::nat=>real). [| \<forall>m. \<forall> n \<ge> m. X m \<le> X n; |
|
739 isLub (UNIV::real set) {x. \<exists>n. X n = x} (X ma) |
|
740 |] ==> \<forall>n \<ge> ma. X n = X ma" |
|
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: |
|
786 "[| Bseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> convergent (X::nat=>real)" |
|
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 |
|
813 subsubsection{*A Few More Equivalence Theorems for Boundedness*} |
|
814 |
|
815 text{*alternative formulation for boundedness*} |
|
816 lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)" |
|
817 apply (unfold Bseq_def, safe) |
|
818 apply (rule_tac [2] x = "k + norm x" in exI) |
|
819 apply (rule_tac x = K in exI, simp) |
|
820 apply (rule exI [where x = 0], auto) |
|
821 apply (erule order_less_le_trans, simp) |
|
822 apply (drule_tac x=n in spec, fold diff_def) |
|
823 apply (drule order_trans [OF norm_triangle_ineq2]) |
|
824 apply simp |
|
825 done |
|
826 |
|
827 text{*alternative formulation for boundedness*} |
|
828 lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)" |
|
829 apply safe |
|
830 apply (simp add: Bseq_def, safe) |
|
831 apply (rule_tac x = "K + norm (X N)" in exI) |
|
832 apply auto |
|
833 apply (erule order_less_le_trans, simp) |
|
834 apply (rule_tac x = N in exI, safe) |
|
835 apply (drule_tac x = n in spec) |
|
836 apply (rule order_trans [OF norm_triangle_ineq], simp) |
|
837 apply (auto simp add: Bseq_iff2) |
|
838 done |
|
839 |
|
840 lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f" |
|
841 apply (simp add: Bseq_def) |
|
842 apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto) |
|
843 apply (drule_tac x = n in spec, arith) |
|
844 done |
|
845 |
|
846 |
|
847 subsection {* Cauchy Sequences *} |
|
848 |
|
849 lemma CauchyI: |
|
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" |
|
851 by (simp add: Cauchy_def) |
|
852 |
|
853 lemma CauchyD: |
|
854 "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e" |
|
855 by (simp add: Cauchy_def) |
|
856 |
|
857 subsubsection {* Cauchy Sequences are Bounded *} |
|
858 |
|
859 text{*A Cauchy sequence is bounded -- this is the standard |
|
860 proof mechanization rather than the nonstandard proof*} |
|
861 |
|
862 lemma lemmaCauchy: "\<forall>n \<ge> M. norm (X M - X n) < (1::real) |
|
863 ==> \<forall>n \<ge> M. norm (X n :: 'a::real_normed_vector) < 1 + norm (X M)" |
|
864 apply (clarify, drule spec, drule (1) mp) |
|
865 apply (simp only: norm_minus_commute) |
|
866 apply (drule order_le_less_trans [OF norm_triangle_ineq2]) |
|
867 apply simp |
|
868 done |
|
869 |
|
870 lemma Cauchy_Bseq: "Cauchy X ==> Bseq X" |
|
871 apply (simp add: Cauchy_def) |
|
872 apply (drule spec, drule mp, rule zero_less_one, safe) |
|
873 apply (drule_tac x="M" in spec, simp) |
|
874 apply (drule lemmaCauchy) |
|
875 apply (rule_tac k="M" in Bseq_offset) |
|
876 apply (simp add: Bseq_def) |
|
877 apply (rule_tac x="1 + norm (X M)" in exI) |
|
878 apply (rule conjI, rule order_less_le_trans [OF zero_less_one], simp) |
|
879 apply (simp add: order_less_imp_le) |
|
880 done |
|
881 |
|
882 subsubsection {* Cauchy Sequences are Convergent *} |
|
883 |
|
884 axclass banach \<subseteq> real_normed_vector |
|
885 Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X" |
|
886 |
|
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) |
|
903 also from m n have "\<dots> < e" by(simp add:field_simps) |
|
904 finally show "norm (X m - X n) < e" . |
|
905 qed |
|
906 qed |
|
907 |
|
908 lemma convergent_Cauchy: "convergent X \<Longrightarrow> Cauchy X" |
|
909 unfolding convergent_def |
|
910 by (erule exE, erule LIMSEQ_imp_Cauchy) |
|
911 |
|
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 |
|
929 locale real_Cauchy = |
|
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 |
|
935 lemma real_CauchyI: |
|
936 assumes "Cauchy X" |
|
937 shows "real_Cauchy X" |
|
938 proof qed (fact assms) |
|
939 |
|
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) |
|
991 hence 1: "X N - r/2 \<le> x" using x isLub_isUb isUbD by fast |
|
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) |
|
995 hence 2: "x \<le> X N + r/2" using x isLub_le_isUb by fast |
|
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" |
|
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 |
|
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 |
|
1015 lemma real_Cauchy_convergent: |
|
1016 fixes X :: "nat \<Rightarrow> real" |
|
1017 shows "Cauchy X \<Longrightarrow> convergent X" |
|
1018 unfolding convergent_def |
|
1019 by (rule real_Cauchy.LIMSEQ_ex) |
|
1020 (rule real_CauchyI) |
|
1021 |
|
1022 instance real :: banach |
|
1023 by intro_classes (rule real_Cauchy_convergent) |
|
1024 |
|
1025 lemma Cauchy_convergent_iff: |
|
1026 fixes X :: "nat \<Rightarrow> 'a::banach" |
|
1027 shows "Cauchy X = convergent X" |
|
1028 by (fast intro: Cauchy_convergent convergent_Cauchy) |
|
1029 |
|
1030 |
|
1031 subsection {* Power Sequences *} |
|
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 |
|
1037 lemma Bseq_realpow: "[| 0 \<le> (x::real); x \<le> 1 |] ==> Bseq (%n. x ^ n)" |
|
1038 apply (simp add: Bseq_def) |
|
1039 apply (rule_tac x = 1 in exI) |
|
1040 apply (simp add: power_abs) |
|
1041 apply (auto dest: power_mono) |
|
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 |
|
1049 lemma convergent_realpow: |
|
1050 "[| 0 \<le> (x::real); x \<le> 1 |] ==> convergent (%n. x ^ n)" |
|
1051 by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow) |
|
1052 |
|
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) |
|
1065 apply (simp add: ring_distribs) |
|
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 |
|
1093 lemma LIMSEQ_realpow_zero: |
|
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 |
|
1109 |
|
1110 lemma LIMSEQ_power_zero: |
|
1111 fixes x :: "'a::{real_normed_algebra_1,recpower}" |
|
1112 shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0" |
|
1113 apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero]) |
|
1114 apply (simp only: LIMSEQ_Zseq_iff, erule Zseq_le) |
|
1115 apply (simp add: power_abs norm_power_ineq) |
|
1116 done |
|
1117 |
|
1118 lemma LIMSEQ_divide_realpow_zero: |
|
1119 "1 < (x::real) ==> (%n. a / (x ^ n)) ----> 0" |
|
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 |
|
1126 text{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*} |
|
1127 |
|
1128 lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < (1::real) ==> (%n. \<bar>c\<bar> ^ n) ----> 0" |
|
1129 by (rule LIMSEQ_realpow_zero [OF abs_ge_zero]) |
|
1130 |
|
1131 lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) ----> 0" |
|
1132 apply (rule LIMSEQ_rabs_zero [THEN iffD1]) |
|
1133 apply (auto intro: LIMSEQ_rabs_realpow_zero simp add: power_abs) |
|
1134 done |
|
1135 |
|
1136 end |