|
1 (* Title: HOL/Nonstandard_Analysis/HLim.thy |
|
2 Author: Jacques D. Fleuriot, University of Cambridge |
|
3 Author: Lawrence C Paulson |
|
4 *) |
|
5 |
|
6 section\<open>Limits and Continuity (Nonstandard)\<close> |
|
7 |
|
8 theory HLim |
|
9 imports Star |
|
10 begin |
|
11 |
|
12 text\<open>Nonstandard Definitions\<close> |
|
13 |
|
14 definition |
|
15 NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool" |
|
16 ("((_)/ \<midarrow>(_)/\<rightarrow>\<^sub>N\<^sub>S (_))" [60, 0, 60] 60) where |
|
17 "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L = |
|
18 (\<forall>x. (x \<noteq> star_of a & x \<approx> star_of a --> ( *f* f) x \<approx> star_of L))" |
|
19 |
|
20 definition |
|
21 isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where |
|
22 \<comment>\<open>NS definition dispenses with limit notions\<close> |
|
23 "isNSCont f a = (\<forall>y. y \<approx> star_of a --> |
|
24 ( *f* f) y \<approx> star_of (f a))" |
|
25 |
|
26 definition |
|
27 isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where |
|
28 "isNSUCont f = (\<forall>x y. x \<approx> y --> ( *f* f) x \<approx> ( *f* f) y)" |
|
29 |
|
30 |
|
31 subsection \<open>Limits of Functions\<close> |
|
32 |
|
33 lemma NSLIM_I: |
|
34 "(\<And>x. \<lbrakk>x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> \<Longrightarrow> starfun f x \<approx> star_of L) |
|
35 \<Longrightarrow> f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L" |
|
36 by (simp add: NSLIM_def) |
|
37 |
|
38 lemma NSLIM_D: |
|
39 "\<lbrakk>f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L; x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> |
|
40 \<Longrightarrow> starfun f x \<approx> star_of L" |
|
41 by (simp add: NSLIM_def) |
|
42 |
|
43 text\<open>Proving properties of limits using nonstandard definition. |
|
44 The properties hold for standard limits as well!\<close> |
|
45 |
|
46 lemma NSLIM_mult: |
|
47 fixes l m :: "'a::real_normed_algebra" |
|
48 shows "[| f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m |] |
|
49 ==> (%x. f(x) * g(x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l * m)" |
|
50 by (auto simp add: NSLIM_def intro!: approx_mult_HFinite) |
|
51 |
|
52 lemma starfun_scaleR [simp]: |
|
53 "starfun (\<lambda>x. f x *\<^sub>R g x) = (\<lambda>x. scaleHR (starfun f x) (starfun g x))" |
|
54 by transfer (rule refl) |
|
55 |
|
56 lemma NSLIM_scaleR: |
|
57 "[| f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m |] |
|
58 ==> (%x. f(x) *\<^sub>R g(x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l *\<^sub>R m)" |
|
59 by (auto simp add: NSLIM_def intro!: approx_scaleR_HFinite) |
|
60 |
|
61 lemma NSLIM_add: |
|
62 "[| f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m |] |
|
63 ==> (%x. f(x) + g(x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l + m)" |
|
64 by (auto simp add: NSLIM_def intro!: approx_add) |
|
65 |
|
66 lemma NSLIM_const [simp]: "(%x. k) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S k" |
|
67 by (simp add: NSLIM_def) |
|
68 |
|
69 lemma NSLIM_minus: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L ==> (%x. -f(x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S -L" |
|
70 by (simp add: NSLIM_def) |
|
71 |
|
72 lemma NSLIM_diff: |
|
73 "\<lbrakk>f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l - m)" |
|
74 by (simp only: NSLIM_add NSLIM_minus diff_conv_add_uminus) |
|
75 |
|
76 lemma NSLIM_add_minus: "[| f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m |] ==> (%x. f(x) + -g(x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l + -m)" |
|
77 by (simp only: NSLIM_add NSLIM_minus) |
|
78 |
|
79 lemma NSLIM_inverse: |
|
80 fixes L :: "'a::real_normed_div_algebra" |
|
81 shows "[| f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L; L \<noteq> 0 |] |
|
82 ==> (%x. inverse(f(x))) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (inverse L)" |
|
83 apply (simp add: NSLIM_def, clarify) |
|
84 apply (drule spec) |
|
85 apply (auto simp add: star_of_approx_inverse) |
|
86 done |
|
87 |
|
88 lemma NSLIM_zero: |
|
89 assumes f: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S l" shows "(%x. f(x) - l) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S 0" |
|
90 proof - |
|
91 have "(\<lambda>x. f x - l) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S l - l" |
|
92 by (rule NSLIM_diff [OF f NSLIM_const]) |
|
93 thus ?thesis by simp |
|
94 qed |
|
95 |
|
96 lemma NSLIM_zero_cancel: "(%x. f(x) - l) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0 ==> f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l" |
|
97 apply (drule_tac g = "%x. l" and m = l in NSLIM_add) |
|
98 apply (auto simp add: add.assoc) |
|
99 done |
|
100 |
|
101 lemma NSLIM_const_not_eq: |
|
102 fixes a :: "'a::real_normed_algebra_1" |
|
103 shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L" |
|
104 apply (simp add: NSLIM_def) |
|
105 apply (rule_tac x="star_of a + of_hypreal \<epsilon>" in exI) |
|
106 apply (simp add: hypreal_epsilon_not_zero approx_def) |
|
107 done |
|
108 |
|
109 lemma NSLIM_not_zero: |
|
110 fixes a :: "'a::real_normed_algebra_1" |
|
111 shows "k \<noteq> 0 \<Longrightarrow> \<not> (\<lambda>x. k) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S 0" |
|
112 by (rule NSLIM_const_not_eq) |
|
113 |
|
114 lemma NSLIM_const_eq: |
|
115 fixes a :: "'a::real_normed_algebra_1" |
|
116 shows "(\<lambda>x. k) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> k = L" |
|
117 apply (rule ccontr) |
|
118 apply (blast dest: NSLIM_const_not_eq) |
|
119 done |
|
120 |
|
121 lemma NSLIM_unique: |
|
122 fixes a :: "'a::real_normed_algebra_1" |
|
123 shows "\<lbrakk>f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L; f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S M\<rbrakk> \<Longrightarrow> L = M" |
|
124 apply (drule (1) NSLIM_diff) |
|
125 apply (auto dest!: NSLIM_const_eq) |
|
126 done |
|
127 |
|
128 lemma NSLIM_mult_zero: |
|
129 fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" |
|
130 shows "[| f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0 |] ==> (%x. f(x)*g(x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0" |
|
131 by (drule NSLIM_mult, auto) |
|
132 |
|
133 lemma NSLIM_self: "(%x. x) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S a" |
|
134 by (simp add: NSLIM_def) |
|
135 |
|
136 subsubsection \<open>Equivalence of @{term filterlim} and @{term NSLIM}\<close> |
|
137 |
|
138 lemma LIM_NSLIM: |
|
139 assumes f: "f \<midarrow>a\<rightarrow> L" shows "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L" |
|
140 proof (rule NSLIM_I) |
|
141 fix x |
|
142 assume neq: "x \<noteq> star_of a" |
|
143 assume approx: "x \<approx> star_of a" |
|
144 have "starfun f x - star_of L \<in> Infinitesimal" |
|
145 proof (rule InfinitesimalI2) |
|
146 fix r::real assume r: "0 < r" |
|
147 from LIM_D [OF f r] |
|
148 obtain s where s: "0 < s" and |
|
149 less_r: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < s\<rbrakk> \<Longrightarrow> norm (f x - L) < r" |
|
150 by fast |
|
151 from less_r have less_r': |
|
152 "\<And>x. \<lbrakk>x \<noteq> star_of a; hnorm (x - star_of a) < star_of s\<rbrakk> |
|
153 \<Longrightarrow> hnorm (starfun f x - star_of L) < star_of r" |
|
154 by transfer |
|
155 from approx have "x - star_of a \<in> Infinitesimal" |
|
156 by (unfold approx_def) |
|
157 hence "hnorm (x - star_of a) < star_of s" |
|
158 using s by (rule InfinitesimalD2) |
|
159 with neq show "hnorm (starfun f x - star_of L) < star_of r" |
|
160 by (rule less_r') |
|
161 qed |
|
162 thus "starfun f x \<approx> star_of L" |
|
163 by (unfold approx_def) |
|
164 qed |
|
165 |
|
166 lemma NSLIM_LIM: |
|
167 assumes f: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L" shows "f \<midarrow>a\<rightarrow> L" |
|
168 proof (rule LIM_I) |
|
169 fix r::real assume r: "0 < r" |
|
170 have "\<exists>s>0. \<forall>x. x \<noteq> star_of a \<and> hnorm (x - star_of a) < s |
|
171 \<longrightarrow> hnorm (starfun f x - star_of L) < star_of r" |
|
172 proof (rule exI, safe) |
|
173 show "0 < \<epsilon>" by (rule hypreal_epsilon_gt_zero) |
|
174 next |
|
175 fix x assume neq: "x \<noteq> star_of a" |
|
176 assume "hnorm (x - star_of a) < \<epsilon>" |
|
177 with Infinitesimal_epsilon |
|
178 have "x - star_of a \<in> Infinitesimal" |
|
179 by (rule hnorm_less_Infinitesimal) |
|
180 hence "x \<approx> star_of a" |
|
181 by (unfold approx_def) |
|
182 with f neq have "starfun f x \<approx> star_of L" |
|
183 by (rule NSLIM_D) |
|
184 hence "starfun f x - star_of L \<in> Infinitesimal" |
|
185 by (unfold approx_def) |
|
186 thus "hnorm (starfun f x - star_of L) < star_of r" |
|
187 using r by (rule InfinitesimalD2) |
|
188 qed |
|
189 thus "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x - L) < r" |
|
190 by transfer |
|
191 qed |
|
192 |
|
193 theorem LIM_NSLIM_iff: "(f \<midarrow>x\<rightarrow> L) = (f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S L)" |
|
194 by (blast intro: LIM_NSLIM NSLIM_LIM) |
|
195 |
|
196 |
|
197 subsection \<open>Continuity\<close> |
|
198 |
|
199 lemma isNSContD: |
|
200 "\<lbrakk>isNSCont f a; y \<approx> star_of a\<rbrakk> \<Longrightarrow> ( *f* f) y \<approx> star_of (f a)" |
|
201 by (simp add: isNSCont_def) |
|
202 |
|
203 lemma isNSCont_NSLIM: "isNSCont f a ==> f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (f a) " |
|
204 by (simp add: isNSCont_def NSLIM_def) |
|
205 |
|
206 lemma NSLIM_isNSCont: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (f a) ==> isNSCont f a" |
|
207 apply (simp add: isNSCont_def NSLIM_def, auto) |
|
208 apply (case_tac "y = star_of a", auto) |
|
209 done |
|
210 |
|
211 text\<open>NS continuity can be defined using NS Limit in |
|
212 similar fashion to standard def of continuity\<close> |
|
213 lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (f a))" |
|
214 by (blast intro: isNSCont_NSLIM NSLIM_isNSCont) |
|
215 |
|
216 text\<open>Hence, NS continuity can be given |
|
217 in terms of standard limit\<close> |
|
218 lemma isNSCont_LIM_iff: "(isNSCont f a) = (f \<midarrow>a\<rightarrow> (f a))" |
|
219 by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff) |
|
220 |
|
221 text\<open>Moreover, it's trivial now that NS continuity |
|
222 is equivalent to standard continuity\<close> |
|
223 lemma isNSCont_isCont_iff: "(isNSCont f a) = (isCont f a)" |
|
224 apply (simp add: isCont_def) |
|
225 apply (rule isNSCont_LIM_iff) |
|
226 done |
|
227 |
|
228 text\<open>Standard continuity ==> NS continuity\<close> |
|
229 lemma isCont_isNSCont: "isCont f a ==> isNSCont f a" |
|
230 by (erule isNSCont_isCont_iff [THEN iffD2]) |
|
231 |
|
232 text\<open>NS continuity ==> Standard continuity\<close> |
|
233 lemma isNSCont_isCont: "isNSCont f a ==> isCont f a" |
|
234 by (erule isNSCont_isCont_iff [THEN iffD1]) |
|
235 |
|
236 text\<open>Alternative definition of continuity\<close> |
|
237 |
|
238 (* Prove equivalence between NS limits - *) |
|
239 (* seems easier than using standard def *) |
|
240 lemma NSLIM_h_iff: "(f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L) = ((%h. f(a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S L)" |
|
241 apply (simp add: NSLIM_def, auto) |
|
242 apply (drule_tac x = "star_of a + x" in spec) |
|
243 apply (drule_tac [2] x = "- star_of a + x" in spec, safe, simp) |
|
244 apply (erule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]]) |
|
245 apply (erule_tac [3] approx_minus_iff2 [THEN iffD1]) |
|
246 prefer 2 apply (simp add: add.commute) |
|
247 apply (rule_tac x = x in star_cases) |
|
248 apply (rule_tac [2] x = x in star_cases) |
|
249 apply (auto simp add: starfun star_of_def star_n_minus star_n_add add.assoc star_n_zero_num) |
|
250 done |
|
251 |
|
252 lemma NSLIM_isCont_iff: "(f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S f a) = ((%h. f(a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S f a)" |
|
253 by (fact NSLIM_h_iff) |
|
254 |
|
255 lemma isNSCont_minus: "isNSCont f a ==> isNSCont (%x. - f x) a" |
|
256 by (simp add: isNSCont_def) |
|
257 |
|
258 lemma isNSCont_inverse: |
|
259 fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra" |
|
260 shows "[| isNSCont f x; f x \<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x" |
|
261 by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff) |
|
262 |
|
263 lemma isNSCont_const [simp]: "isNSCont (%x. k) a" |
|
264 by (simp add: isNSCont_def) |
|
265 |
|
266 lemma isNSCont_abs [simp]: "isNSCont abs (a::real)" |
|
267 apply (simp add: isNSCont_def) |
|
268 apply (auto intro: approx_hrabs simp add: starfun_rabs_hrabs) |
|
269 done |
|
270 |
|
271 |
|
272 subsection \<open>Uniform Continuity\<close> |
|
273 |
|
274 lemma isNSUContD: "[| isNSUCont f; x \<approx> y|] ==> ( *f* f) x \<approx> ( *f* f) y" |
|
275 by (simp add: isNSUCont_def) |
|
276 |
|
277 lemma isUCont_isNSUCont: |
|
278 fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
|
279 assumes f: "isUCont f" shows "isNSUCont f" |
|
280 proof (unfold isNSUCont_def, safe) |
|
281 fix x y :: "'a star" |
|
282 assume approx: "x \<approx> y" |
|
283 have "starfun f x - starfun f y \<in> Infinitesimal" |
|
284 proof (rule InfinitesimalI2) |
|
285 fix r::real assume r: "0 < r" |
|
286 with f obtain s where s: "0 < s" and |
|
287 less_r: "\<And>x y. norm (x - y) < s \<Longrightarrow> norm (f x - f y) < r" |
|
288 by (auto simp add: isUCont_def dist_norm) |
|
289 from less_r have less_r': |
|
290 "\<And>x y. hnorm (x - y) < star_of s |
|
291 \<Longrightarrow> hnorm (starfun f x - starfun f y) < star_of r" |
|
292 by transfer |
|
293 from approx have "x - y \<in> Infinitesimal" |
|
294 by (unfold approx_def) |
|
295 hence "hnorm (x - y) < star_of s" |
|
296 using s by (rule InfinitesimalD2) |
|
297 thus "hnorm (starfun f x - starfun f y) < star_of r" |
|
298 by (rule less_r') |
|
299 qed |
|
300 thus "starfun f x \<approx> starfun f y" |
|
301 by (unfold approx_def) |
|
302 qed |
|
303 |
|
304 lemma isNSUCont_isUCont: |
|
305 fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
|
306 assumes f: "isNSUCont f" shows "isUCont f" |
|
307 proof (unfold isUCont_def dist_norm, safe) |
|
308 fix r::real assume r: "0 < r" |
|
309 have "\<exists>s>0. \<forall>x y. hnorm (x - y) < s |
|
310 \<longrightarrow> hnorm (starfun f x - starfun f y) < star_of r" |
|
311 proof (rule exI, safe) |
|
312 show "0 < \<epsilon>" by (rule hypreal_epsilon_gt_zero) |
|
313 next |
|
314 fix x y :: "'a star" |
|
315 assume "hnorm (x - y) < \<epsilon>" |
|
316 with Infinitesimal_epsilon |
|
317 have "x - y \<in> Infinitesimal" |
|
318 by (rule hnorm_less_Infinitesimal) |
|
319 hence "x \<approx> y" |
|
320 by (unfold approx_def) |
|
321 with f have "starfun f x \<approx> starfun f y" |
|
322 by (simp add: isNSUCont_def) |
|
323 hence "starfun f x - starfun f y \<in> Infinitesimal" |
|
324 by (unfold approx_def) |
|
325 thus "hnorm (starfun f x - starfun f y) < star_of r" |
|
326 using r by (rule InfinitesimalD2) |
|
327 qed |
|
328 thus "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r" |
|
329 by transfer |
|
330 qed |
|
331 |
|
332 end |