1 (* Title : HSEQ.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 section \<open>Sequences and Convergence (Nonstandard)\<close> |
|
10 |
|
11 theory HSEQ |
|
12 imports Limits NatStar |
|
13 begin |
|
14 |
|
15 definition |
|
16 NSLIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool" |
|
17 ("((_)/ \<longlonglongrightarrow>\<^sub>N\<^sub>S (_))" [60, 60] 60) where |
|
18 \<comment>\<open>Nonstandard definition of convergence of sequence\<close> |
|
19 "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)" |
|
20 |
|
21 definition |
|
22 nslim :: "(nat => 'a::real_normed_vector) => 'a" where |
|
23 \<comment>\<open>Nonstandard definition of limit using choice operator\<close> |
|
24 "nslim X = (THE L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)" |
|
25 |
|
26 definition |
|
27 NSconvergent :: "(nat => 'a::real_normed_vector) => bool" where |
|
28 \<comment>\<open>Nonstandard definition of convergence\<close> |
|
29 "NSconvergent X = (\<exists>L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)" |
|
30 |
|
31 definition |
|
32 NSBseq :: "(nat => 'a::real_normed_vector) => bool" where |
|
33 \<comment>\<open>Nonstandard definition for bounded sequence\<close> |
|
34 "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)" |
|
35 |
|
36 definition |
|
37 NSCauchy :: "(nat => 'a::real_normed_vector) => bool" where |
|
38 \<comment>\<open>Nonstandard definition\<close> |
|
39 "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)" |
|
40 |
|
41 subsection \<open>Limits of Sequences\<close> |
|
42 |
|
43 lemma NSLIMSEQ_iff: |
|
44 "(X \<longlonglongrightarrow>\<^sub>N\<^sub>S L) = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)" |
|
45 by (simp add: NSLIMSEQ_def) |
|
46 |
|
47 lemma NSLIMSEQ_I: |
|
48 "(\<And>N. N \<in> HNatInfinite \<Longrightarrow> starfun X N \<approx> star_of L) \<Longrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S L" |
|
49 by (simp add: NSLIMSEQ_def) |
|
50 |
|
51 lemma NSLIMSEQ_D: |
|
52 "\<lbrakk>X \<longlonglongrightarrow>\<^sub>N\<^sub>S L; N \<in> HNatInfinite\<rbrakk> \<Longrightarrow> starfun X N \<approx> star_of L" |
|
53 by (simp add: NSLIMSEQ_def) |
|
54 |
|
55 lemma NSLIMSEQ_const: "(%n. k) \<longlonglongrightarrow>\<^sub>N\<^sub>S k" |
|
56 by (simp add: NSLIMSEQ_def) |
|
57 |
|
58 lemma NSLIMSEQ_add: |
|
59 "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b |] ==> (%n. X n + Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + b" |
|
60 by (auto intro: approx_add simp add: NSLIMSEQ_def starfun_add [symmetric]) |
|
61 |
|
62 lemma NSLIMSEQ_add_const: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S a ==> (%n.(f n + b)) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + b" |
|
63 by (simp only: NSLIMSEQ_add NSLIMSEQ_const) |
|
64 |
|
65 lemma NSLIMSEQ_mult: |
|
66 fixes a b :: "'a::real_normed_algebra" |
|
67 shows "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b |] ==> (%n. X n * Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a * b" |
|
68 by (auto intro!: approx_mult_HFinite simp add: NSLIMSEQ_def) |
|
69 |
|
70 lemma NSLIMSEQ_minus: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a ==> (%n. -(X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S -a" |
|
71 by (auto simp add: NSLIMSEQ_def) |
|
72 |
|
73 lemma NSLIMSEQ_minus_cancel: "(%n. -(X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S -a ==> X \<longlonglongrightarrow>\<^sub>N\<^sub>S a" |
|
74 by (drule NSLIMSEQ_minus, simp) |
|
75 |
|
76 lemma NSLIMSEQ_diff: |
|
77 "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b |] ==> (%n. X n - Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a - b" |
|
78 using NSLIMSEQ_add [of X a "- Y" "- b"] by (simp add: NSLIMSEQ_minus fun_Compl_def) |
|
79 |
|
80 (* FIXME: delete *) |
|
81 lemma NSLIMSEQ_add_minus: |
|
82 "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b |] ==> (%n. X n + -Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + -b" |
|
83 by (simp add: NSLIMSEQ_diff) |
|
84 |
|
85 lemma NSLIMSEQ_diff_const: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S a ==> (%n.(f n - b)) \<longlonglongrightarrow>\<^sub>N\<^sub>S a - b" |
|
86 by (simp add: NSLIMSEQ_diff NSLIMSEQ_const) |
|
87 |
|
88 lemma NSLIMSEQ_inverse: |
|
89 fixes a :: "'a::real_normed_div_algebra" |
|
90 shows "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; a ~= 0 |] ==> (%n. inverse(X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S inverse(a)" |
|
91 by (simp add: NSLIMSEQ_def star_of_approx_inverse) |
|
92 |
|
93 lemma NSLIMSEQ_mult_inverse: |
|
94 fixes a b :: "'a::real_normed_field" |
|
95 shows |
|
96 "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b; b ~= 0 |] ==> (%n. X n / Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a/b" |
|
97 by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse) |
|
98 |
|
99 lemma starfun_hnorm: "\<And>x. hnorm (( *f* f) x) = ( *f* (\<lambda>x. norm (f x))) x" |
|
100 by transfer simp |
|
101 |
|
102 lemma NSLIMSEQ_norm: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. norm (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S norm a" |
|
103 by (simp add: NSLIMSEQ_def starfun_hnorm [symmetric] approx_hnorm) |
|
104 |
|
105 text\<open>Uniqueness of limit\<close> |
|
106 lemma NSLIMSEQ_unique: "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; X \<longlonglongrightarrow>\<^sub>N\<^sub>S b |] ==> a = b" |
|
107 apply (simp add: NSLIMSEQ_def) |
|
108 apply (drule HNatInfinite_whn [THEN [2] bspec])+ |
|
109 apply (auto dest: approx_trans3) |
|
110 done |
|
111 |
|
112 lemma NSLIMSEQ_pow [rule_format]: |
|
113 fixes a :: "'a::{real_normed_algebra,power}" |
|
114 shows "(X \<longlonglongrightarrow>\<^sub>N\<^sub>S a) --> ((%n. (X n) ^ m) \<longlonglongrightarrow>\<^sub>N\<^sub>S a ^ m)" |
|
115 apply (induct "m") |
|
116 apply (auto simp add: power_Suc intro: NSLIMSEQ_mult NSLIMSEQ_const) |
|
117 done |
|
118 |
|
119 text\<open>We can now try and derive a few properties of sequences, |
|
120 starting with the limit comparison property for sequences.\<close> |
|
121 |
|
122 lemma NSLIMSEQ_le: |
|
123 "[| f \<longlonglongrightarrow>\<^sub>N\<^sub>S l; g \<longlonglongrightarrow>\<^sub>N\<^sub>S m; |
|
124 \<exists>N. \<forall>n \<ge> N. f(n) \<le> g(n) |
|
125 |] ==> l \<le> (m::real)" |
|
126 apply (simp add: NSLIMSEQ_def, safe) |
|
127 apply (drule starfun_le_mono) |
|
128 apply (drule HNatInfinite_whn [THEN [2] bspec])+ |
|
129 apply (drule_tac x = whn in spec) |
|
130 apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+ |
|
131 apply clarify |
|
132 apply (auto intro: hypreal_of_real_le_add_Infininitesimal_cancel2) |
|
133 done |
|
134 |
|
135 lemma NSLIMSEQ_le_const: "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S (r::real); \<forall>n. a \<le> X n |] ==> a \<le> r" |
|
136 by (erule NSLIMSEQ_le [OF NSLIMSEQ_const], auto) |
|
137 |
|
138 lemma NSLIMSEQ_le_const2: "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S (r::real); \<forall>n. X n \<le> a |] ==> r \<le> a" |
|
139 by (erule NSLIMSEQ_le [OF _ NSLIMSEQ_const], auto) |
|
140 |
|
141 text\<open>Shift a convergent series by 1: |
|
142 By the equivalence between Cauchiness and convergence and because |
|
143 the successor of an infinite hypernatural is also infinite.\<close> |
|
144 |
|
145 lemma NSLIMSEQ_Suc: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S l ==> (%n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l" |
|
146 apply (unfold NSLIMSEQ_def, safe) |
|
147 apply (drule_tac x="N + 1" in bspec) |
|
148 apply (erule HNatInfinite_add) |
|
149 apply (simp add: starfun_shift_one) |
|
150 done |
|
151 |
|
152 lemma NSLIMSEQ_imp_Suc: "(%n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l ==> f \<longlonglongrightarrow>\<^sub>N\<^sub>S l" |
|
153 apply (unfold NSLIMSEQ_def, safe) |
|
154 apply (drule_tac x="N - 1" in bspec) |
|
155 apply (erule Nats_1 [THEN [2] HNatInfinite_diff]) |
|
156 apply (simp add: starfun_shift_one one_le_HNatInfinite) |
|
157 done |
|
158 |
|
159 lemma NSLIMSEQ_Suc_iff: "((%n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l) = (f \<longlonglongrightarrow>\<^sub>N\<^sub>S l)" |
|
160 by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc) |
|
161 |
|
162 subsubsection \<open>Equivalence of @{term LIMSEQ} and @{term NSLIMSEQ}\<close> |
|
163 |
|
164 lemma LIMSEQ_NSLIMSEQ: |
|
165 assumes X: "X \<longlonglongrightarrow> L" shows "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L" |
|
166 proof (rule NSLIMSEQ_I) |
|
167 fix N assume N: "N \<in> HNatInfinite" |
|
168 have "starfun X N - star_of L \<in> Infinitesimal" |
|
169 proof (rule InfinitesimalI2) |
|
170 fix r::real assume r: "0 < r" |
|
171 from LIMSEQ_D [OF X r] |
|
172 obtain no where "\<forall>n\<ge>no. norm (X n - L) < r" .. |
|
173 hence "\<forall>n\<ge>star_of no. hnorm (starfun X n - star_of L) < star_of r" |
|
174 by transfer |
|
175 thus "hnorm (starfun X N - star_of L) < star_of r" |
|
176 using N by (simp add: star_of_le_HNatInfinite) |
|
177 qed |
|
178 thus "starfun X N \<approx> star_of L" |
|
179 by (unfold approx_def) |
|
180 qed |
|
181 |
|
182 lemma NSLIMSEQ_LIMSEQ: |
|
183 assumes X: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L" shows "X \<longlonglongrightarrow> L" |
|
184 proof (rule LIMSEQ_I) |
|
185 fix r::real assume r: "0 < r" |
|
186 have "\<exists>no. \<forall>n\<ge>no. hnorm (starfun X n - star_of L) < star_of r" |
|
187 proof (intro exI allI impI) |
|
188 fix n assume "whn \<le> n" |
|
189 with HNatInfinite_whn have "n \<in> HNatInfinite" |
|
190 by (rule HNatInfinite_upward_closed) |
|
191 with X have "starfun X n \<approx> star_of L" |
|
192 by (rule NSLIMSEQ_D) |
|
193 hence "starfun X n - star_of L \<in> Infinitesimal" |
|
194 by (unfold approx_def) |
|
195 thus "hnorm (starfun X n - star_of L) < star_of r" |
|
196 using r by (rule InfinitesimalD2) |
|
197 qed |
|
198 thus "\<exists>no. \<forall>n\<ge>no. norm (X n - L) < r" |
|
199 by transfer |
|
200 qed |
|
201 |
|
202 theorem LIMSEQ_NSLIMSEQ_iff: "(f \<longlonglongrightarrow> L) = (f \<longlonglongrightarrow>\<^sub>N\<^sub>S L)" |
|
203 by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ) |
|
204 |
|
205 subsubsection \<open>Derived theorems about @{term NSLIMSEQ}\<close> |
|
206 |
|
207 text\<open>We prove the NS version from the standard one, since the NS proof |
|
208 seems more complicated than the standard one above!\<close> |
|
209 lemma NSLIMSEQ_norm_zero: "((\<lambda>n. norm (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0) = (X \<longlonglongrightarrow>\<^sub>N\<^sub>S 0)" |
|
210 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_norm_zero_iff) |
|
211 |
|
212 lemma NSLIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0) = (f \<longlonglongrightarrow>\<^sub>N\<^sub>S (0::real))" |
|
213 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_rabs_zero_iff) |
|
214 |
|
215 text\<open>Generalization to other limits\<close> |
|
216 lemma NSLIMSEQ_imp_rabs: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S (l::real) ==> (%n. \<bar>f n\<bar>) \<longlonglongrightarrow>\<^sub>N\<^sub>S \<bar>l\<bar>" |
|
217 apply (simp add: NSLIMSEQ_def) |
|
218 apply (auto intro: approx_hrabs |
|
219 simp add: starfun_abs) |
|
220 done |
|
221 |
|
222 lemma NSLIMSEQ_inverse_zero: |
|
223 "\<forall>y::real. \<exists>N. \<forall>n \<ge> N. y < f(n) |
|
224 ==> (%n. inverse(f n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0" |
|
225 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero) |
|
226 |
|
227 lemma NSLIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0" |
|
228 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat del: of_nat_Suc) |
|
229 |
|
230 lemma NSLIMSEQ_inverse_real_of_nat_add: |
|
231 "(%n. r + inverse(real(Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r" |
|
232 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add del: of_nat_Suc) |
|
233 |
|
234 lemma NSLIMSEQ_inverse_real_of_nat_add_minus: |
|
235 "(%n. r + -inverse(real(Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r" |
|
236 using LIMSEQ_inverse_real_of_nat_add_minus by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric]) |
|
237 |
|
238 lemma NSLIMSEQ_inverse_real_of_nat_add_minus_mult: |
|
239 "(%n. r*( 1 + -inverse(real(Suc n)))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r" |
|
240 using LIMSEQ_inverse_real_of_nat_add_minus_mult by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric]) |
|
241 |
|
242 |
|
243 subsection \<open>Convergence\<close> |
|
244 |
|
245 lemma nslimI: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L ==> nslim X = L" |
|
246 apply (simp add: nslim_def) |
|
247 apply (blast intro: NSLIMSEQ_unique) |
|
248 done |
|
249 |
|
250 lemma lim_nslim_iff: "lim X = nslim X" |
|
251 by (simp add: lim_def nslim_def LIMSEQ_NSLIMSEQ_iff) |
|
252 |
|
253 lemma NSconvergentD: "NSconvergent X ==> \<exists>L. (X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)" |
|
254 by (simp add: NSconvergent_def) |
|
255 |
|
256 lemma NSconvergentI: "(X \<longlonglongrightarrow>\<^sub>N\<^sub>S L) ==> NSconvergent X" |
|
257 by (auto simp add: NSconvergent_def) |
|
258 |
|
259 lemma convergent_NSconvergent_iff: "convergent X = NSconvergent X" |
|
260 by (simp add: convergent_def NSconvergent_def LIMSEQ_NSLIMSEQ_iff) |
|
261 |
|
262 lemma NSconvergent_NSLIMSEQ_iff: "NSconvergent X = (X \<longlonglongrightarrow>\<^sub>N\<^sub>S nslim X)" |
|
263 by (auto intro: theI NSLIMSEQ_unique simp add: NSconvergent_def nslim_def) |
|
264 |
|
265 |
|
266 subsection \<open>Bounded Monotonic Sequences\<close> |
|
267 |
|
268 lemma NSBseqD: "[| NSBseq X; N: HNatInfinite |] ==> ( *f* X) N : HFinite" |
|
269 by (simp add: NSBseq_def) |
|
270 |
|
271 lemma Standard_subset_HFinite: "Standard \<subseteq> HFinite" |
|
272 unfolding Standard_def by auto |
|
273 |
|
274 lemma NSBseqD2: "NSBseq X \<Longrightarrow> ( *f* X) N \<in> HFinite" |
|
275 apply (cases "N \<in> HNatInfinite") |
|
276 apply (erule (1) NSBseqD) |
|
277 apply (rule subsetD [OF Standard_subset_HFinite]) |
|
278 apply (simp add: HNatInfinite_def Nats_eq_Standard) |
|
279 done |
|
280 |
|
281 lemma NSBseqI: "\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite ==> NSBseq X" |
|
282 by (simp add: NSBseq_def) |
|
283 |
|
284 text\<open>The standard definition implies the nonstandard definition\<close> |
|
285 |
|
286 lemma Bseq_NSBseq: "Bseq X ==> NSBseq X" |
|
287 proof (unfold NSBseq_def, safe) |
|
288 assume X: "Bseq X" |
|
289 fix N assume N: "N \<in> HNatInfinite" |
|
290 from BseqD [OF X] obtain K where "\<forall>n. norm (X n) \<le> K" by fast |
|
291 hence "\<forall>N. hnorm (starfun X N) \<le> star_of K" by transfer |
|
292 hence "hnorm (starfun X N) \<le> star_of K" by simp |
|
293 also have "star_of K < star_of (K + 1)" by simp |
|
294 finally have "\<exists>x\<in>Reals. hnorm (starfun X N) < x" by (rule bexI, simp) |
|
295 thus "starfun X N \<in> HFinite" by (simp add: HFinite_def) |
|
296 qed |
|
297 |
|
298 text\<open>The nonstandard definition implies the standard definition\<close> |
|
299 |
|
300 lemma SReal_less_omega: "r \<in> \<real> \<Longrightarrow> r < \<omega>" |
|
301 apply (insert HInfinite_omega) |
|
302 apply (simp add: HInfinite_def) |
|
303 apply (simp add: order_less_imp_le) |
|
304 done |
|
305 |
|
306 lemma NSBseq_Bseq: "NSBseq X \<Longrightarrow> Bseq X" |
|
307 proof (rule ccontr) |
|
308 let ?n = "\<lambda>K. LEAST n. K < norm (X n)" |
|
309 assume "NSBseq X" |
|
310 hence finite: "( *f* X) (( *f* ?n) \<omega>) \<in> HFinite" |
|
311 by (rule NSBseqD2) |
|
312 assume "\<not> Bseq X" |
|
313 hence "\<forall>K>0. \<exists>n. K < norm (X n)" |
|
314 by (simp add: Bseq_def linorder_not_le) |
|
315 hence "\<forall>K>0. K < norm (X (?n K))" |
|
316 by (auto intro: LeastI_ex) |
|
317 hence "\<forall>K>0. K < hnorm (( *f* X) (( *f* ?n) K))" |
|
318 by transfer |
|
319 hence "\<omega> < hnorm (( *f* X) (( *f* ?n) \<omega>))" |
|
320 by simp |
|
321 hence "\<forall>r\<in>\<real>. r < hnorm (( *f* X) (( *f* ?n) \<omega>))" |
|
322 by (simp add: order_less_trans [OF SReal_less_omega]) |
|
323 hence "( *f* X) (( *f* ?n) \<omega>) \<in> HInfinite" |
|
324 by (simp add: HInfinite_def) |
|
325 with finite show "False" |
|
326 by (simp add: HFinite_HInfinite_iff) |
|
327 qed |
|
328 |
|
329 text\<open>Equivalence of nonstandard and standard definitions |
|
330 for a bounded sequence\<close> |
|
331 lemma Bseq_NSBseq_iff: "(Bseq X) = (NSBseq X)" |
|
332 by (blast intro!: NSBseq_Bseq Bseq_NSBseq) |
|
333 |
|
334 text\<open>A convergent sequence is bounded: |
|
335 Boundedness as a necessary condition for convergence. |
|
336 The nonstandard version has no existential, as usual\<close> |
|
337 |
|
338 lemma NSconvergent_NSBseq: "NSconvergent X ==> NSBseq X" |
|
339 apply (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def) |
|
340 apply (blast intro: HFinite_star_of approx_sym approx_HFinite) |
|
341 done |
|
342 |
|
343 text\<open>Standard Version: easily now proved using equivalence of NS and |
|
344 standard definitions\<close> |
|
345 |
|
346 lemma convergent_Bseq: "convergent X ==> Bseq (X::nat \<Rightarrow> _::real_normed_vector)" |
|
347 by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff) |
|
348 |
|
349 subsubsection\<open>Upper Bounds and Lubs of Bounded Sequences\<close> |
|
350 |
|
351 lemma NSBseq_isUb: "NSBseq X ==> \<exists>U::real. isUb UNIV {x. \<exists>n. X n = x} U" |
|
352 by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isUb) |
|
353 |
|
354 lemma NSBseq_isLub: "NSBseq X ==> \<exists>U::real. isLub UNIV {x. \<exists>n. X n = x} U" |
|
355 by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub) |
|
356 |
|
357 subsubsection\<open>A Bounded and Monotonic Sequence Converges\<close> |
|
358 |
|
359 text\<open>The best of both worlds: Easier to prove this result as a standard |
|
360 theorem and then use equivalence to "transfer" it into the |
|
361 equivalent nonstandard form if needed!\<close> |
|
362 |
|
363 lemma Bmonoseq_NSLIMSEQ: "\<forall>n \<ge> m. X n = X m ==> \<exists>L. (X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)" |
|
364 by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff) |
|
365 |
|
366 lemma NSBseq_mono_NSconvergent: |
|
367 "[| NSBseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> NSconvergent (X::nat=>real)" |
|
368 by (auto intro: Bseq_mono_convergent |
|
369 simp add: convergent_NSconvergent_iff [symmetric] |
|
370 Bseq_NSBseq_iff [symmetric]) |
|
371 |
|
372 |
|
373 subsection \<open>Cauchy Sequences\<close> |
|
374 |
|
375 lemma NSCauchyI: |
|
376 "(\<And>M N. \<lbrakk>M \<in> HNatInfinite; N \<in> HNatInfinite\<rbrakk> \<Longrightarrow> starfun X M \<approx> starfun X N) |
|
377 \<Longrightarrow> NSCauchy X" |
|
378 by (simp add: NSCauchy_def) |
|
379 |
|
380 lemma NSCauchyD: |
|
381 "\<lbrakk>NSCauchy X; M \<in> HNatInfinite; N \<in> HNatInfinite\<rbrakk> |
|
382 \<Longrightarrow> starfun X M \<approx> starfun X N" |
|
383 by (simp add: NSCauchy_def) |
|
384 |
|
385 subsubsection\<open>Equivalence Between NS and Standard\<close> |
|
386 |
|
387 lemma Cauchy_NSCauchy: |
|
388 assumes X: "Cauchy X" shows "NSCauchy X" |
|
389 proof (rule NSCauchyI) |
|
390 fix M assume M: "M \<in> HNatInfinite" |
|
391 fix N assume N: "N \<in> HNatInfinite" |
|
392 have "starfun X M - starfun X N \<in> Infinitesimal" |
|
393 proof (rule InfinitesimalI2) |
|
394 fix r :: real assume r: "0 < r" |
|
395 from CauchyD [OF X r] |
|
396 obtain k where "\<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r" .. |
|
397 hence "\<forall>m\<ge>star_of k. \<forall>n\<ge>star_of k. |
|
398 hnorm (starfun X m - starfun X n) < star_of r" |
|
399 by transfer |
|
400 thus "hnorm (starfun X M - starfun X N) < star_of r" |
|
401 using M N by (simp add: star_of_le_HNatInfinite) |
|
402 qed |
|
403 thus "starfun X M \<approx> starfun X N" |
|
404 by (unfold approx_def) |
|
405 qed |
|
406 |
|
407 lemma NSCauchy_Cauchy: |
|
408 assumes X: "NSCauchy X" shows "Cauchy X" |
|
409 proof (rule CauchyI) |
|
410 fix r::real assume r: "0 < r" |
|
411 have "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. hnorm (starfun X m - starfun X n) < star_of r" |
|
412 proof (intro exI allI impI) |
|
413 fix M assume "whn \<le> M" |
|
414 with HNatInfinite_whn have M: "M \<in> HNatInfinite" |
|
415 by (rule HNatInfinite_upward_closed) |
|
416 fix N assume "whn \<le> N" |
|
417 with HNatInfinite_whn have N: "N \<in> HNatInfinite" |
|
418 by (rule HNatInfinite_upward_closed) |
|
419 from X M N have "starfun X M \<approx> starfun X N" |
|
420 by (rule NSCauchyD) |
|
421 hence "starfun X M - starfun X N \<in> Infinitesimal" |
|
422 by (unfold approx_def) |
|
423 thus "hnorm (starfun X M - starfun X N) < star_of r" |
|
424 using r by (rule InfinitesimalD2) |
|
425 qed |
|
426 thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r" |
|
427 by transfer |
|
428 qed |
|
429 |
|
430 theorem NSCauchy_Cauchy_iff: "NSCauchy X = Cauchy X" |
|
431 by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy) |
|
432 |
|
433 subsubsection \<open>Cauchy Sequences are Bounded\<close> |
|
434 |
|
435 text\<open>A Cauchy sequence is bounded -- nonstandard version\<close> |
|
436 |
|
437 lemma NSCauchy_NSBseq: "NSCauchy X ==> NSBseq X" |
|
438 by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff) |
|
439 |
|
440 subsubsection \<open>Cauchy Sequences are Convergent\<close> |
|
441 |
|
442 text\<open>Equivalence of Cauchy criterion and convergence: |
|
443 We will prove this using our NS formulation which provides a |
|
444 much easier proof than using the standard definition. We do not |
|
445 need to use properties of subsequences such as boundedness, |
|
446 monotonicity etc... Compare with Harrison's corresponding proof |
|
447 in HOL which is much longer and more complicated. Of course, we do |
|
448 not have problems which he encountered with guessing the right |
|
449 instantiations for his 'espsilon-delta' proof(s) in this case |
|
450 since the NS formulations do not involve existential quantifiers.\<close> |
|
451 |
|
452 lemma NSconvergent_NSCauchy: "NSconvergent X \<Longrightarrow> NSCauchy X" |
|
453 apply (simp add: NSconvergent_def NSLIMSEQ_def NSCauchy_def, safe) |
|
454 apply (auto intro: approx_trans2) |
|
455 done |
|
456 |
|
457 lemma real_NSCauchy_NSconvergent: |
|
458 fixes X :: "nat \<Rightarrow> real" |
|
459 shows "NSCauchy X \<Longrightarrow> NSconvergent X" |
|
460 apply (simp add: NSconvergent_def NSLIMSEQ_def) |
|
461 apply (frule NSCauchy_NSBseq) |
|
462 apply (simp add: NSBseq_def NSCauchy_def) |
|
463 apply (drule HNatInfinite_whn [THEN [2] bspec]) |
|
464 apply (drule HNatInfinite_whn [THEN [2] bspec]) |
|
465 apply (auto dest!: st_part_Ex simp add: SReal_iff) |
|
466 apply (blast intro: approx_trans3) |
|
467 done |
|
468 |
|
469 lemma NSCauchy_NSconvergent: |
|
470 fixes X :: "nat \<Rightarrow> 'a::banach" |
|
471 shows "NSCauchy X \<Longrightarrow> NSconvergent X" |
|
472 apply (drule NSCauchy_Cauchy [THEN Cauchy_convergent]) |
|
473 apply (erule convergent_NSconvergent_iff [THEN iffD1]) |
|
474 done |
|
475 |
|
476 lemma NSCauchy_NSconvergent_iff: |
|
477 fixes X :: "nat \<Rightarrow> 'a::banach" |
|
478 shows "NSCauchy X = NSconvergent X" |
|
479 by (fast intro: NSCauchy_NSconvergent NSconvergent_NSCauchy) |
|
480 |
|
481 |
|
482 subsection \<open>Power Sequences\<close> |
|
483 |
|
484 text\<open>The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term |
|
485 "x<1"}. Proof will use (NS) Cauchy equivalence for convergence and |
|
486 also fact that bounded and monotonic sequence converges.\<close> |
|
487 |
|
488 text\<open>We now use NS criterion to bring proof of theorem through\<close> |
|
489 |
|
490 lemma NSLIMSEQ_realpow_zero: |
|
491 "[| 0 \<le> (x::real); x < 1 |] ==> (%n. x ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0" |
|
492 apply (simp add: NSLIMSEQ_def) |
|
493 apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff) |
|
494 apply (frule NSconvergentD) |
|
495 apply (auto simp add: NSLIMSEQ_def NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfun_pow) |
|
496 apply (frule HNatInfinite_add_one) |
|
497 apply (drule bspec, assumption) |
|
498 apply (drule bspec, assumption) |
|
499 apply (drule_tac x = "N + (1::hypnat) " in bspec, assumption) |
|
500 apply (simp add: hyperpow_add) |
|
501 apply (drule approx_mult_subst_star_of, assumption) |
|
502 apply (drule approx_trans3, assumption) |
|
503 apply (auto simp del: star_of_mult simp add: star_of_mult [symmetric]) |
|
504 done |
|
505 |
|
506 lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < (1::real) ==> (%n. \<bar>c\<bar> ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0" |
|
507 by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric]) |
|
508 |
|
509 lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0" |
|
510 by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric]) |
|
511 |
|
512 (***--------------------------------------------------------------- |
|
513 Theorems proved by Harrison in HOL that we do not need |
|
514 in order to prove equivalence between Cauchy criterion |
|
515 and convergence: |
|
516 -- Show that every sequence contains a monotonic subsequence |
|
517 Goal "\<exists>f. subseq f & monoseq (%n. s (f n))" |
|
518 -- Show that a subsequence of a bounded sequence is bounded |
|
519 Goal "Bseq X ==> Bseq (%n. X (f n))"; |
|
520 -- Show we can take subsequential terms arbitrarily far |
|
521 up a sequence |
|
522 Goal "subseq f ==> n \<le> f(n)"; |
|
523 Goal "subseq f ==> \<exists>n. N1 \<le> n & N2 \<le> f(n)"; |
|
524 ---------------------------------------------------------------***) |
|
525 |
|
526 end |
|