13 begin |
13 begin |
14 |
14 |
15 text{*Standard and Nonstandard Definitions*} |
15 text{*Standard and Nonstandard Definitions*} |
16 |
16 |
17 definition |
17 definition |
18 LIM :: "[real => 'a::real_normed_vector, real, 'a] => bool" |
18 LIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool" |
19 ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) |
19 ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) |
20 "f -- a --> L = |
20 "f -- a --> L = |
21 (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s |
21 (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x + -a) < s |
22 --> norm (f x + -L) < r)" |
22 --> norm (f x + -L) < r)" |
23 |
23 |
24 NSLIM :: "[real => 'a::real_normed_vector, real, 'a] => bool" |
24 NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool" |
25 ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) |
25 ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) |
26 "f -- a --NS> L = |
26 "f -- a --NS> L = |
27 (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))" |
27 (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))" |
28 |
28 |
29 isCont :: "[real => 'a::real_normed_vector, real] => bool" |
29 isCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" |
30 "isCont f a = (f -- a --> (f a))" |
30 "isCont f a = (f -- a --> (f a))" |
31 |
31 |
32 isNSCont :: "[real => 'a::real_normed_vector, real] => bool" |
32 isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" |
33 --{*NS definition dispenses with limit notions*} |
33 --{*NS definition dispenses with limit notions*} |
34 "isNSCont f a = (\<forall>y. y @= star_of a --> |
34 "isNSCont f a = (\<forall>y. y @= star_of a --> |
35 ( *f* f) y @= star_of (f a))" |
35 ( *f* f) y @= star_of (f a))" |
36 |
36 |
37 deriv:: "[real=>real,real,real] => bool" |
37 deriv:: "[real=>real,real,real] => bool" |
76 |
76 |
77 section{*Some Purely Standard Proofs*} |
77 section{*Some Purely Standard Proofs*} |
78 |
78 |
79 lemma LIM_eq: |
79 lemma LIM_eq: |
80 "f -- a --> L = |
80 "f -- a --> L = |
81 (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> norm (f x - L) < r)" |
81 (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)" |
82 by (simp add: LIM_def diff_minus) |
82 by (simp add: LIM_def diff_minus) |
83 |
83 |
84 lemma LIM_I: |
84 lemma LIM_I: |
85 "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> norm (f x - L) < r) |
85 "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r) |
86 ==> f -- a --> L" |
86 ==> f -- a --> L" |
87 by (simp add: LIM_eq) |
87 by (simp add: LIM_eq) |
88 |
88 |
89 lemma LIM_D: |
89 lemma LIM_D: |
90 "[| f -- a --> L; 0<r |] |
90 "[| f -- a --> L; 0<r |] |
91 ==> \<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> norm (f x - L) < r" |
91 ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r" |
92 by (simp add: LIM_eq) |
92 by (simp add: LIM_eq) |
93 |
93 |
94 lemma LIM_const [simp]: "(%x. k) -- x --> k" |
94 lemma LIM_const [simp]: "(%x. k) -- x --> k" |
95 by (simp add: LIM_def) |
95 by (simp add: LIM_def) |
96 |
96 |
97 lemma LIM_add: |
97 lemma LIM_add: |
|
98 fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
98 assumes f: "f -- a --> L" and g: "g -- a --> M" |
99 assumes f: "f -- a --> L" and g: "g -- a --> M" |
99 shows "(%x. f x + g(x)) -- a --> (L + M)" |
100 shows "(%x. f x + g(x)) -- a --> (L + M)" |
100 proof (rule LIM_I) |
101 proof (rule LIM_I) |
101 fix r :: real |
102 fix r :: real |
102 assume r: "0 < r" |
103 assume r: "0 < r" |
103 from LIM_D [OF f half_gt_zero [OF r]] |
104 from LIM_D [OF f half_gt_zero [OF r]] |
104 obtain fs |
105 obtain fs |
105 where fs: "0 < fs" |
106 where fs: "0 < fs" |
106 and fs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < fs --> norm (f x - L) < r/2" |
107 and fs_lt: "\<forall>x. x \<noteq> a & norm (x-a) < fs --> norm (f x - L) < r/2" |
107 by blast |
108 by blast |
108 from LIM_D [OF g half_gt_zero [OF r]] |
109 from LIM_D [OF g half_gt_zero [OF r]] |
109 obtain gs |
110 obtain gs |
110 where gs: "0 < gs" |
111 where gs: "0 < gs" |
111 and gs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < gs --> norm (g x - M) < r/2" |
112 and gs_lt: "\<forall>x. x \<noteq> a & norm (x-a) < gs --> norm (g x - M) < r/2" |
112 by blast |
113 by blast |
113 show "\<exists>s>0.\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> norm (f x + g x - (L + M)) < r" |
114 show "\<exists>s>0.\<forall>x. x \<noteq> a \<and> norm (x-a) < s \<longrightarrow> norm (f x + g x - (L + M)) < r" |
114 proof (intro exI conjI strip) |
115 proof (intro exI conjI strip) |
115 show "0 < min fs gs" by (simp add: fs gs) |
116 show "0 < min fs gs" by (simp add: fs gs) |
116 fix x :: real |
117 fix x :: 'a |
117 assume "x \<noteq> a \<and> \<bar>x-a\<bar> < min fs gs" |
118 assume "x \<noteq> a \<and> norm (x-a) < min fs gs" |
118 hence "x \<noteq> a \<and> \<bar>x-a\<bar> < fs \<and> \<bar>x-a\<bar> < gs" by simp |
119 hence "x \<noteq> a \<and> norm (x-a) < fs \<and> norm (x-a) < gs" by simp |
119 with fs_lt gs_lt |
120 with fs_lt gs_lt |
120 have "norm (f x - L) < r/2" and "norm (g x - M) < r/2" by blast+ |
121 have "norm (f x - L) < r/2" and "norm (g x - M) < r/2" by blast+ |
121 hence "norm (f x - L) + norm (g x - M) < r" by arith |
122 hence "norm (f x - L) + norm (g x - M) < r" by arith |
122 thus "norm (f x + g x - (L + M)) < r" |
123 thus "norm (f x + g x - (L + M)) < r" |
123 by (blast intro: norm_diff_triangle_ineq order_le_less_trans) |
124 by (blast intro: norm_diff_triangle_ineq order_le_less_trans) |
139 lemma LIM_diff: |
140 lemma LIM_diff: |
140 "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) - g(x)) -- x --> l-m" |
141 "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) - g(x)) -- x --> l-m" |
141 by (simp only: diff_minus LIM_add LIM_minus) |
142 by (simp only: diff_minus LIM_add LIM_minus) |
142 |
143 |
143 |
144 |
144 lemma LIM_const_not_eq: "k \<noteq> L ==> ~ ((%x. k) -- a --> L)" |
145 lemma LIM_const_not_eq: |
|
146 fixes a :: "'a::real_normed_div_algebra" |
|
147 shows "k \<noteq> L ==> ~ ((%x. k) -- a --> L)" |
145 apply (simp add: LIM_eq) |
148 apply (simp add: LIM_eq) |
146 apply (rule_tac x="norm (k - L)" in exI, simp, safe) |
149 apply (rule_tac x="norm (k - L)" in exI, simp, safe) |
147 apply (rule_tac x="a + s/2" in exI, simp) |
150 apply (rule_tac x="a + of_real (s/2)" in exI, simp add: norm_of_real) |
148 done |
151 done |
149 |
152 |
150 lemma LIM_const_eq: "(%x. k) -- x --> L ==> k = L" |
153 lemma LIM_const_eq: |
|
154 fixes a :: "'a::real_normed_div_algebra" |
|
155 shows "(%x. k) -- a --> L ==> k = L" |
151 apply (rule ccontr) |
156 apply (rule ccontr) |
152 apply (blast dest: LIM_const_not_eq) |
157 apply (blast dest: LIM_const_not_eq) |
153 done |
158 done |
154 |
159 |
155 lemma LIM_unique: "[| f -- a --> L; f -- a --> M |] ==> L = M" |
160 lemma LIM_unique: |
|
161 fixes a :: "'a::real_normed_div_algebra" |
|
162 shows "[| f -- a --> L; f -- a --> M |] ==> L = M" |
156 apply (drule LIM_diff, assumption) |
163 apply (drule LIM_diff, assumption) |
157 apply (auto dest!: LIM_const_eq) |
164 apply (auto dest!: LIM_const_eq) |
158 done |
165 done |
159 |
166 |
160 lemma LIM_mult_zero: |
167 lemma LIM_mult_zero: |
161 fixes f g :: "real \<Rightarrow> 'a::real_normed_algebra" |
168 fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" |
162 assumes f: "f -- a --> 0" and g: "g -- a --> 0" |
169 assumes f: "f -- a --> 0" and g: "g -- a --> 0" |
163 shows "(%x. f(x) * g(x)) -- a --> 0" |
170 shows "(%x. f(x) * g(x)) -- a --> 0" |
164 proof (rule LIM_I, simp) |
171 proof (rule LIM_I, simp) |
165 fix r :: real |
172 fix r :: real |
166 assume r: "0<r" |
173 assume r: "0<r" |
167 from LIM_D [OF f zero_less_one] |
174 from LIM_D [OF f zero_less_one] |
168 obtain fs |
175 obtain fs |
169 where fs: "0 < fs" |
176 where fs: "0 < fs" |
170 and fs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < fs --> norm (f x) < 1" |
177 and fs_lt: "\<forall>x. x \<noteq> a & norm (x-a) < fs --> norm (f x) < 1" |
171 by auto |
178 by auto |
172 from LIM_D [OF g r] |
179 from LIM_D [OF g r] |
173 obtain gs |
180 obtain gs |
174 where gs: "0 < gs" |
181 where gs: "0 < gs" |
175 and gs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < gs --> norm (g x) < r" |
182 and gs_lt: "\<forall>x. x \<noteq> a & norm (x-a) < gs --> norm (g x) < r" |
176 by auto |
183 by auto |
177 show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> norm (f x * g x) < r)" |
184 show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> a \<and> norm (x-a) < s \<longrightarrow> norm (f x * g x) < r)" |
178 proof (intro exI conjI strip) |
185 proof (intro exI conjI strip) |
179 show "0 < min fs gs" by (simp add: fs gs) |
186 show "0 < min fs gs" by (simp add: fs gs) |
180 fix x :: real |
187 fix x :: 'a |
181 assume "x \<noteq> a \<and> \<bar>x-a\<bar> < min fs gs" |
188 assume "x \<noteq> a \<and> norm (x-a) < min fs gs" |
182 hence "x \<noteq> a \<and> \<bar>x-a\<bar> < fs \<and> \<bar>x-a\<bar> < gs" by simp |
189 hence "x \<noteq> a \<and> norm (x-a) < fs \<and> norm (x-a) < gs" by simp |
183 with fs_lt gs_lt |
190 with fs_lt gs_lt |
184 have "norm (f x) < 1" and "norm (g x) < r" by blast+ |
191 have "norm (f x) < 1" and "norm (g x) < r" by blast+ |
185 hence "norm (f x) * norm (g x) < 1*r" |
192 hence "norm (f x) * norm (g x) < 1*r" |
186 by (rule mult_strict_mono' [OF _ _ norm_ge_zero norm_ge_zero]) |
193 by (rule mult_strict_mono' [OF _ _ norm_ge_zero norm_ge_zero]) |
187 thus "norm (f x * g x) < r" |
194 thus "norm (f x * g x) < r" |
224 |
231 |
225 subsubsection{*Limit: The NS definition implies the standard definition.*} |
232 subsubsection{*Limit: The NS definition implies the standard definition.*} |
226 |
233 |
227 lemma lemma_LIM: |
234 lemma lemma_LIM: |
228 fixes L :: "'a::real_normed_vector" |
235 fixes L :: "'a::real_normed_vector" |
229 shows "\<forall>s>0. \<exists>x. x \<noteq> a \<and> \<bar>x + - a\<bar> < s \<and> \<not> norm (f x + -L) < r |
236 shows "\<forall>s>0. \<exists>x. x \<noteq> a \<and> norm (x + - a) < s \<and> \<not> norm (f x + -L) < r |
230 ==> \<forall>n::nat. \<exists>x. x \<noteq> a \<and> |
237 ==> \<forall>n::nat. \<exists>x. x \<noteq> a \<and> |
231 \<bar>x + -a\<bar> < inverse(real(Suc n)) \<and> \<not> norm (f x + -L) < r" |
238 norm (x + -a) < inverse(real(Suc n)) \<and> \<not> norm (f x + -L) < r" |
232 apply clarify |
239 apply clarify |
233 apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto) |
240 apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto) |
234 done |
241 done |
235 |
242 |
236 lemma lemma_skolemize_LIM2: |
243 lemma lemma_skolemize_LIM2: |
237 fixes L :: "'a::real_normed_vector" |
244 fixes L :: "'a::real_normed_vector" |
238 shows "\<forall>s>0. \<exists>x. x \<noteq> a \<and> \<bar>x + - a\<bar> < s \<and> \<not> norm (f x + -L) < r |
245 shows "\<forall>s>0. \<exists>x. x \<noteq> a \<and> norm (x + - a) < s \<and> \<not> norm (f x + -L) < r |
239 ==> \<exists>X. \<forall>n::nat. X n \<noteq> a \<and> |
246 ==> \<exists>X. \<forall>n::nat. X n \<noteq> a \<and> |
240 \<bar>X n + -a\<bar> < inverse(real(Suc n)) \<and> \<not> norm(f (X n) + -L) < r" |
247 norm (X n + -a) < inverse(real(Suc n)) \<and> \<not> norm(f (X n) + -L) < r" |
241 apply (drule lemma_LIM) |
248 apply (drule lemma_LIM) |
242 apply (drule choice, blast) |
249 apply (drule choice, blast) |
243 done |
250 done |
244 |
251 |
245 lemma FreeUltrafilterNat_most: "\<exists>N. \<forall>n\<ge>N. P n \<Longrightarrow> {n. P n} \<in> \<U>" |
252 lemma FreeUltrafilterNat_most: "\<exists>N. \<forall>n\<ge>N. P n \<Longrightarrow> {n. P n} \<in> \<U>" |
357 lemma LIM_zero_cancel: "(%x. f(x) - l) -- x --> 0 ==> f -- x --> l" |
364 lemma LIM_zero_cancel: "(%x. f(x) - l) -- x --> 0 ==> f -- x --> l" |
358 apply (drule_tac g = "%x. l" and M = l in LIM_add) |
365 apply (drule_tac g = "%x. l" and M = l in LIM_add) |
359 apply (auto simp add: diff_minus add_assoc) |
366 apply (auto simp add: diff_minus add_assoc) |
360 done |
367 done |
361 |
368 |
362 lemma NSLIM_const_not_eq: "k \<noteq> L ==> ~ ((%x. k) -- x --NS> L)" |
369 lemma NSLIM_const_not_eq: |
|
370 fixes a :: real (* TODO: generalize to real_normed_div_algebra *) |
|
371 shows "k \<noteq> L ==> ~ ((%x. k) -- a --NS> L)" |
363 apply (simp add: NSLIM_def) |
372 apply (simp add: NSLIM_def) |
364 apply (rule_tac x = "hypreal_of_real x + epsilon" in exI) |
373 apply (rule_tac x="star_of a + epsilon" in exI) |
365 apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym] |
374 apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym] |
366 simp add: hypreal_epsilon_not_zero) |
375 simp add: hypreal_epsilon_not_zero) |
367 done |
376 done |
368 |
377 |
369 lemma NSLIM_not_zero: "k \<noteq> 0 ==> ~ ((%x. k) -- x --NS> 0)" |
378 lemma NSLIM_not_zero: |
|
379 fixes a :: real |
|
380 shows "k \<noteq> 0 ==> ~ ((%x. k) -- a --NS> 0)" |
370 by (rule NSLIM_const_not_eq) |
381 by (rule NSLIM_const_not_eq) |
371 |
382 |
372 lemma NSLIM_const_eq: "(%x. k) -- x --NS> L ==> k = L" |
383 lemma NSLIM_const_eq: |
|
384 fixes a :: real |
|
385 shows "(%x. k) -- a --NS> L ==> k = L" |
373 apply (rule ccontr) |
386 apply (rule ccontr) |
374 apply (blast dest: NSLIM_const_not_eq) |
387 apply (blast dest: NSLIM_const_not_eq) |
375 done |
388 done |
376 |
389 |
377 text{* can actually be proved more easily by unfolding the definition!*} |
390 text{* can actually be proved more easily by unfolding the definition!*} |
378 lemma NSLIM_unique: "[| f -- x --NS> L; f -- x --NS> M |] ==> L = M" |
391 lemma NSLIM_unique: |
|
392 fixes a :: real |
|
393 shows "[| f -- a --NS> L; f -- a --NS> M |] ==> L = M" |
379 apply (drule NSLIM_minus) |
394 apply (drule NSLIM_minus) |
380 apply (drule NSLIM_add, assumption) |
395 apply (drule NSLIM_add, assumption) |
381 apply (auto dest!: NSLIM_const_eq [symmetric]) |
396 apply (auto dest!: NSLIM_const_eq [symmetric]) |
382 apply (simp add: diff_def [symmetric]) |
397 apply (simp add: diff_def [symmetric]) |
383 done |
398 done |
384 |
399 |
385 lemma LIM_unique2: "[| f -- x --> L; f -- x --> M |] ==> L = M" |
400 lemma LIM_unique2: |
|
401 fixes a :: real |
|
402 shows "[| f -- a --> L; f -- a --> M |] ==> L = M" |
386 by (simp add: LIM_NSLIM_iff NSLIM_unique) |
403 by (simp add: LIM_NSLIM_iff NSLIM_unique) |
387 |
404 |
388 |
405 |
389 lemma NSLIM_mult_zero: |
406 lemma NSLIM_mult_zero: |
390 fixes f g :: "real \<Rightarrow> 'a::real_normed_algebra" |
407 fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" |
391 shows "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0" |
408 shows "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0" |
392 by (drule NSLIM_mult, auto) |
409 by (drule NSLIM_mult, auto) |
393 |
410 |
394 (* we can use the corresponding thm LIM_mult2 *) |
411 (* we can use the corresponding thm LIM_mult2 *) |
395 (* for standard definition of limit *) |
412 (* for standard definition of limit *) |
396 |
413 |
397 lemma LIM_mult_zero2: |
414 lemma LIM_mult_zero2: |
398 fixes f g :: "real \<Rightarrow> 'a::real_normed_algebra" |
415 fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" |
399 shows "[| f -- x --> 0; g -- x --> 0 |] ==> (%x. f(x)*g(x)) -- x --> 0" |
416 shows "[| f -- x --> 0; g -- x --> 0 |] ==> (%x. f(x)*g(x)) -- x --> 0" |
400 by (drule LIM_mult2, auto) |
417 by (drule LIM_mult2, auto) |
401 |
418 |
402 |
419 |
403 lemma NSLIM_self: "(%x. x) -- a --NS> a" |
420 lemma NSLIM_self: "(%x. x) -- a --NS> a" |
414 lemma isNSCont_NSLIM: "isNSCont f a ==> f -- a --NS> (f a) " |
431 lemma isNSCont_NSLIM: "isNSCont f a ==> f -- a --NS> (f a) " |
415 by (simp add: isNSCont_def NSLIM_def) |
432 by (simp add: isNSCont_def NSLIM_def) |
416 |
433 |
417 lemma NSLIM_isNSCont: "f -- a --NS> (f a) ==> isNSCont f a" |
434 lemma NSLIM_isNSCont: "f -- a --NS> (f a) ==> isNSCont f a" |
418 apply (simp add: isNSCont_def NSLIM_def, auto) |
435 apply (simp add: isNSCont_def NSLIM_def, auto) |
419 apply (rule_tac Q = "y = hypreal_of_real a" in excluded_middle [THEN disjE], auto) |
436 apply (case_tac "y = star_of a", auto) |
420 done |
437 done |
421 |
438 |
422 text{*NS continuity can be defined using NS Limit in |
439 text{*NS continuity can be defined using NS Limit in |
423 similar fashion to standard def of continuity*} |
440 similar fashion to standard def of continuity*} |
424 lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f -- a --NS> (f a))" |
441 lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f -- a --NS> (f a))" |
447 text{*Alternative definition of continuity*} |
464 text{*Alternative definition of continuity*} |
448 (* Prove equivalence between NS limits - *) |
465 (* Prove equivalence between NS limits - *) |
449 (* seems easier than using standard def *) |
466 (* seems easier than using standard def *) |
450 lemma NSLIM_h_iff: "(f -- a --NS> L) = ((%h. f(a + h)) -- 0 --NS> L)" |
467 lemma NSLIM_h_iff: "(f -- a --NS> L) = ((%h. f(a + h)) -- 0 --NS> L)" |
451 apply (simp add: NSLIM_def, auto) |
468 apply (simp add: NSLIM_def, auto) |
452 apply (drule_tac x = "hypreal_of_real a + x" in spec) |
469 apply (drule_tac x = "star_of a + x" in spec) |
453 apply (drule_tac [2] x = "-hypreal_of_real a + x" in spec, safe, simp) |
470 apply (drule_tac [2] x = "- star_of a + x" in spec, safe, simp) |
454 apply (rule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]]) |
471 apply (erule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]]) |
455 apply (rule_tac [4] approx_minus_iff2 [THEN iffD1]) |
472 apply (erule_tac [3] approx_minus_iff2 [THEN iffD1]) |
456 prefer 3 apply (simp add: add_commute) |
473 prefer 2 apply (simp add: add_commute diff_def [symmetric]) |
|
474 apply (rule_tac x = x in star_cases) |
457 apply (rule_tac [2] x = x in star_cases) |
475 apply (rule_tac [2] x = x in star_cases) |
458 apply (rule_tac [4] x = x in star_cases) |
|
459 apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num) |
476 apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num) |
460 done |
477 done |
461 |
478 |
462 lemma NSLIM_isCont_iff: "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)" |
479 lemma NSLIM_isCont_iff: "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)" |
463 by (rule NSLIM_h_iff) |
480 by (rule NSLIM_h_iff) |
474 lemma isCont_add: "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) + g(x)) a" |
491 lemma isCont_add: "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) + g(x)) a" |
475 by (auto intro: approx_add simp add: isNSCont_isCont_iff [symmetric] isNSCont_def) |
492 by (auto intro: approx_add simp add: isNSCont_isCont_iff [symmetric] isNSCont_def) |
476 |
493 |
477 text{*mult continuous*} |
494 text{*mult continuous*} |
478 lemma isCont_mult: |
495 lemma isCont_mult: |
479 fixes f g :: "real \<Rightarrow> 'a::real_normed_algebra" |
496 fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" |
480 shows "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) * g(x)) a" |
497 shows "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) * g(x)) a" |
481 by (auto intro!: starfun_mult_HFinite_approx |
498 by (auto intro!: starfun_mult_HFinite_approx |
482 simp del: starfun_mult [symmetric] |
499 simp del: starfun_mult [symmetric] |
483 simp add: isNSCont_isCont_iff [symmetric] isNSCont_def) |
500 simp add: isNSCont_isCont_iff [symmetric] isNSCont_def) |
484 |
501 |
495 |
512 |
496 lemma isCont_minus: "isCont f a ==> isCont (%x. - f x) a" |
513 lemma isCont_minus: "isCont f a ==> isCont (%x. - f x) a" |
497 by (auto simp add: isNSCont_isCont_iff [symmetric] isNSCont_minus) |
514 by (auto simp add: isNSCont_isCont_iff [symmetric] isNSCont_minus) |
498 |
515 |
499 lemma isCont_inverse: |
516 lemma isCont_inverse: |
500 fixes f :: "real \<Rightarrow> 'a::{real_normed_div_algebra,division_by_zero}" |
517 fixes f :: "'a::real_normed_vector \<Rightarrow> |
|
518 'b::{real_normed_div_algebra,division_by_zero}" |
501 shows "[| isCont f x; f x \<noteq> 0 |] ==> isCont (%x. inverse (f x)) x" |
519 shows "[| isCont f x; f x \<noteq> 0 |] ==> isCont (%x. inverse (f x)) x" |
502 apply (simp add: isCont_def) |
520 apply (simp add: isCont_def) |
503 apply (blast intro: LIM_inverse) |
521 apply (blast intro: LIM_inverse) |
504 done |
522 done |
505 |
523 |
506 lemma isNSCont_inverse: |
524 lemma isNSCont_inverse: |
507 fixes f :: "real \<Rightarrow> 'a::{real_normed_div_algebra,division_by_zero}" |
525 fixes f :: "'a::real_normed_vector \<Rightarrow> |
|
526 'b::{real_normed_div_algebra,division_by_zero}" |
508 shows "[| isNSCont f x; f x \<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x" |
527 shows "[| isNSCont f x; f x \<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x" |
509 by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff) |
528 by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff) |
510 |
529 |
511 lemma isCont_diff: |
530 lemma isCont_diff: |
512 "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) - g(x)) a" |
531 "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) - g(x)) a" |
518 by (simp add: isCont_def) |
537 by (simp add: isCont_def) |
519 |
538 |
520 lemma isNSCont_const [simp]: "isNSCont (%x. k) a" |
539 lemma isNSCont_const [simp]: "isNSCont (%x. k) a" |
521 by (simp add: isNSCont_def) |
540 by (simp add: isNSCont_def) |
522 |
541 |
523 lemma isNSCont_abs [simp]: "isNSCont abs a" |
542 lemma isNSCont_abs [simp]: "isNSCont abs (a::real)" |
524 apply (simp add: isNSCont_def) |
543 apply (simp add: isNSCont_def) |
525 apply (auto intro: approx_hrabs simp add: hypreal_of_real_hrabs [symmetric] starfun_rabs_hrabs) |
544 apply (auto intro: approx_hrabs simp add: hypreal_of_real_hrabs [symmetric] starfun_rabs_hrabs) |
526 done |
545 done |
527 |
546 |
528 lemma isCont_abs [simp]: "isCont abs a" |
547 lemma isCont_abs [simp]: "isCont abs (a::real)" |
529 by (auto simp add: isNSCont_isCont_iff [symmetric]) |
548 by (auto simp add: isNSCont_isCont_iff [symmetric]) |
530 |
549 |
531 |
550 |
532 (**************************************************************** |
551 (**************************************************************** |
533 (%* Leave as commented until I add topology theory or remove? *%) |
552 (%* Leave as commented until I add topology theory or remove? *%) |
694 obtain s |
713 obtain s |
695 where s: "0 < s" |
714 where s: "0 < s" |
696 and s_lt: "\<forall>x. x \<noteq> 0 & \<bar>x\<bar> < s --> \<bar>(f (a + x) - f a) / x - D\<bar> < r" |
715 and s_lt: "\<forall>x. x \<noteq> 0 & \<bar>x\<bar> < s --> \<bar>(f (a + x) - f a) / x - D\<bar> < r" |
697 by auto |
716 by auto |
698 show "\<exists>s. 0 < s \<and> |
717 show "\<exists>s. 0 < s \<and> |
699 (\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> norm ((f x - f a) / (x-a) - D) < r)" |
718 (\<forall>x. x \<noteq> a \<and> norm (x-a) < s \<longrightarrow> norm ((f x - f a) / (x-a) - D) < r)" |
700 proof (intro exI conjI strip) |
719 proof (intro exI conjI strip) |
701 show "0 < s" by (rule s) |
720 show "0 < s" by (rule s) |
702 next |
721 next |
703 fix x::real |
722 fix x::real |
704 assume "x \<noteq> a \<and> \<bar>x-a\<bar> < s" |
723 assume "x \<noteq> a \<and> norm (x-a) < s" |
705 with s_lt [THEN spec [where x="x-a"]] |
724 with s_lt [THEN spec [where x="x-a"]] |
706 show "norm ((f x - f a) / (x-a) - D) < r" by auto |
725 show "norm ((f x - f a) / (x-a) - D) < r" by auto |
707 qed |
726 qed |
708 next |
727 next |
709 fix r::real |
728 fix r::real |
713 obtain s |
732 obtain s |
714 where s: "0 < s" |
733 where s: "0 < s" |
715 and s_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>(f x - f a)/(x-a) - D\<bar> < r" |
734 and s_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>(f x - f a)/(x-a) - D\<bar> < r" |
716 by auto |
735 by auto |
717 show "\<exists>s. 0 < s \<and> |
736 show "\<exists>s. 0 < s \<and> |
718 (\<forall>x. x \<noteq> 0 & \<bar>x - 0\<bar> < s --> norm ((f (a + x) - f a) / x - D) < r)" |
737 (\<forall>x. x \<noteq> 0 & norm (x - 0) < s --> norm ((f (a + x) - f a) / x - D) < r)" |
719 proof (intro exI conjI strip) |
738 proof (intro exI conjI strip) |
720 show "0 < s" by (rule s) |
739 show "0 < s" by (rule s) |
721 next |
740 next |
722 fix x::real |
741 fix x::real |
723 assume "x \<noteq> 0 \<and> \<bar>x - 0\<bar> < s" |
742 assume "x \<noteq> 0 \<and> norm (x - 0) < s" |
724 with s_lt [THEN spec [where x="x+a"]] |
743 with s_lt [THEN spec [where x="x+a"]] |
725 show "norm ((f (a + x) - f a) / x - D) < r" by (auto simp add: add_ac) |
744 show "norm ((f (a + x) - f a) / x - D) < r" by (auto simp add: add_ac) |
726 qed |
745 qed |
727 qed |
746 qed |
728 |
747 |
1413 done |
1432 done |
1414 |
1433 |
1415 |
1434 |
1416 subsection{*Intermediate Value Theorem: Prove Contrapositive by Bisection*} |
1435 subsection{*Intermediate Value Theorem: Prove Contrapositive by Bisection*} |
1417 |
1436 |
1418 lemma IVT: "[| f(a) \<le> (y::real); y \<le> f(b); |
1437 lemma IVT: "[| f(a::real) \<le> (y::real); y \<le> f(b); |
1419 a \<le> b; |
1438 a \<le> b; |
1420 (\<forall>x. a \<le> x & x \<le> b --> isCont f x) |] |
1439 (\<forall>x. a \<le> x & x \<le> b --> isCont f x) |] |
1421 ==> \<exists>x. a \<le> x & x \<le> b & f(x) = y" |
1440 ==> \<exists>x. a \<le> x & x \<le> b & f(x) = y" |
1422 apply (rule contrapos_pp, assumption) |
1441 apply (rule contrapos_pp, assumption) |
1423 apply (cut_tac P = "% (u,v) . a \<le> u & u \<le> v & v \<le> b --> ~ (f (u) \<le> y & y \<le> f (v))" in lemma_BOLZANO2) |
1442 apply (cut_tac P = "% (u,v) . a \<le> u & u \<le> v & v \<le> b --> ~ (f (u) \<le> y & y \<le> f (v))" in lemma_BOLZANO2) |
1440 apply (simp_all add: abs_if) |
1459 apply (simp_all add: abs_if) |
1441 apply (drule_tac x = "aa-x" in spec) |
1460 apply (drule_tac x = "aa-x" in spec) |
1442 apply (case_tac "x \<le> aa", simp_all) |
1461 apply (case_tac "x \<le> aa", simp_all) |
1443 done |
1462 done |
1444 |
1463 |
1445 lemma IVT2: "[| f(b) \<le> (y::real); y \<le> f(a); |
1464 lemma IVT2: "[| f(b::real) \<le> (y::real); y \<le> f(a); |
1446 a \<le> b; |
1465 a \<le> b; |
1447 (\<forall>x. a \<le> x & x \<le> b --> isCont f x) |
1466 (\<forall>x. a \<le> x & x \<le> b --> isCont f x) |
1448 |] ==> \<exists>x. a \<le> x & x \<le> b & f(x) = y" |
1467 |] ==> \<exists>x. a \<le> x & x \<le> b & f(x) = y" |
1449 apply (subgoal_tac "- f a \<le> -y & -y \<le> - f b", clarify) |
1468 apply (subgoal_tac "- f a \<le> -y & -y \<le> - f b", clarify) |
1450 apply (drule IVT [where f = "%x. - f x"], assumption) |
1469 apply (drule IVT [where f = "%x. - f x"], assumption) |
1451 apply (auto intro: isCont_minus) |
1470 apply (auto intro: isCont_minus) |
1452 done |
1471 done |
1453 |
1472 |
1454 (*HOL style here: object-level formulations*) |
1473 (*HOL style here: object-level formulations*) |
1455 lemma IVT_objl: "(f(a) \<le> (y::real) & y \<le> f(b) & a \<le> b & |
1474 lemma IVT_objl: "(f(a::real) \<le> (y::real) & y \<le> f(b) & a \<le> b & |
1456 (\<forall>x. a \<le> x & x \<le> b --> isCont f x)) |
1475 (\<forall>x. a \<le> x & x \<le> b --> isCont f x)) |
1457 --> (\<exists>x. a \<le> x & x \<le> b & f(x) = y)" |
1476 --> (\<exists>x. a \<le> x & x \<le> b & f(x) = y)" |
1458 apply (blast intro: IVT) |
1477 apply (blast intro: IVT) |
1459 done |
1478 done |
1460 |
1479 |
1461 lemma IVT2_objl: "(f(b) \<le> (y::real) & y \<le> f(a) & a \<le> b & |
1480 lemma IVT2_objl: "(f(b::real) \<le> (y::real) & y \<le> f(a) & a \<le> b & |
1462 (\<forall>x. a \<le> x & x \<le> b --> isCont f x)) |
1481 (\<forall>x. a \<le> x & x \<le> b --> isCont f x)) |
1463 --> (\<exists>x. a \<le> x & x \<le> b & f(x) = y)" |
1482 --> (\<exists>x. a \<le> x & x \<le> b & f(x) = y)" |
1464 apply (blast intro: IVT2) |
1483 apply (blast intro: IVT2) |
1465 done |
1484 done |
1466 |
1485 |
1467 subsection{*By bisection, function continuous on closed interval is bounded above*} |
1486 subsection{*By bisection, function continuous on closed interval is bounded above*} |
1468 |
1487 |
1469 lemma isCont_bounded: |
1488 lemma isCont_bounded: |
1470 "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |] |
1489 "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |] |
1471 ==> \<exists>M::real. \<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M" |
1490 ==> \<exists>M::real. \<forall>x::real. a \<le> x & x \<le> b --> f(x) \<le> M" |
1472 apply (cut_tac P = "% (u,v) . a \<le> u & u \<le> v & v \<le> b --> (\<exists>M. \<forall>x. u \<le> x & x \<le> v --> f x \<le> M)" in lemma_BOLZANO2) |
1491 apply (cut_tac P = "% (u,v) . a \<le> u & u \<le> v & v \<le> b --> (\<exists>M. \<forall>x. u \<le> x & x \<le> v --> f x \<le> M)" in lemma_BOLZANO2) |
1473 apply safe |
1492 apply safe |
1474 apply simp_all |
1493 apply simp_all |
1475 apply (rename_tac x xa ya M Ma) |
1494 apply (rename_tac x xa ya M Ma) |
1476 apply (cut_tac x = M and y = Ma in linorder_linear, safe) |
1495 apply (cut_tac x = M and y = Ma in linorder_linear, safe) |
1496 lemma lemma_reals_complete: "((\<exists>x. x \<in> S) & (\<exists>y. isUb UNIV S (y::real))) --> |
1515 lemma lemma_reals_complete: "((\<exists>x. x \<in> S) & (\<exists>y. isUb UNIV S (y::real))) --> |
1497 (\<exists>t. isLub UNIV S t)" |
1516 (\<exists>t. isLub UNIV S t)" |
1498 by (blast intro: reals_complete) |
1517 by (blast intro: reals_complete) |
1499 |
1518 |
1500 lemma isCont_has_Ub: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |] |
1519 lemma isCont_has_Ub: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |] |
1501 ==> \<exists>M::real. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) & |
1520 ==> \<exists>M::real. (\<forall>x::real. a \<le> x & x \<le> b --> f(x) \<le> M) & |
1502 (\<forall>N. N < M --> (\<exists>x. a \<le> x & x \<le> b & N < f(x)))" |
1521 (\<forall>N. N < M --> (\<exists>x. a \<le> x & x \<le> b & N < f(x)))" |
1503 apply (cut_tac S = "Collect (%y. \<exists>x. a \<le> x & x \<le> b & y = f x)" |
1522 apply (cut_tac S = "Collect (%y. \<exists>x. a \<le> x & x \<le> b & y = f x)" |
1504 in lemma_reals_complete) |
1523 in lemma_reals_complete) |
1505 apply auto |
1524 apply auto |
1506 apply (drule isCont_bounded, assumption) |
1525 apply (drule isCont_bounded, assumption) |
1511 |
1530 |
1512 text{*Now show that it attains its upper bound*} |
1531 text{*Now show that it attains its upper bound*} |
1513 |
1532 |
1514 lemma isCont_eq_Ub: |
1533 lemma isCont_eq_Ub: |
1515 assumes le: "a \<le> b" |
1534 assumes le: "a \<le> b" |
1516 and con: "\<forall>x. a \<le> x & x \<le> b --> isCont f x" |
1535 and con: "\<forall>x::real. a \<le> x & x \<le> b --> isCont f x" |
1517 shows "\<exists>M::real. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) & |
1536 shows "\<exists>M::real. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) & |
1518 (\<exists>x. a \<le> x & x \<le> b & f(x) = M)" |
1537 (\<exists>x. a \<le> x & x \<le> b & f(x) = M)" |
1519 proof - |
1538 proof - |
1520 from isCont_has_Ub [OF le con] |
1539 from isCont_has_Ub [OF le con] |
1521 obtain M where M1: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M" |
1540 obtain M where M1: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M" |
1552 |
1571 |
1553 |
1572 |
1554 text{*Same theorem for lower bound*} |
1573 text{*Same theorem for lower bound*} |
1555 |
1574 |
1556 lemma isCont_eq_Lb: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |] |
1575 lemma isCont_eq_Lb: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |] |
1557 ==> \<exists>M::real. (\<forall>x. a \<le> x & x \<le> b --> M \<le> f(x)) & |
1576 ==> \<exists>M::real. (\<forall>x::real. a \<le> x & x \<le> b --> M \<le> f(x)) & |
1558 (\<exists>x. a \<le> x & x \<le> b & f(x) = M)" |
1577 (\<exists>x. a \<le> x & x \<le> b & f(x) = M)" |
1559 apply (subgoal_tac "\<forall>x. a \<le> x & x \<le> b --> isCont (%x. - (f x)) x") |
1578 apply (subgoal_tac "\<forall>x. a \<le> x & x \<le> b --> isCont (%x. - (f x)) x") |
1560 prefer 2 apply (blast intro: isCont_minus) |
1579 prefer 2 apply (blast intro: isCont_minus) |
1561 apply (drule_tac f = "(%x. - (f x))" in isCont_eq_Ub) |
1580 apply (drule_tac f = "(%x. - (f x))" in isCont_eq_Ub) |
1562 apply safe |
1581 apply safe |
1565 |
1584 |
1566 |
1585 |
1567 text{*Another version.*} |
1586 text{*Another version.*} |
1568 |
1587 |
1569 lemma isCont_Lb_Ub: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |] |
1588 lemma isCont_Lb_Ub: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |] |
1570 ==> \<exists>L M::real. (\<forall>x. a \<le> x & x \<le> b --> L \<le> f(x) & f(x) \<le> M) & |
1589 ==> \<exists>L M::real. (\<forall>x::real. a \<le> x & x \<le> b --> L \<le> f(x) & f(x) \<le> M) & |
1571 (\<forall>y. L \<le> y & y \<le> M --> (\<exists>x. a \<le> x & x \<le> b & (f(x) = y)))" |
1590 (\<forall>y. L \<le> y & y \<le> M --> (\<exists>x. a \<le> x & x \<le> b & (f(x) = y)))" |
1572 apply (frule isCont_eq_Lb) |
1591 apply (frule isCont_eq_Lb) |
1573 apply (frule_tac [2] isCont_eq_Ub) |
1592 apply (frule_tac [2] isCont_eq_Ub) |
1574 apply (assumption+, safe) |
1593 apply (assumption+, safe) |
1575 apply (rule_tac x = "f x" in exI) |
1594 apply (rule_tac x = "f x" in exI) |
2203 with g'cdef f'cdef cint show ?thesis by auto |
2223 with g'cdef f'cdef cint show ?thesis by auto |
2204 qed |
2224 qed |
2205 |
2225 |
2206 |
2226 |
2207 lemma LIMSEQ_SEQ_conv1: |
2227 lemma LIMSEQ_SEQ_conv1: |
|
2228 fixes a :: real |
2208 assumes "X -- a --> L" |
2229 assumes "X -- a --> L" |
2209 shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" |
2230 shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" |
2210 proof - |
2231 proof - |
2211 { |
2232 { |
2212 from prems have Xdef: "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s --> norm (X x + -L) < r" by (unfold LIM_def) |
2233 from prems have Xdef: "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x + -a) < s --> norm (X x + -L) < r" by (unfold LIM_def) |
2213 |
2234 |
2214 fix S |
2235 fix S |
2215 assume as: "(\<forall>n. S n \<noteq> a) \<and> S ----> a" |
2236 assume as: "(\<forall>n. S n \<noteq> a) \<and> S ----> a" |
2216 then have "S ----> a" by auto |
2237 then have "S ----> a" by auto |
2217 then have Sdef: "(\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (S n + -a) < r))" by (unfold LIMSEQ_def) |
2238 then have Sdef: "(\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (S n + -a) < r))" by (unfold LIMSEQ_def) |
2244 qed |
2265 qed |
2245 |
2266 |
2246 ML {* fast_arith_split_limit := 0; *} (* FIXME *) |
2267 ML {* fast_arith_split_limit := 0; *} (* FIXME *) |
2247 |
2268 |
2248 lemma LIMSEQ_SEQ_conv2: |
2269 lemma LIMSEQ_SEQ_conv2: |
|
2270 fixes a :: real |
2249 assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" |
2271 assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" |
2250 shows "X -- a --> L" |
2272 shows "X -- a --> L" |
2251 proof (rule ccontr) |
2273 proof (rule ccontr) |
2252 assume "\<not> (X -- a --> L)" |
2274 assume "\<not> (X -- a --> L)" |
2253 hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s --> norm (X x + -L) < r)" by (unfold LIM_def) |
2275 hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x + -a) < s --> norm (X x + -L) < r)" by (unfold LIM_def) |
2254 hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. \<not>(x \<noteq> a \<and> \<bar>x + -a\<bar> < s --> norm (X x + -L) < r)" by simp |
2276 hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. \<not>(x \<noteq> a \<and> \<bar>x + -a\<bar> < s --> norm (X x + -L) < r)" by simp |
2255 hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> norm (X x + -L) \<ge> r)" by (simp add: linorder_not_less) |
2277 hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> norm (X x + -L) \<ge> r)" by (simp add: linorder_not_less) |
2256 then obtain r where rdef: "r > 0 \<and> (\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> norm (X x + -L) \<ge> r))" by auto |
2278 then obtain r where rdef: "r > 0 \<and> (\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> norm (X x + -L) \<ge> r))" by auto |
2257 |
2279 |
2258 let ?F = "\<lambda>n::nat. SOME x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> norm (X x + -L) \<ge> r" |
2280 let ?F = "\<lambda>n::nat. SOME x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> norm (X x + -L) \<ge> r" |
2354 assumes "(\<lambda>x. f x) -- a --> L" |
2377 assumes "(\<lambda>x. f x) -- a --> L" |
2355 shows "(\<lambda>x. f (x+c)) -- (a-c) --> L" |
2378 shows "(\<lambda>x. f (x+c)) -- (a-c) --> L" |
2356 proof - |
2379 proof - |
2357 have "f -- a --> L" . |
2380 have "f -- a --> L" . |
2358 hence |
2381 hence |
2359 fd: "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s --> norm (f x + -L) < r" |
2382 fd: "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x + -a) < s --> norm (f x + -L) < r" |
2360 by (unfold LIM_def) |
2383 by (unfold LIM_def) |
2361 { |
2384 { |
2362 fix r::real |
2385 fix r::real |
2363 assume rgz: "0 < r" |
2386 assume rgz: "0 < r" |
2364 with fd have "\<exists>s > 0. \<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s --> norm (f x + -L) < r" by simp |
2387 with fd have "\<exists>s > 0. \<forall>x. x\<noteq>a \<and> norm (x + -a) < s --> norm (f x + -L) < r" by simp |
2365 then obtain s where sgz: "s > 0" and ax: "\<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s \<longrightarrow> norm (f x + -L) < r" by auto |
2388 then obtain s where sgz: "s > 0" and ax: "\<forall>x. x\<noteq>a \<and> norm (x + -a) < s \<longrightarrow> norm (f x + -L) < r" by auto |
2366 from ax have ax2: "\<forall>x. (x+c)\<noteq>a \<and> \<bar>(x+c) + -a\<bar> < s \<longrightarrow> norm (f (x+c) + -L) < r" by auto |
2389 from ax have ax2: "\<forall>x. (x+c)\<noteq>a \<and> norm ((x+c) + -a) < s \<longrightarrow> norm (f (x+c) + -L) < r" by auto |
2367 { |
2390 { |
2368 fix x::real |
2391 fix x |
2369 from ax2 have nt: "(x+c)\<noteq>a \<and> \<bar>(x+c) + -a\<bar> < s \<longrightarrow> norm (f (x+c) + -L) < r" .. |
2392 from ax2 have nt: "(x+c)\<noteq>a \<and> norm ((x+c) + -a) < s \<longrightarrow> norm (f (x+c) + -L) < r" .. |
2370 moreover have "((x+c)\<noteq>a) = (x\<noteq>(a-c))" by auto |
2393 moreover have "((x+c)\<noteq>a) = (x\<noteq>(a-c))" by auto |
2371 moreover have "((x+c) + -a) = (x + -(a-c))" by simp |
2394 moreover have "((x+c) + -a) = (x + -(a-c))" by simp |
2372 ultimately have "x\<noteq>(a-c) \<and> \<bar>x + -(a-c)\<bar> < s \<longrightarrow> norm (f (x+c) + -L) < r" by simp |
2395 ultimately have "x\<noteq>(a-c) \<and> norm (x + -(a-c)) < s \<longrightarrow> norm (f (x+c) + -L) < r" by simp |
2373 } |
2396 } |
2374 then have "\<forall>x. x\<noteq>(a-c) \<and> \<bar>x + -(a-c)\<bar> < s \<longrightarrow> norm (f (x+c) + -L) < r" .. |
2397 then have "\<forall>x. x\<noteq>(a-c) \<and> norm (x + -(a-c)) < s \<longrightarrow> norm (f (x+c) + -L) < r" .. |
2375 with sgz have "\<exists>s > 0. \<forall>x. x\<noteq>(a-c) \<and> \<bar>x + -(a-c)\<bar> < s \<longrightarrow> norm (f (x+c) + -L) < r" by auto |
2398 with sgz have "\<exists>s > 0. \<forall>x. x\<noteq>(a-c) \<and> norm (x + -(a-c)) < s \<longrightarrow> norm (f (x+c) + -L) < r" by auto |
2376 } |
2399 } |
2377 then have |
2400 then have |
2378 "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> (a-c) & \<bar>x + -(a-c)\<bar> < s --> norm (f (x+c) + -L) < r" by simp |
2401 "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> (a-c) & norm (x + -(a-c)) < s --> norm (f (x+c) + -L) < r" by simp |
2379 thus ?thesis by (fold LIM_def) |
2402 thus ?thesis by (fold LIM_def) |
2380 qed |
2403 qed |
2381 |
2404 |
2382 end |
2405 end |