73 NSCauchy :: "(nat => 'a::real_normed_vector) => bool" where |
78 NSCauchy :: "(nat => 'a::real_normed_vector) => bool" where |
74 --{*Nonstandard definition*} |
79 --{*Nonstandard definition*} |
75 "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)" |
80 "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)" |
76 |
81 |
77 |
82 |
|
83 subsection {* Bounded Sequences *} |
|
84 |
|
85 lemma BseqI: assumes K: "\<And>n. norm (X n) \<le> K" shows "Bseq X" |
|
86 unfolding Bseq_def |
|
87 proof (intro exI conjI allI) |
|
88 show "0 < max K 1" by simp |
|
89 next |
|
90 fix n::nat |
|
91 have "norm (X n) \<le> K" by (rule K) |
|
92 thus "norm (X n) \<le> max K 1" by simp |
|
93 qed |
|
94 |
|
95 lemma BseqD: "Bseq X \<Longrightarrow> \<exists>K>0. \<forall>n. norm (X n) \<le> K" |
|
96 unfolding Bseq_def by simp |
|
97 |
|
98 lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
|
99 unfolding Bseq_def by auto |
|
100 |
|
101 lemma BseqI2: assumes K: "\<forall>n\<ge>N. norm (X n) \<le> K" shows "Bseq X" |
|
102 proof (rule BseqI) |
|
103 let ?A = "norm ` X ` {..N}" |
|
104 have 1: "finite ?A" by simp |
|
105 have 2: "?A \<noteq> {}" by auto |
|
106 fix n::nat |
|
107 show "norm (X n) \<le> max K (Max ?A)" |
|
108 proof (cases rule: linorder_le_cases) |
|
109 assume "n \<ge> N" |
|
110 hence "norm (X n) \<le> K" using K by simp |
|
111 thus "norm (X n) \<le> max K (Max ?A)" by simp |
|
112 next |
|
113 assume "n \<le> N" |
|
114 hence "norm (X n) \<in> ?A" by simp |
|
115 with 1 2 have "norm (X n) \<le> Max ?A" by (rule Max_ge) |
|
116 thus "norm (X n) \<le> max K (Max ?A)" by simp |
|
117 qed |
|
118 qed |
|
119 |
|
120 lemma Bseq_ignore_initial_segment: "Bseq X \<Longrightarrow> Bseq (\<lambda>n. X (n + k))" |
|
121 unfolding Bseq_def by auto |
|
122 |
|
123 lemma Bseq_offset: "Bseq (\<lambda>n. X (n + k)) \<Longrightarrow> Bseq X" |
|
124 apply (erule BseqE) |
|
125 apply (rule_tac N="k" and K="K" in BseqI2) |
|
126 apply clarify |
|
127 apply (drule_tac x="n - k" in spec, simp) |
|
128 done |
|
129 |
|
130 |
|
131 subsection {* Sequences That Converge to Zero *} |
|
132 |
|
133 lemma ZseqI: |
|
134 "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n) < r) \<Longrightarrow> Zseq X" |
|
135 unfolding Zseq_def by simp |
|
136 |
|
137 lemma ZseqD: |
|
138 "\<lbrakk>Zseq X; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n) < r" |
|
139 unfolding Zseq_def by simp |
|
140 |
|
141 lemma Zseq_zero: "Zseq (\<lambda>n. 0)" |
|
142 unfolding Zseq_def by simp |
|
143 |
|
144 lemma Zseq_const_iff: "Zseq (\<lambda>n. k) = (k = 0)" |
|
145 unfolding Zseq_def by force |
|
146 |
|
147 lemma Zseq_norm_iff: "Zseq (\<lambda>n. norm (X n)) = Zseq (\<lambda>n. X n)" |
|
148 unfolding Zseq_def by simp |
|
149 |
|
150 lemma Zseq_imp_Zseq: |
|
151 assumes X: "Zseq X" |
|
152 assumes Y: "\<And>n. norm (Y n) \<le> norm (X n) * K" |
|
153 shows "Zseq (\<lambda>n. Y n)" |
|
154 proof (cases) |
|
155 assume K: "0 < K" |
|
156 show ?thesis |
|
157 proof (rule ZseqI) |
|
158 fix r::real assume "0 < r" |
|
159 hence "0 < r / K" |
|
160 using K by (rule divide_pos_pos) |
|
161 then obtain N where "\<forall>n\<ge>N. norm (X n) < r / K" |
|
162 using ZseqD [OF X] by fast |
|
163 hence "\<forall>n\<ge>N. norm (X n) * K < r" |
|
164 by (simp add: pos_less_divide_eq K) |
|
165 hence "\<forall>n\<ge>N. norm (Y n) < r" |
|
166 by (simp add: order_le_less_trans [OF Y]) |
|
167 thus "\<exists>N. \<forall>n\<ge>N. norm (Y n) < r" .. |
|
168 qed |
|
169 next |
|
170 assume "\<not> 0 < K" |
|
171 hence K: "K \<le> 0" by (simp only: linorder_not_less) |
|
172 { |
|
173 fix n::nat |
|
174 have "norm (Y n) \<le> norm (X n) * K" by (rule Y) |
|
175 also have "\<dots> \<le> norm (X n) * 0" |
|
176 using K norm_ge_zero by (rule mult_left_mono) |
|
177 finally have "norm (Y n) = 0" by simp |
|
178 } |
|
179 thus ?thesis by (simp add: Zseq_zero) |
|
180 qed |
|
181 |
|
182 lemma Zseq_le: "\<lbrakk>Zseq Y; \<forall>n. norm (X n) \<le> norm (Y n)\<rbrakk> \<Longrightarrow> Zseq X" |
|
183 by (erule_tac K="1" in Zseq_imp_Zseq, simp) |
|
184 |
|
185 lemma Zseq_add: |
|
186 assumes X: "Zseq X" |
|
187 assumes Y: "Zseq Y" |
|
188 shows "Zseq (\<lambda>n. X n + Y n)" |
|
189 proof (rule ZseqI) |
|
190 fix r::real assume "0 < r" |
|
191 hence r: "0 < r / 2" by simp |
|
192 obtain M where M: "\<forall>n\<ge>M. norm (X n) < r/2" |
|
193 using ZseqD [OF X r] by fast |
|
194 obtain N where N: "\<forall>n\<ge>N. norm (Y n) < r/2" |
|
195 using ZseqD [OF Y r] by fast |
|
196 show "\<exists>N. \<forall>n\<ge>N. norm (X n + Y n) < r" |
|
197 proof (intro exI allI impI) |
|
198 fix n assume n: "max M N \<le> n" |
|
199 have "norm (X n + Y n) \<le> norm (X n) + norm (Y n)" |
|
200 by (rule norm_triangle_ineq) |
|
201 also have "\<dots> < r/2 + r/2" |
|
202 proof (rule add_strict_mono) |
|
203 from M n show "norm (X n) < r/2" by simp |
|
204 from N n show "norm (Y n) < r/2" by simp |
|
205 qed |
|
206 finally show "norm (X n + Y n) < r" by simp |
|
207 qed |
|
208 qed |
|
209 |
|
210 lemma Zseq_minus: "Zseq X \<Longrightarrow> Zseq (\<lambda>n. - X n)" |
|
211 unfolding Zseq_def by simp |
|
212 |
|
213 lemma Zseq_diff: "\<lbrakk>Zseq X; Zseq Y\<rbrakk> \<Longrightarrow> Zseq (\<lambda>n. X n - Y n)" |
|
214 by (simp only: diff_minus Zseq_add Zseq_minus) |
|
215 |
|
216 lemma (in bounded_linear) Zseq: |
|
217 assumes X: "Zseq X" |
|
218 shows "Zseq (\<lambda>n. f (X n))" |
|
219 proof - |
|
220 obtain K where "\<And>x. norm (f x) \<le> norm x * K" |
|
221 using bounded by fast |
|
222 with X show ?thesis |
|
223 by (rule Zseq_imp_Zseq) |
|
224 qed |
|
225 |
|
226 lemma (in bounded_bilinear) Zseq_prod: |
|
227 assumes X: "Zseq X" |
|
228 assumes Y: "Zseq Y" |
|
229 shows "Zseq (\<lambda>n. X n ** Y n)" |
|
230 proof (rule ZseqI) |
|
231 fix r::real assume r: "0 < r" |
|
232 obtain K where K: "0 < K" |
|
233 and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K" |
|
234 using pos_bounded by fast |
|
235 from K have K': "0 < inverse K" |
|
236 by (rule positive_imp_inverse_positive) |
|
237 obtain M where M: "\<forall>n\<ge>M. norm (X n) < r" |
|
238 using ZseqD [OF X r] by fast |
|
239 obtain N where N: "\<forall>n\<ge>N. norm (Y n) < inverse K" |
|
240 using ZseqD [OF Y K'] by fast |
|
241 show "\<exists>N. \<forall>n\<ge>N. norm (X n ** Y n) < r" |
|
242 proof (intro exI allI impI) |
|
243 fix n assume n: "max M N \<le> n" |
|
244 have "norm (X n ** Y n) \<le> norm (X n) * norm (Y n) * K" |
|
245 by (rule norm_le) |
|
246 also have "norm (X n) * norm (Y n) * K < r * inverse K * K" |
|
247 proof (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero K) |
|
248 from M n show Xn: "norm (X n) < r" by simp |
|
249 from N n show Yn: "norm (Y n) < inverse K" by simp |
|
250 qed |
|
251 also from K have "r * inverse K * K = r" by simp |
|
252 finally show "norm (X n ** Y n) < r" . |
|
253 qed |
|
254 qed |
|
255 |
|
256 lemma (in bounded_bilinear) Zseq_prod_Bseq: |
|
257 assumes X: "Zseq X" |
|
258 assumes Y: "Bseq Y" |
|
259 shows "Zseq (\<lambda>n. X n ** Y n)" |
|
260 proof - |
|
261 obtain K where K: "0 \<le> K" |
|
262 and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K" |
|
263 using nonneg_bounded by fast |
|
264 obtain B where B: "0 < B" |
|
265 and norm_Y: "\<And>n. norm (Y n) \<le> B" |
|
266 using Y [unfolded Bseq_def] by fast |
|
267 from X show ?thesis |
|
268 proof (rule Zseq_imp_Zseq) |
|
269 fix n::nat |
|
270 have "norm (X n ** Y n) \<le> norm (X n) * norm (Y n) * K" |
|
271 by (rule norm_le) |
|
272 also have "\<dots> \<le> norm (X n) * B * K" |
|
273 by (intro mult_mono' order_refl norm_Y norm_ge_zero |
|
274 mult_nonneg_nonneg K) |
|
275 also have "\<dots> = norm (X n) * (B * K)" |
|
276 by (rule mult_assoc) |
|
277 finally show "norm (X n ** Y n) \<le> norm (X n) * (B * K)" . |
|
278 qed |
|
279 qed |
|
280 |
|
281 lemma (in bounded_bilinear) Bseq_prod_Zseq: |
|
282 assumes X: "Bseq X" |
|
283 assumes Y: "Zseq Y" |
|
284 shows "Zseq (\<lambda>n. X n ** Y n)" |
|
285 proof - |
|
286 obtain K where K: "0 \<le> K" |
|
287 and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K" |
|
288 using nonneg_bounded by fast |
|
289 obtain B where B: "0 < B" |
|
290 and norm_X: "\<And>n. norm (X n) \<le> B" |
|
291 using X [unfolded Bseq_def] by fast |
|
292 from Y show ?thesis |
|
293 proof (rule Zseq_imp_Zseq) |
|
294 fix n::nat |
|
295 have "norm (X n ** Y n) \<le> norm (X n) * norm (Y n) * K" |
|
296 by (rule norm_le) |
|
297 also have "\<dots> \<le> B * norm (Y n) * K" |
|
298 by (intro mult_mono' order_refl norm_X norm_ge_zero |
|
299 mult_nonneg_nonneg K) |
|
300 also have "\<dots> = norm (Y n) * (B * K)" |
|
301 by (simp only: mult_ac) |
|
302 finally show "norm (X n ** Y n) \<le> norm (Y n) * (B * K)" . |
|
303 qed |
|
304 qed |
|
305 |
|
306 lemma (in bounded_bilinear) Zseq_prod_left: |
|
307 "Zseq X \<Longrightarrow> Zseq (\<lambda>n. X n ** a)" |
|
308 by (rule bounded_linear_left [THEN bounded_linear.Zseq]) |
|
309 |
|
310 lemma (in bounded_bilinear) Zseq_prod_right: |
|
311 "Zseq X \<Longrightarrow> Zseq (\<lambda>n. a ** X n)" |
|
312 by (rule bounded_linear_right [THEN bounded_linear.Zseq]) |
|
313 |
|
314 lemmas Zseq_mult = bounded_bilinear_mult.Zseq_prod |
|
315 lemmas Zseq_mult_right = bounded_bilinear_mult.Zseq_prod_right |
|
316 lemmas Zseq_mult_left = bounded_bilinear_mult.Zseq_prod_left |
|
317 |
|
318 |
78 subsection {* Limits of Sequences *} |
319 subsection {* Limits of Sequences *} |
79 |
320 |
80 subsubsection {* Purely standard proofs *} |
321 subsubsection {* Purely standard proofs *} |
81 |
322 |
82 lemma LIMSEQ_iff: |
323 lemma LIMSEQ_iff: |
83 "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)" |
324 "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)" |
84 by (simp add: LIMSEQ_def) |
325 by (rule LIMSEQ_def) |
|
326 |
|
327 lemma LIMSEQ_Zseq_iff: "((\<lambda>n. X n) ----> L) = Zseq (\<lambda>n. X n - L)" |
|
328 by (simp only: LIMSEQ_def Zseq_def) |
85 |
329 |
86 lemma LIMSEQ_I: |
330 lemma LIMSEQ_I: |
87 "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r) \<Longrightarrow> X ----> L" |
331 "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r) \<Longrightarrow> X ----> L" |
88 by (simp add: LIMSEQ_def) |
332 by (simp add: LIMSEQ_def) |
89 |
333 |
90 lemma LIMSEQ_D: |
334 lemma LIMSEQ_D: |
91 "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r" |
335 "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r" |
92 by (simp add: LIMSEQ_def) |
336 by (simp add: LIMSEQ_def) |
93 |
337 |
94 lemma LIMSEQ_const: "(%n. k) ----> k" |
338 lemma LIMSEQ_const: "(\<lambda>n. k) ----> k" |
95 by (simp add: LIMSEQ_def) |
339 by (simp add: LIMSEQ_def) |
|
340 |
|
341 lemma LIMSEQ_const_iff: "(\<lambda>n. k) ----> l = (k = l)" |
|
342 by (simp add: LIMSEQ_Zseq_iff Zseq_const_iff) |
96 |
343 |
97 lemma LIMSEQ_norm: "X ----> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----> norm a" |
344 lemma LIMSEQ_norm: "X ----> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----> norm a" |
98 apply (simp add: LIMSEQ_def, safe) |
345 apply (simp add: LIMSEQ_def, safe) |
99 apply (drule_tac x="r" in spec, safe) |
346 apply (drule_tac x="r" in spec, safe) |
100 apply (rule_tac x="no" in exI, safe) |
347 apply (rule_tac x="no" in exI, safe) |
123 apply (frule mp) |
370 apply (frule mp) |
124 apply arith |
371 apply arith |
125 apply simp |
372 apply simp |
126 done |
373 done |
127 |
374 |
128 subsubsection {* Purely nonstandard proofs *} |
375 lemma add_diff_add: |
129 |
376 fixes a b c d :: "'a::ab_group_add" |
130 lemma NSLIMSEQ_iff: |
377 shows "(a + c) - (b + d) = (a - b) + (c - d)" |
131 "(X ----NS> L) = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)" |
378 by simp |
132 by (simp add: NSLIMSEQ_def) |
379 |
133 |
380 lemma minus_diff_minus: |
134 lemma NSLIMSEQ_I: |
381 fixes a b :: "'a::ab_group_add" |
135 "(\<And>N. N \<in> HNatInfinite \<Longrightarrow> starfun X N \<approx> star_of L) \<Longrightarrow> X ----NS> L" |
382 shows "(- a) - (- b) = - (a - b)" |
136 by (simp add: NSLIMSEQ_def) |
383 by simp |
137 |
384 |
138 lemma NSLIMSEQ_D: |
385 lemma LIMSEQ_add: "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n + Y n) ----> a + b" |
139 "\<lbrakk>X ----NS> L; N \<in> HNatInfinite\<rbrakk> \<Longrightarrow> starfun X N \<approx> star_of L" |
386 by (simp only: LIMSEQ_Zseq_iff add_diff_add Zseq_add) |
140 by (simp add: NSLIMSEQ_def) |
387 |
141 |
388 lemma LIMSEQ_minus: "X ----> a \<Longrightarrow> (\<lambda>n. - X n) ----> - a" |
142 lemma NSLIMSEQ_const: "(%n. k) ----NS> k" |
389 by (simp only: LIMSEQ_Zseq_iff minus_diff_minus Zseq_minus) |
143 by (simp add: NSLIMSEQ_def) |
390 |
144 |
391 lemma LIMSEQ_minus_cancel: "(\<lambda>n. - X n) ----> - a \<Longrightarrow> X ----> a" |
145 lemma NSLIMSEQ_add: |
392 by (drule LIMSEQ_minus, simp) |
146 "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + Y n) ----NS> a + b" |
393 |
147 by (auto intro: approx_add simp add: NSLIMSEQ_def starfun_add [symmetric]) |
394 lemma LIMSEQ_diff: "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n - Y n) ----> a - b" |
148 |
395 by (simp add: diff_minus LIMSEQ_add LIMSEQ_minus) |
149 lemma NSLIMSEQ_add_const: "f ----NS> a ==> (%n.(f n + b)) ----NS> a + b" |
396 |
150 by (simp only: NSLIMSEQ_add NSLIMSEQ_const) |
397 lemma LIMSEQ_unique: "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b" |
151 |
398 by (drule (1) LIMSEQ_diff, simp add: LIMSEQ_const_iff) |
152 lemma NSLIMSEQ_mult: |
399 |
153 fixes a b :: "'a::real_normed_algebra" |
400 lemma (in bounded_linear) LIMSEQ: |
154 shows "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b" |
401 "X ----> a \<Longrightarrow> (\<lambda>n. f (X n)) ----> f a" |
155 by (auto intro!: approx_mult_HFinite simp add: NSLIMSEQ_def) |
402 by (simp only: LIMSEQ_Zseq_iff diff [symmetric] Zseq) |
156 |
403 |
157 lemma NSLIMSEQ_minus: "X ----NS> a ==> (%n. -(X n)) ----NS> -a" |
404 lemma (in bounded_bilinear) LIMSEQ: |
158 by (auto simp add: NSLIMSEQ_def) |
405 "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n ** Y n) ----> a ** b" |
159 |
406 by (simp only: LIMSEQ_Zseq_iff prod_diff_prod |
160 lemma NSLIMSEQ_minus_cancel: "(%n. -(X n)) ----NS> -a ==> X ----NS> a" |
407 Zseq_add Zseq_prod Zseq_prod_left Zseq_prod_right) |
161 by (drule NSLIMSEQ_minus, simp) |
|
162 |
|
163 (* FIXME: delete *) |
|
164 lemma NSLIMSEQ_add_minus: |
|
165 "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + -Y n) ----NS> a + -b" |
|
166 by (simp add: NSLIMSEQ_add NSLIMSEQ_minus) |
|
167 |
|
168 lemma NSLIMSEQ_diff: |
|
169 "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n - Y n) ----NS> a - b" |
|
170 by (simp add: diff_minus NSLIMSEQ_add NSLIMSEQ_minus) |
|
171 |
|
172 lemma NSLIMSEQ_diff_const: "f ----NS> a ==> (%n.(f n - b)) ----NS> a - b" |
|
173 by (simp add: NSLIMSEQ_diff NSLIMSEQ_const) |
|
174 |
|
175 lemma NSLIMSEQ_inverse: |
|
176 fixes a :: "'a::real_normed_div_algebra" |
|
177 shows "[| X ----NS> a; a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)" |
|
178 by (simp add: NSLIMSEQ_def star_of_approx_inverse) |
|
179 |
|
180 lemma NSLIMSEQ_mult_inverse: |
|
181 fixes a b :: "'a::real_normed_field" |
|
182 shows |
|
183 "[| X ----NS> a; Y ----NS> b; b ~= 0 |] ==> (%n. X n / Y n) ----NS> a/b" |
|
184 by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse) |
|
185 |
|
186 lemma starfun_hnorm: "\<And>x. hnorm (( *f* f) x) = ( *f* (\<lambda>x. norm (f x))) x" |
|
187 by transfer simp |
|
188 |
|
189 lemma NSLIMSEQ_norm: "X ----NS> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----NS> norm a" |
|
190 by (simp add: NSLIMSEQ_def starfun_hnorm [symmetric] approx_hnorm) |
|
191 |
|
192 text{*Uniqueness of limit*} |
|
193 lemma NSLIMSEQ_unique: "[| X ----NS> a; X ----NS> b |] ==> a = b" |
|
194 apply (simp add: NSLIMSEQ_def) |
|
195 apply (drule HNatInfinite_whn [THEN [2] bspec])+ |
|
196 apply (auto dest: approx_trans3) |
|
197 done |
|
198 |
|
199 lemma NSLIMSEQ_pow [rule_format]: |
|
200 fixes a :: "'a::{real_normed_algebra,recpower}" |
|
201 shows "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)" |
|
202 apply (induct "m") |
|
203 apply (auto simp add: power_Suc intro: NSLIMSEQ_mult NSLIMSEQ_const) |
|
204 done |
|
205 |
|
206 subsubsection {* Equivalence of @{term LIMSEQ} and @{term NSLIMSEQ} *} |
|
207 |
|
208 lemma LIMSEQ_NSLIMSEQ: |
|
209 assumes X: "X ----> L" shows "X ----NS> L" |
|
210 proof (rule NSLIMSEQ_I) |
|
211 fix N assume N: "N \<in> HNatInfinite" |
|
212 have "starfun X N - star_of L \<in> Infinitesimal" |
|
213 proof (rule InfinitesimalI2) |
|
214 fix r::real assume r: "0 < r" |
|
215 from LIMSEQ_D [OF X r] |
|
216 obtain no where "\<forall>n\<ge>no. norm (X n - L) < r" .. |
|
217 hence "\<forall>n\<ge>star_of no. hnorm (starfun X n - star_of L) < star_of r" |
|
218 by transfer |
|
219 thus "hnorm (starfun X N - star_of L) < star_of r" |
|
220 using N by (simp add: star_of_le_HNatInfinite) |
|
221 qed |
|
222 thus "starfun X N \<approx> star_of L" |
|
223 by (unfold approx_def) |
|
224 qed |
|
225 |
|
226 lemma NSLIMSEQ_LIMSEQ: |
|
227 assumes X: "X ----NS> L" shows "X ----> L" |
|
228 proof (rule LIMSEQ_I) |
|
229 fix r::real assume r: "0 < r" |
|
230 have "\<exists>no. \<forall>n\<ge>no. hnorm (starfun X n - star_of L) < star_of r" |
|
231 proof (intro exI allI impI) |
|
232 fix n assume "whn \<le> n" |
|
233 with HNatInfinite_whn have "n \<in> HNatInfinite" |
|
234 by (rule HNatInfinite_upward_closed) |
|
235 with X have "starfun X n \<approx> star_of L" |
|
236 by (rule NSLIMSEQ_D) |
|
237 hence "starfun X n - star_of L \<in> Infinitesimal" |
|
238 by (unfold approx_def) |
|
239 thus "hnorm (starfun X n - star_of L) < star_of r" |
|
240 using r by (rule InfinitesimalD2) |
|
241 qed |
|
242 thus "\<exists>no. \<forall>n\<ge>no. norm (X n - L) < r" |
|
243 by transfer |
|
244 qed |
|
245 |
|
246 theorem LIMSEQ_NSLIMSEQ_iff: "(f ----> L) = (f ----NS> L)" |
|
247 by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ) |
|
248 |
|
249 (* Used once by Integration/Rats.thy in AFP *) |
|
250 lemma NSLIMSEQ_finite_set: |
|
251 "!!(f::nat=>nat). \<forall>n. n \<le> f n ==> finite {n. f n \<le> u}" |
|
252 by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans) |
|
253 |
|
254 subsubsection {* Derived theorems about @{term LIMSEQ} *} |
|
255 |
|
256 lemma LIMSEQ_add: "[| X ----> a; Y ----> b |] ==> (%n. X n + Y n) ----> a + b" |
|
257 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_add) |
|
258 |
|
259 lemma LIMSEQ_add_const: "f ----> a ==> (%n.(f n + b)) ----> a + b" |
|
260 by (simp add: LIMSEQ_add LIMSEQ_const) |
|
261 |
408 |
262 lemma LIMSEQ_mult: |
409 lemma LIMSEQ_mult: |
263 fixes a b :: "'a::real_normed_algebra" |
410 fixes a b :: "'a::real_normed_algebra" |
264 shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b" |
411 shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b" |
265 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_mult) |
412 by (rule bounded_bilinear_mult.LIMSEQ) |
266 |
413 |
267 lemma LIMSEQ_minus: "X ----> a ==> (%n. -(X n)) ----> -a" |
414 lemma inverse_diff_inverse: |
268 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_minus) |
415 "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk> |
269 |
416 \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)" |
270 lemma LIMSEQ_minus_cancel: "(%n. -(X n)) ----> -a ==> X ----> a" |
417 by (simp add: right_diff_distrib left_diff_distrib mult_assoc) |
271 by (drule LIMSEQ_minus, simp) |
418 |
272 |
419 lemma Bseq_inverse_lemma: |
273 (* FIXME: delete *) |
420 fixes x :: "'a::real_normed_div_algebra" |
274 lemma LIMSEQ_add_minus: |
421 shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r" |
275 "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b" |
422 apply (subst nonzero_norm_inverse, clarsimp) |
276 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_add_minus) |
423 apply (erule (1) le_imp_inverse_le) |
277 |
424 done |
278 lemma LIMSEQ_diff: "[| X ----> a; Y ----> b |] ==> (%n. X n - Y n) ----> a - b" |
425 |
279 by (simp add: diff_minus LIMSEQ_add LIMSEQ_minus) |
426 lemma Bseq_inverse: |
280 |
427 fixes a :: "'a::real_normed_div_algebra" |
281 lemma LIMSEQ_diff_const: "f ----> a ==> (%n.(f n - b)) ----> a - b" |
428 assumes X: "X ----> a" |
282 by (simp add: LIMSEQ_diff LIMSEQ_const) |
429 assumes a: "a \<noteq> 0" |
|
430 shows "Bseq (\<lambda>n. inverse (X n))" |
|
431 proof - |
|
432 from a have "0 < norm a" by simp |
|
433 hence "\<exists>r>0. r < norm a" by (rule dense) |
|
434 then obtain r where r1: "0 < r" and r2: "r < norm a" by fast |
|
435 obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> norm (X n - a) < r" |
|
436 using LIMSEQ_D [OF X r1] by fast |
|
437 show ?thesis |
|
438 proof (rule BseqI2 [rule_format]) |
|
439 fix n assume n: "N \<le> n" |
|
440 hence 1: "norm (X n - a) < r" by (rule N) |
|
441 hence 2: "X n \<noteq> 0" using r2 by auto |
|
442 hence "norm (inverse (X n)) = inverse (norm (X n))" |
|
443 by (rule nonzero_norm_inverse) |
|
444 also have "\<dots> \<le> inverse (norm a - r)" |
|
445 proof (rule le_imp_inverse_le) |
|
446 show "0 < norm a - r" using r2 by simp |
|
447 next |
|
448 have "norm a - norm (X n) \<le> norm (a - X n)" |
|
449 by (rule norm_triangle_ineq2) |
|
450 also have "\<dots> = norm (X n - a)" |
|
451 by (rule norm_minus_commute) |
|
452 also have "\<dots> < r" using 1 . |
|
453 finally show "norm a - r \<le> norm (X n)" by simp |
|
454 qed |
|
455 finally show "norm (inverse (X n)) \<le> inverse (norm a - r)" . |
|
456 qed |
|
457 qed |
|
458 |
|
459 lemma LIMSEQ_inverse_lemma: |
|
460 fixes a :: "'a::real_normed_div_algebra" |
|
461 shows "\<lbrakk>X ----> a; a \<noteq> 0; \<forall>n. X n \<noteq> 0\<rbrakk> |
|
462 \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> inverse a" |
|
463 apply (subst LIMSEQ_Zseq_iff) |
|
464 apply (simp add: inverse_diff_inverse nonzero_imp_inverse_nonzero) |
|
465 apply (rule Zseq_minus) |
|
466 apply (rule Zseq_mult_left) |
|
467 apply (rule bounded_bilinear_mult.Bseq_prod_Zseq) |
|
468 apply (erule (1) Bseq_inverse) |
|
469 apply (simp add: LIMSEQ_Zseq_iff) |
|
470 done |
283 |
471 |
284 lemma LIMSEQ_inverse: |
472 lemma LIMSEQ_inverse: |
285 fixes a :: "'a::real_normed_div_algebra" |
473 fixes a :: "'a::real_normed_div_algebra" |
286 shows "[| X ----> a; a ~= 0 |] ==> (%n. inverse(X n)) ----> inverse(a)" |
474 assumes X: "X ----> a" |
287 by (simp add: NSLIMSEQ_inverse LIMSEQ_NSLIMSEQ_iff) |
475 assumes a: "a \<noteq> 0" |
|
476 shows "(\<lambda>n. inverse (X n)) ----> inverse a" |
|
477 proof - |
|
478 from a have "0 < norm a" by simp |
|
479 then obtain k where "\<forall>n\<ge>k. norm (X n - a) < norm a" |
|
480 using LIMSEQ_D [OF X] by fast |
|
481 hence "\<forall>n\<ge>k. X n \<noteq> 0" by auto |
|
482 hence k: "\<forall>n. X (n + k) \<noteq> 0" by simp |
|
483 |
|
484 from X have "(\<lambda>n. X (n + k)) ----> a" |
|
485 by (rule LIMSEQ_ignore_initial_segment) |
|
486 hence "(\<lambda>n. inverse (X (n + k))) ----> inverse a" |
|
487 using a k by (rule LIMSEQ_inverse_lemma) |
|
488 thus "(\<lambda>n. inverse (X n)) ----> inverse a" |
|
489 by (rule LIMSEQ_offset) |
|
490 qed |
288 |
491 |
289 lemma LIMSEQ_divide: |
492 lemma LIMSEQ_divide: |
290 fixes a b :: "'a::real_normed_field" |
493 fixes a b :: "'a::real_normed_field" |
291 shows "[| X ----> a; Y ----> b; b ~= 0 |] ==> (%n. X n / Y n) ----> a/b" |
494 shows "\<lbrakk>X ----> a; Y ----> b; b \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>n. X n / Y n) ----> a / b" |
292 by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse) |
495 by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse) |
293 |
|
294 lemma LIMSEQ_unique: "[| X ----> a; X ----> b |] ==> a = b" |
|
295 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_unique) |
|
296 |
496 |
297 lemma LIMSEQ_pow: |
497 lemma LIMSEQ_pow: |
298 fixes a :: "'a::{real_normed_algebra,recpower}" |
498 fixes a :: "'a::{real_normed_algebra,recpower}" |
299 shows "X ----> a ==> (%n. (X n) ^ m) ----> a ^ m" |
499 shows "X ----> a \<Longrightarrow> (\<lambda>n. (X n) ^ m) ----> a ^ m" |
300 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_pow) |
500 by (induct m) (simp_all add: power_Suc LIMSEQ_const LIMSEQ_mult) |
301 |
501 |
302 lemma LIMSEQ_setsum: |
502 lemma LIMSEQ_setsum: |
303 assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n" |
503 assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n" |
304 shows "(\<lambda>m. \<Sum>n\<in>S. X n m) ----> (\<Sum>n\<in>S. L n)" |
504 shows "(\<lambda>m. \<Sum>n\<in>S. X n m) ----> (\<Sum>n\<in>S. L n)" |
305 proof (cases "finite S") |
505 proof (cases "finite S") |
339 next |
539 next |
340 case False |
540 case False |
341 thus ?thesis |
541 thus ?thesis |
342 by (simp add: setprod_def LIMSEQ_const) |
542 by (simp add: setprod_def LIMSEQ_const) |
343 qed |
543 qed |
|
544 |
|
545 subsubsection {* Purely nonstandard proofs *} |
|
546 |
|
547 lemma NSLIMSEQ_iff: |
|
548 "(X ----NS> L) = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)" |
|
549 by (simp add: NSLIMSEQ_def) |
|
550 |
|
551 lemma NSLIMSEQ_I: |
|
552 "(\<And>N. N \<in> HNatInfinite \<Longrightarrow> starfun X N \<approx> star_of L) \<Longrightarrow> X ----NS> L" |
|
553 by (simp add: NSLIMSEQ_def) |
|
554 |
|
555 lemma NSLIMSEQ_D: |
|
556 "\<lbrakk>X ----NS> L; N \<in> HNatInfinite\<rbrakk> \<Longrightarrow> starfun X N \<approx> star_of L" |
|
557 by (simp add: NSLIMSEQ_def) |
|
558 |
|
559 lemma NSLIMSEQ_const: "(%n. k) ----NS> k" |
|
560 by (simp add: NSLIMSEQ_def) |
|
561 |
|
562 lemma NSLIMSEQ_add: |
|
563 "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + Y n) ----NS> a + b" |
|
564 by (auto intro: approx_add simp add: NSLIMSEQ_def starfun_add [symmetric]) |
|
565 |
|
566 lemma NSLIMSEQ_add_const: "f ----NS> a ==> (%n.(f n + b)) ----NS> a + b" |
|
567 by (simp only: NSLIMSEQ_add NSLIMSEQ_const) |
|
568 |
|
569 lemma NSLIMSEQ_mult: |
|
570 fixes a b :: "'a::real_normed_algebra" |
|
571 shows "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b" |
|
572 by (auto intro!: approx_mult_HFinite simp add: NSLIMSEQ_def) |
|
573 |
|
574 lemma NSLIMSEQ_minus: "X ----NS> a ==> (%n. -(X n)) ----NS> -a" |
|
575 by (auto simp add: NSLIMSEQ_def) |
|
576 |
|
577 lemma NSLIMSEQ_minus_cancel: "(%n. -(X n)) ----NS> -a ==> X ----NS> a" |
|
578 by (drule NSLIMSEQ_minus, simp) |
|
579 |
|
580 (* FIXME: delete *) |
|
581 lemma NSLIMSEQ_add_minus: |
|
582 "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + -Y n) ----NS> a + -b" |
|
583 by (simp add: NSLIMSEQ_add NSLIMSEQ_minus) |
|
584 |
|
585 lemma NSLIMSEQ_diff: |
|
586 "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n - Y n) ----NS> a - b" |
|
587 by (simp add: diff_minus NSLIMSEQ_add NSLIMSEQ_minus) |
|
588 |
|
589 lemma NSLIMSEQ_diff_const: "f ----NS> a ==> (%n.(f n - b)) ----NS> a - b" |
|
590 by (simp add: NSLIMSEQ_diff NSLIMSEQ_const) |
|
591 |
|
592 lemma NSLIMSEQ_inverse: |
|
593 fixes a :: "'a::real_normed_div_algebra" |
|
594 shows "[| X ----NS> a; a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)" |
|
595 by (simp add: NSLIMSEQ_def star_of_approx_inverse) |
|
596 |
|
597 lemma NSLIMSEQ_mult_inverse: |
|
598 fixes a b :: "'a::real_normed_field" |
|
599 shows |
|
600 "[| X ----NS> a; Y ----NS> b; b ~= 0 |] ==> (%n. X n / Y n) ----NS> a/b" |
|
601 by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse) |
|
602 |
|
603 lemma starfun_hnorm: "\<And>x. hnorm (( *f* f) x) = ( *f* (\<lambda>x. norm (f x))) x" |
|
604 by transfer simp |
|
605 |
|
606 lemma NSLIMSEQ_norm: "X ----NS> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----NS> norm a" |
|
607 by (simp add: NSLIMSEQ_def starfun_hnorm [symmetric] approx_hnorm) |
|
608 |
|
609 text{*Uniqueness of limit*} |
|
610 lemma NSLIMSEQ_unique: "[| X ----NS> a; X ----NS> b |] ==> a = b" |
|
611 apply (simp add: NSLIMSEQ_def) |
|
612 apply (drule HNatInfinite_whn [THEN [2] bspec])+ |
|
613 apply (auto dest: approx_trans3) |
|
614 done |
|
615 |
|
616 lemma NSLIMSEQ_pow [rule_format]: |
|
617 fixes a :: "'a::{real_normed_algebra,recpower}" |
|
618 shows "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)" |
|
619 apply (induct "m") |
|
620 apply (auto simp add: power_Suc intro: NSLIMSEQ_mult NSLIMSEQ_const) |
|
621 done |
|
622 |
|
623 subsubsection {* Equivalence of @{term LIMSEQ} and @{term NSLIMSEQ} *} |
|
624 |
|
625 lemma LIMSEQ_NSLIMSEQ: |
|
626 assumes X: "X ----> L" shows "X ----NS> L" |
|
627 proof (rule NSLIMSEQ_I) |
|
628 fix N assume N: "N \<in> HNatInfinite" |
|
629 have "starfun X N - star_of L \<in> Infinitesimal" |
|
630 proof (rule InfinitesimalI2) |
|
631 fix r::real assume r: "0 < r" |
|
632 from LIMSEQ_D [OF X r] |
|
633 obtain no where "\<forall>n\<ge>no. norm (X n - L) < r" .. |
|
634 hence "\<forall>n\<ge>star_of no. hnorm (starfun X n - star_of L) < star_of r" |
|
635 by transfer |
|
636 thus "hnorm (starfun X N - star_of L) < star_of r" |
|
637 using N by (simp add: star_of_le_HNatInfinite) |
|
638 qed |
|
639 thus "starfun X N \<approx> star_of L" |
|
640 by (unfold approx_def) |
|
641 qed |
|
642 |
|
643 lemma NSLIMSEQ_LIMSEQ: |
|
644 assumes X: "X ----NS> L" shows "X ----> L" |
|
645 proof (rule LIMSEQ_I) |
|
646 fix r::real assume r: "0 < r" |
|
647 have "\<exists>no. \<forall>n\<ge>no. hnorm (starfun X n - star_of L) < star_of r" |
|
648 proof (intro exI allI impI) |
|
649 fix n assume "whn \<le> n" |
|
650 with HNatInfinite_whn have "n \<in> HNatInfinite" |
|
651 by (rule HNatInfinite_upward_closed) |
|
652 with X have "starfun X n \<approx> star_of L" |
|
653 by (rule NSLIMSEQ_D) |
|
654 hence "starfun X n - star_of L \<in> Infinitesimal" |
|
655 by (unfold approx_def) |
|
656 thus "hnorm (starfun X n - star_of L) < star_of r" |
|
657 using r by (rule InfinitesimalD2) |
|
658 qed |
|
659 thus "\<exists>no. \<forall>n\<ge>no. norm (X n - L) < r" |
|
660 by transfer |
|
661 qed |
|
662 |
|
663 theorem LIMSEQ_NSLIMSEQ_iff: "(f ----> L) = (f ----NS> L)" |
|
664 by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ) |
|
665 |
|
666 (* Used once by Integration/Rats.thy in AFP *) |
|
667 lemma NSLIMSEQ_finite_set: |
|
668 "!!(f::nat=>nat). \<forall>n. n \<le> f n ==> finite {n. f n \<le> u}" |
|
669 by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans) |
|
670 |
|
671 subsubsection {* Derived theorems about @{term LIMSEQ} *} |
|
672 |
|
673 lemma LIMSEQ_add_const: "f ----> a ==> (%n.(f n + b)) ----> a + b" |
|
674 by (simp add: LIMSEQ_add LIMSEQ_const) |
|
675 |
|
676 (* FIXME: delete *) |
|
677 lemma LIMSEQ_add_minus: |
|
678 "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b" |
|
679 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_add_minus) |
|
680 |
|
681 lemma LIMSEQ_diff_const: "f ----> a ==> (%n.(f n - b)) ----> a - b" |
|
682 by (simp add: LIMSEQ_diff LIMSEQ_const) |
344 |
683 |
345 lemma LIMSEQ_diff_approach_zero: |
684 lemma LIMSEQ_diff_approach_zero: |
346 "g ----> L ==> (%x. f x - g x) ----> 0 ==> |
685 "g ----> L ==> (%x. f x - g x) ----> 0 ==> |
347 f ----> L" |
686 f ----> L" |
348 apply (drule LIMSEQ_add) |
687 apply (drule LIMSEQ_add) |