author | paulson |
Mon, 04 Oct 2004 15:28:03 +0200 | |
changeset 15228 | 4d332d10fa3d |
parent 15140 | 322485b816ac |
child 15234 | ec91a90c604e |
permissions | -rw-r--r-- |
13957 | 1 |
(* Title : CLim.thy |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 2001 University of Edinburgh |
|
14469 | 4 |
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
13957 | 5 |
*) |
6 |
||
14469 | 7 |
header{*Limits, Continuity and Differentiation for Complex Functions*} |
8 |
||
15131 | 9 |
theory CLim |
15140 | 10 |
imports CSeries |
15131 | 11 |
begin |
14405 | 12 |
|
13 |
(*not in simpset?*) |
|
14 |
declare hypreal_epsilon_not_zero [simp] |
|
15 |
||
16 |
(*??generalize*) |
|
17 |
lemma lemma_complex_mult_inverse_squared [simp]: |
|
18 |
"x \<noteq> (0::complex) \<Longrightarrow> (x * inverse(x) ^ 2) = inverse x" |
|
14469 | 19 |
by (simp add: numeral_2_eq_2) |
14405 | 20 |
|
21 |
text{*Changing the quantified variable. Install earlier?*} |
|
14738 | 22 |
lemma all_shift: "(\<forall>x::'a::comm_ring_1. P x) = (\<forall>x. P (x-a))"; |
14405 | 23 |
apply auto |
24 |
apply (drule_tac x="x+a" in spec) |
|
25 |
apply (simp add: diff_minus add_assoc) |
|
26 |
done |
|
27 |
||
28 |
lemma complex_add_minus_iff [simp]: "(x + - a = (0::complex)) = (x=a)" |
|
29 |
by (simp add: diff_eq_eq diff_minus [symmetric]) |
|
30 |
||
31 |
lemma complex_add_eq_0_iff [iff]: "(x+y = (0::complex)) = (y = -x)" |
|
32 |
apply auto |
|
33 |
apply (drule sym [THEN diff_eq_eq [THEN iffD2]], auto) |
|
34 |
done |
|
13957 | 35 |
|
36 |
constdefs |
|
37 |
||
14405 | 38 |
CLIM :: "[complex=>complex,complex,complex] => bool" |
13957 | 39 |
("((_)/ -- (_)/ --C> (_))" [60, 0, 60] 60) |
40 |
"f -- a --C> L == |
|
14405 | 41 |
\<forall>r. 0 < r --> |
42 |
(\<exists>s. 0 < s & (\<forall>x. (x \<noteq> a & (cmod(x - a) < s) |
|
13957 | 43 |
--> cmod(f x - L) < r)))" |
44 |
||
14405 | 45 |
NSCLIM :: "[complex=>complex,complex,complex] => bool" |
13957 | 46 |
("((_)/ -- (_)/ --NSC> (_))" [60, 0, 60] 60) |
14405 | 47 |
"f -- a --NSC> L == (\<forall>x. (x \<noteq> hcomplex_of_complex a & |
48 |
x @c= hcomplex_of_complex a |
|
49 |
--> ( *fc* f) x @c= hcomplex_of_complex L))" |
|
13957 | 50 |
|
51 |
(* f: C --> R *) |
|
14405 | 52 |
CRLIM :: "[complex=>real,complex,real] => bool" |
13957 | 53 |
("((_)/ -- (_)/ --CR> (_))" [60, 0, 60] 60) |
54 |
"f -- a --CR> L == |
|
14405 | 55 |
\<forall>r. 0 < r --> |
56 |
(\<exists>s. 0 < s & (\<forall>x. (x \<noteq> a & (cmod(x - a) < s) |
|
13957 | 57 |
--> abs(f x - L) < r)))" |
58 |
||
14405 | 59 |
NSCRLIM :: "[complex=>real,complex,real] => bool" |
13957 | 60 |
("((_)/ -- (_)/ --NSCR> (_))" [60, 0, 60] 60) |
14405 | 61 |
"f -- a --NSCR> L == (\<forall>x. (x \<noteq> hcomplex_of_complex a & |
62 |
x @c= hcomplex_of_complex a |
|
63 |
--> ( *fcR* f) x @= hypreal_of_real L))" |
|
13957 | 64 |
|
65 |
||
14405 | 66 |
isContc :: "[complex=>complex,complex] => bool" |
67 |
"isContc f a == (f -- a --C> (f a))" |
|
13957 | 68 |
|
69 |
(* NS definition dispenses with limit notions *) |
|
14405 | 70 |
isNSContc :: "[complex=>complex,complex] => bool" |
71 |
"isNSContc f a == (\<forall>y. y @c= hcomplex_of_complex a --> |
|
13957 | 72 |
( *fc* f) y @c= hcomplex_of_complex (f a))" |
73 |
||
14405 | 74 |
isContCR :: "[complex=>real,complex] => bool" |
75 |
"isContCR f a == (f -- a --CR> (f a))" |
|
13957 | 76 |
|
77 |
(* NS definition dispenses with limit notions *) |
|
14405 | 78 |
isNSContCR :: "[complex=>real,complex] => bool" |
79 |
"isNSContCR f a == (\<forall>y. y @c= hcomplex_of_complex a --> |
|
13957 | 80 |
( *fcR* f) y @= hypreal_of_real (f a))" |
81 |
||
82 |
(* differentiation: D is derivative of function f at x *) |
|
14405 | 83 |
cderiv:: "[complex=>complex,complex,complex] => bool" |
13957 | 84 |
("(CDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60) |
85 |
"CDERIV f x :> D == ((%h. (f(x + h) - f(x))/h) -- 0 --C> D)" |
|
86 |
||
14405 | 87 |
nscderiv :: "[complex=>complex,complex,complex] => bool" |
13957 | 88 |
("(NSCDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60) |
14405 | 89 |
"NSCDERIV f x :> D == (\<forall>h \<in> CInfinitesimal - {0}. |
13957 | 90 |
(( *fc* f)(hcomplex_of_complex x + h) |
91 |
- hcomplex_of_complex (f x))/h @c= hcomplex_of_complex D)" |
|
92 |
||
14405 | 93 |
cdifferentiable :: "[complex=>complex,complex] => bool" |
94 |
(infixl "cdifferentiable" 60) |
|
95 |
"f cdifferentiable x == (\<exists>D. CDERIV f x :> D)" |
|
96 |
||
97 |
NSCdifferentiable :: "[complex=>complex,complex] => bool" |
|
98 |
(infixl "NSCdifferentiable" 60) |
|
99 |
"f NSCdifferentiable x == (\<exists>D. NSCDERIV f x :> D)" |
|
100 |
||
101 |
||
102 |
isUContc :: "(complex=>complex) => bool" |
|
103 |
"isUContc f == (\<forall>r. 0 < r --> |
|
104 |
(\<exists>s. 0 < s & (\<forall>x y. cmod(x - y) < s |
|
105 |
--> cmod(f x - f y) < r)))" |
|
106 |
||
107 |
isNSUContc :: "(complex=>complex) => bool" |
|
108 |
"isNSUContc f == (\<forall>x y. x @c= y --> ( *fc* f) x @c= ( *fc* f) y)" |
|
109 |
||
110 |
||
111 |
||
112 |
subsection{*Limit of Complex to Complex Function*} |
|
113 |
||
114 |
lemma NSCLIM_NSCRLIM_Re: "f -- a --NSC> L ==> (%x. Re(f x)) -- a --NSCR> Re(L)" |
|
14469 | 115 |
by (simp add: NSCLIM_def NSCRLIM_def starfunC_approx_Re_Im_iff |
116 |
hRe_hcomplex_of_complex) |
|
117 |
||
14405 | 118 |
|
14469 | 119 |
lemma NSCLIM_NSCRLIM_Im: "f -- a --NSC> L ==> (%x. Im(f x)) -- a --NSCR> Im(L)" |
120 |
by (simp add: NSCLIM_def NSCRLIM_def starfunC_approx_Re_Im_iff |
|
121 |
hIm_hcomplex_of_complex) |
|
14405 | 122 |
|
123 |
lemma CLIM_NSCLIM: |
|
124 |
"f -- x --C> L ==> f -- x --NSC> L" |
|
14469 | 125 |
apply (simp add: CLIM_def NSCLIM_def capprox_def, auto) |
14405 | 126 |
apply (rule_tac z = xa in eq_Abs_hcomplex) |
127 |
apply (auto simp add: hcomplex_of_complex_def starfunC hcomplex_diff |
|
128 |
CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff) |
|
129 |
apply (rule bexI, rule_tac [2] lemma_hyprel_refl, safe) |
|
130 |
apply (drule_tac x = u in spec, auto) |
|
131 |
apply (drule_tac x = s in spec, auto, ultra) |
|
132 |
apply (drule sym, auto) |
|
133 |
done |
|
134 |
||
135 |
lemma eq_Abs_hcomplex_ALL: |
|
136 |
"(\<forall>t. P t) = (\<forall>X. P (Abs_hcomplex(hcomplexrel `` {X})))" |
|
137 |
apply auto |
|
138 |
apply (rule_tac z = t in eq_Abs_hcomplex, auto) |
|
139 |
done |
|
140 |
||
141 |
lemma lemma_CLIM: |
|
142 |
"\<forall>s. 0 < s --> (\<exists>xa. xa \<noteq> x & |
|
143 |
cmod (xa - x) < s & r \<le> cmod (f xa - L)) |
|
144 |
==> \<forall>(n::nat). \<exists>xa. xa \<noteq> x & |
|
145 |
cmod(xa - x) < inverse(real(Suc n)) & r \<le> cmod(f xa - L)" |
|
146 |
apply clarify |
|
147 |
apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto) |
|
148 |
done |
|
149 |
||
150 |
||
151 |
lemma lemma_skolemize_CLIM2: |
|
152 |
"\<forall>s. 0 < s --> (\<exists>xa. xa \<noteq> x & |
|
153 |
cmod (xa - x) < s & r \<le> cmod (f xa - L)) |
|
154 |
==> \<exists>X. \<forall>(n::nat). X n \<noteq> x & |
|
155 |
cmod(X n - x) < inverse(real(Suc n)) & r \<le> cmod(f (X n) - L)" |
|
156 |
apply (drule lemma_CLIM) |
|
157 |
apply (drule choice, blast) |
|
158 |
done |
|
159 |
||
160 |
lemma lemma_csimp: |
|
161 |
"\<forall>n. X n \<noteq> x & |
|
162 |
cmod (X n - x) < inverse (real(Suc n)) & |
|
163 |
r \<le> cmod (f (X n) - L) ==> |
|
164 |
\<forall>n. cmod (X n - x) < inverse (real(Suc n))" |
|
165 |
by auto |
|
166 |
||
167 |
lemma NSCLIM_CLIM: |
|
168 |
"f -- x --NSC> L ==> f -- x --C> L" |
|
14469 | 169 |
apply (simp add: CLIM_def NSCLIM_def) |
14405 | 170 |
apply (rule ccontr) |
14469 | 171 |
apply (auto simp add: eq_Abs_hcomplex_ALL starfunC |
172 |
CInfinitesimal_capprox_minus [symmetric] hcomplex_diff |
|
173 |
CInfinitesimal_hcmod_iff hcomplex_of_complex_def |
|
174 |
Infinitesimal_FreeUltrafilterNat_iff hcmod) |
|
14405 | 175 |
apply (simp add: linorder_not_less) |
176 |
apply (drule lemma_skolemize_CLIM2, safe) |
|
177 |
apply (drule_tac x = X in spec, auto) |
|
178 |
apply (drule lemma_csimp [THEN complex_seq_to_hcomplex_CInfinitesimal]) |
|
14469 | 179 |
apply (simp add: CInfinitesimal_hcmod_iff hcomplex_of_complex_def |
180 |
Infinitesimal_FreeUltrafilterNat_iff hcomplex_diff hcmod, blast) |
|
14405 | 181 |
apply (drule_tac x = r in spec, clarify) |
182 |
apply (drule FreeUltrafilterNat_all, ultra, arith) |
|
183 |
done |
|
184 |
||
185 |
||
186 |
text{*First key result*} |
|
187 |
theorem CLIM_NSCLIM_iff: "(f -- x --C> L) = (f -- x --NSC> L)" |
|
188 |
by (blast intro: CLIM_NSCLIM NSCLIM_CLIM) |
|
189 |
||
190 |
||
191 |
subsection{*Limit of Complex to Real Function*} |
|
192 |
||
193 |
lemma CRLIM_NSCRLIM: "f -- x --CR> L ==> f -- x --NSCR> L" |
|
14469 | 194 |
apply (simp add: CRLIM_def NSCRLIM_def capprox_def, auto) |
14405 | 195 |
apply (rule_tac z = xa in eq_Abs_hcomplex) |
14469 | 196 |
apply (auto simp add: hcomplex_of_complex_def starfunCR hcomplex_diff |
197 |
CInfinitesimal_hcmod_iff hcmod hypreal_diff |
|
198 |
Infinitesimal_FreeUltrafilterNat_iff |
|
199 |
Infinitesimal_approx_minus [symmetric] hypreal_of_real_def) |
|
14405 | 200 |
apply (rule bexI, rule_tac [2] lemma_hyprel_refl, safe) |
201 |
apply (drule_tac x = u in spec, auto) |
|
202 |
apply (drule_tac x = s in spec, auto, ultra) |
|
203 |
apply (drule sym, auto) |
|
204 |
done |
|
205 |
||
206 |
lemma lemma_CRLIM: |
|
207 |
"\<forall>s. 0 < s --> (\<exists>xa. xa \<noteq> x & |
|
208 |
cmod (xa - x) < s & r \<le> abs (f xa - L)) |
|
209 |
==> \<forall>(n::nat). \<exists>xa. xa \<noteq> x & |
|
210 |
cmod(xa - x) < inverse(real(Suc n)) & r \<le> abs (f xa - L)" |
|
211 |
apply clarify |
|
212 |
apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto) |
|
213 |
done |
|
214 |
||
215 |
lemma lemma_skolemize_CRLIM2: |
|
216 |
"\<forall>s. 0 < s --> (\<exists>xa. xa \<noteq> x & |
|
217 |
cmod (xa - x) < s & r \<le> abs (f xa - L)) |
|
218 |
==> \<exists>X. \<forall>(n::nat). X n \<noteq> x & |
|
219 |
cmod(X n - x) < inverse(real(Suc n)) & r \<le> abs (f (X n) - L)" |
|
220 |
apply (drule lemma_CRLIM) |
|
221 |
apply (drule choice, blast) |
|
222 |
done |
|
223 |
||
224 |
lemma lemma_crsimp: |
|
225 |
"\<forall>n. X n \<noteq> x & |
|
226 |
cmod (X n - x) < inverse (real(Suc n)) & |
|
227 |
r \<le> abs (f (X n) - L) ==> |
|
228 |
\<forall>n. cmod (X n - x) < inverse (real(Suc n))" |
|
229 |
by auto |
|
230 |
||
231 |
lemma NSCRLIM_CRLIM: "f -- x --NSCR> L ==> f -- x --CR> L" |
|
14469 | 232 |
apply (simp add: CRLIM_def NSCRLIM_def capprox_def) |
14405 | 233 |
apply (rule ccontr) |
234 |
apply (auto simp add: eq_Abs_hcomplex_ALL starfunCR hcomplex_diff |
|
235 |
hcomplex_of_complex_def hypreal_diff CInfinitesimal_hcmod_iff |
|
236 |
hcmod Infinitesimal_approx_minus [symmetric] |
|
237 |
Infinitesimal_FreeUltrafilterNat_iff) |
|
238 |
apply (simp add: linorder_not_less) |
|
239 |
apply (drule lemma_skolemize_CRLIM2, safe) |
|
240 |
apply (drule_tac x = X in spec, auto) |
|
241 |
apply (drule lemma_crsimp [THEN complex_seq_to_hcomplex_CInfinitesimal]) |
|
242 |
apply (simp add: CInfinitesimal_hcmod_iff hcomplex_of_complex_def |
|
243 |
Infinitesimal_FreeUltrafilterNat_iff hcomplex_diff hcmod) |
|
244 |
apply (auto simp add: hypreal_of_real_def hypreal_diff) |
|
245 |
apply (drule_tac x = r in spec, clarify) |
|
246 |
apply (drule FreeUltrafilterNat_all, ultra) |
|
247 |
done |
|
248 |
||
249 |
text{*Second key result*} |
|
250 |
theorem CRLIM_NSCRLIM_iff: "(f -- x --CR> L) = (f -- x --NSCR> L)" |
|
251 |
by (blast intro: CRLIM_NSCRLIM NSCRLIM_CRLIM) |
|
252 |
||
253 |
(** get this result easily now **) |
|
254 |
lemma CLIM_CRLIM_Re: "f -- a --C> L ==> (%x. Re(f x)) -- a --CR> Re(L)" |
|
255 |
by (auto dest: NSCLIM_NSCRLIM_Re simp add: CLIM_NSCLIM_iff CRLIM_NSCRLIM_iff [symmetric]) |
|
256 |
||
257 |
lemma CLIM_CRLIM_Im: "f -- a --C> L ==> (%x. Im(f x)) -- a --CR> Im(L)" |
|
258 |
by (auto dest: NSCLIM_NSCRLIM_Im simp add: CLIM_NSCLIM_iff CRLIM_NSCRLIM_iff [symmetric]) |
|
259 |
||
260 |
lemma CLIM_cnj: "f -- a --C> L ==> (%x. cnj (f x)) -- a --C> cnj L" |
|
14469 | 261 |
by (simp add: CLIM_def complex_cnj_diff [symmetric]) |
14405 | 262 |
|
263 |
lemma CLIM_cnj_iff: "((%x. cnj (f x)) -- a --C> cnj L) = (f -- a --C> L)" |
|
14469 | 264 |
by (simp add: CLIM_def complex_cnj_diff [symmetric]) |
14405 | 265 |
|
266 |
(*** NSLIM_add hence CLIM_add *) |
|
267 |
||
268 |
lemma NSCLIM_add: |
|
269 |
"[| f -- x --NSC> l; g -- x --NSC> m |] |
|
270 |
==> (%x. f(x) + g(x)) -- x --NSC> (l + m)" |
|
271 |
by (auto simp: NSCLIM_def intro!: capprox_add) |
|
272 |
||
273 |
lemma CLIM_add: |
|
274 |
"[| f -- x --C> l; g -- x --C> m |] |
|
275 |
==> (%x. f(x) + g(x)) -- x --C> (l + m)" |
|
276 |
by (simp add: CLIM_NSCLIM_iff NSCLIM_add) |
|
277 |
||
278 |
(*** NSLIM_mult hence CLIM_mult *) |
|
279 |
||
280 |
lemma NSCLIM_mult: |
|
281 |
"[| f -- x --NSC> l; g -- x --NSC> m |] |
|
282 |
==> (%x. f(x) * g(x)) -- x --NSC> (l * m)" |
|
283 |
by (auto simp add: NSCLIM_def intro!: capprox_mult_CFinite) |
|
284 |
||
285 |
lemma CLIM_mult: |
|
286 |
"[| f -- x --C> l; g -- x --C> m |] |
|
287 |
==> (%x. f(x) * g(x)) -- x --C> (l * m)" |
|
288 |
by (simp add: CLIM_NSCLIM_iff NSCLIM_mult) |
|
289 |
||
290 |
(*** NSCLIM_const and CLIM_const ***) |
|
291 |
||
292 |
lemma NSCLIM_const [simp]: "(%x. k) -- x --NSC> k" |
|
293 |
by (simp add: NSCLIM_def) |
|
294 |
||
295 |
lemma CLIM_const [simp]: "(%x. k) -- x --C> k" |
|
296 |
by (simp add: CLIM_def) |
|
297 |
||
298 |
(*** NSCLIM_minus and CLIM_minus ***) |
|
299 |
||
300 |
lemma NSCLIM_minus: "f -- a --NSC> L ==> (%x. -f(x)) -- a --NSC> -L" |
|
301 |
by (simp add: NSCLIM_def) |
|
302 |
||
303 |
lemma CLIM_minus: "f -- a --C> L ==> (%x. -f(x)) -- a --C> -L" |
|
304 |
by (simp add: CLIM_NSCLIM_iff NSCLIM_minus) |
|
305 |
||
306 |
(*** NSCLIM_diff hence CLIM_diff ***) |
|
307 |
||
308 |
lemma NSCLIM_diff: |
|
309 |
"[| f -- x --NSC> l; g -- x --NSC> m |] |
|
310 |
==> (%x. f(x) - g(x)) -- x --NSC> (l - m)" |
|
14469 | 311 |
by (simp add: diff_minus NSCLIM_add NSCLIM_minus) |
14405 | 312 |
|
313 |
lemma CLIM_diff: |
|
314 |
"[| f -- x --C> l; g -- x --C> m |] |
|
315 |
==> (%x. f(x) - g(x)) -- x --C> (l - m)" |
|
316 |
by (simp add: CLIM_NSCLIM_iff NSCLIM_diff) |
|
317 |
||
318 |
(*** NSCLIM_inverse and hence CLIM_inverse *) |
|
319 |
||
320 |
lemma NSCLIM_inverse: |
|
321 |
"[| f -- a --NSC> L; L \<noteq> 0 |] |
|
322 |
==> (%x. inverse(f(x))) -- a --NSC> (inverse L)" |
|
14469 | 323 |
apply (simp add: NSCLIM_def, clarify) |
14405 | 324 |
apply (drule spec) |
14469 | 325 |
apply (force simp add: hcomplex_of_complex_capprox_inverse) |
14405 | 326 |
done |
327 |
||
328 |
lemma CLIM_inverse: |
|
329 |
"[| f -- a --C> L; L \<noteq> 0 |] |
|
330 |
==> (%x. inverse(f(x))) -- a --C> (inverse L)" |
|
331 |
by (simp add: CLIM_NSCLIM_iff NSCLIM_inverse) |
|
332 |
||
333 |
(*** NSCLIM_zero, CLIM_zero, etc. ***) |
|
334 |
||
335 |
lemma NSCLIM_zero: "f -- a --NSC> l ==> (%x. f(x) - l) -- a --NSC> 0" |
|
14469 | 336 |
apply (simp add: diff_minus) |
14405 | 337 |
apply (rule_tac a1 = l in right_minus [THEN subst]) |
14469 | 338 |
apply (rule NSCLIM_add, auto) |
14405 | 339 |
done |
340 |
||
341 |
lemma CLIM_zero: "f -- a --C> l ==> (%x. f(x) - l) -- a --C> 0" |
|
342 |
by (simp add: CLIM_NSCLIM_iff NSCLIM_zero) |
|
343 |
||
344 |
lemma NSCLIM_zero_cancel: "(%x. f(x) - l) -- x --NSC> 0 ==> f -- x --NSC> l" |
|
345 |
by (drule_tac g = "%x. l" and m = l in NSCLIM_add, auto) |
|
346 |
||
347 |
lemma CLIM_zero_cancel: "(%x. f(x) - l) -- x --C> 0 ==> f -- x --C> l" |
|
348 |
by (drule_tac g = "%x. l" and m = l in CLIM_add, auto) |
|
349 |
||
350 |
(*** NSCLIM_not zero and hence CLIM_not_zero ***) |
|
13957 | 351 |
|
14405 | 352 |
lemma NSCLIM_not_zero: "k \<noteq> 0 ==> ~ ((%x. k) -- x --NSC> 0)" |
353 |
apply (auto simp del: hcomplex_of_complex_zero simp add: NSCLIM_def) |
|
354 |
apply (rule_tac x = "hcomplex_of_complex x + hcomplex_of_hypreal epsilon" in exI) |
|
355 |
apply (auto intro: CInfinitesimal_add_capprox_self [THEN capprox_sym] |
|
356 |
simp del: hcomplex_of_complex_zero) |
|
357 |
done |
|
358 |
||
359 |
(* [| k \<noteq> 0; (%x. k) -- x --NSC> 0 |] ==> R *) |
|
360 |
lemmas NSCLIM_not_zeroE = NSCLIM_not_zero [THEN notE, standard] |
|
361 |
||
362 |
lemma CLIM_not_zero: "k \<noteq> 0 ==> ~ ((%x. k) -- x --C> 0)" |
|
363 |
by (simp add: CLIM_NSCLIM_iff NSCLIM_not_zero) |
|
364 |
||
365 |
(*** NSCLIM_const hence CLIM_const ***) |
|
366 |
||
367 |
lemma NSCLIM_const_eq: "(%x. k) -- x --NSC> L ==> k = L" |
|
368 |
apply (rule ccontr) |
|
369 |
apply (drule NSCLIM_zero) |
|
370 |
apply (rule NSCLIM_not_zeroE [of "k-L"], auto) |
|
371 |
done |
|
372 |
||
373 |
lemma CLIM_const_eq: "(%x. k) -- x --C> L ==> k = L" |
|
374 |
by (simp add: CLIM_NSCLIM_iff NSCLIM_const_eq) |
|
375 |
||
376 |
(*** NSCLIM and hence CLIM are unique ***) |
|
377 |
||
378 |
lemma NSCLIM_unique: "[| f -- x --NSC> L; f -- x --NSC> M |] ==> L = M" |
|
379 |
apply (drule NSCLIM_minus) |
|
380 |
apply (drule NSCLIM_add, assumption) |
|
381 |
apply (auto dest!: NSCLIM_const_eq [symmetric]) |
|
382 |
done |
|
383 |
||
384 |
lemma CLIM_unique: "[| f -- x --C> L; f -- x --C> M |] ==> L = M" |
|
385 |
by (simp add: CLIM_NSCLIM_iff NSCLIM_unique) |
|
386 |
||
387 |
(*** NSCLIM_mult_zero and CLIM_mult_zero ***) |
|
388 |
||
389 |
lemma NSCLIM_mult_zero: |
|
390 |
"[| f -- x --NSC> 0; g -- x --NSC> 0 |] ==> (%x. f(x)*g(x)) -- x --NSC> 0" |
|
391 |
by (drule NSCLIM_mult, auto) |
|
392 |
||
393 |
lemma CLIM_mult_zero: |
|
394 |
"[| f -- x --C> 0; g -- x --C> 0 |] ==> (%x. f(x)*g(x)) -- x --C> 0" |
|
395 |
by (drule CLIM_mult, auto) |
|
396 |
||
397 |
(*** NSCLIM_self hence CLIM_self ***) |
|
398 |
||
399 |
lemma NSCLIM_self: "(%x. x) -- a --NSC> a" |
|
400 |
by (auto simp add: NSCLIM_def intro: starfunC_Idfun_capprox) |
|
401 |
||
402 |
lemma CLIM_self: "(%x. x) -- a --C> a" |
|
403 |
by (simp add: CLIM_NSCLIM_iff NSCLIM_self) |
|
404 |
||
405 |
(** another equivalence result **) |
|
406 |
lemma NSCLIM_NSCRLIM_iff: |
|
407 |
"(f -- x --NSC> L) = ((%y. cmod(f y - L)) -- x --NSCR> 0)" |
|
408 |
apply (auto simp add: NSCLIM_def NSCRLIM_def CInfinitesimal_capprox_minus [symmetric] CInfinitesimal_hcmod_iff) |
|
409 |
apply (auto dest!: spec) |
|
410 |
apply (rule_tac [!] z = xa in eq_Abs_hcomplex) |
|
411 |
apply (auto simp add: hcomplex_diff starfunC starfunCR hcomplex_of_complex_def hcmod mem_infmal_iff) |
|
412 |
done |
|
413 |
||
414 |
(** much, much easier standard proof **) |
|
415 |
lemma CLIM_CRLIM_iff: "(f -- x --C> L) = ((%y. cmod(f y - L)) -- x --CR> 0)" |
|
416 |
by (simp add: CLIM_def CRLIM_def) |
|
417 |
||
418 |
(* so this is nicer nonstandard proof *) |
|
419 |
lemma NSCLIM_NSCRLIM_iff2: |
|
420 |
"(f -- x --NSC> L) = ((%y. cmod(f y - L)) -- x --NSCR> 0)" |
|
14469 | 421 |
by (simp add: CRLIM_NSCRLIM_iff [symmetric] CLIM_CRLIM_iff CLIM_NSCLIM_iff [symmetric]) |
14405 | 422 |
|
423 |
lemma NSCLIM_NSCRLIM_Re_Im_iff: |
|
424 |
"(f -- a --NSC> L) = ((%x. Re(f x)) -- a --NSCR> Re(L) & |
|
425 |
(%x. Im(f x)) -- a --NSCR> Im(L))" |
|
426 |
apply (auto intro: NSCLIM_NSCRLIM_Re NSCLIM_NSCRLIM_Im) |
|
427 |
apply (auto simp add: NSCLIM_def NSCRLIM_def) |
|
428 |
apply (auto dest!: spec) |
|
429 |
apply (rule_tac z = x in eq_Abs_hcomplex) |
|
14469 | 430 |
apply (simp add: capprox_approx_iff starfunC hcomplex_of_complex_def starfunCR hypreal_of_real_def) |
14405 | 431 |
done |
432 |
||
433 |
lemma CLIM_CRLIM_Re_Im_iff: |
|
434 |
"(f -- a --C> L) = ((%x. Re(f x)) -- a --CR> Re(L) & |
|
435 |
(%x. Im(f x)) -- a --CR> Im(L))" |
|
436 |
by (simp add: CLIM_NSCLIM_iff CRLIM_NSCRLIM_iff NSCLIM_NSCRLIM_Re_Im_iff) |
|
437 |
||
438 |
||
439 |
subsection{*Continuity*} |
|
440 |
||
441 |
lemma isNSContcD: |
|
442 |
"[| isNSContc f a; y @c= hcomplex_of_complex a |] |
|
443 |
==> ( *fc* f) y @c= hcomplex_of_complex (f a)" |
|
444 |
by (simp add: isNSContc_def) |
|
445 |
||
446 |
lemma isNSContc_NSCLIM: "isNSContc f a ==> f -- a --NSC> (f a) " |
|
447 |
by (simp add: isNSContc_def NSCLIM_def) |
|
448 |
||
449 |
lemma NSCLIM_isNSContc: |
|
450 |
"f -- a --NSC> (f a) ==> isNSContc f a" |
|
451 |
apply (simp add: isNSContc_def NSCLIM_def, auto) |
|
452 |
apply (case_tac "y = hcomplex_of_complex a", auto) |
|
453 |
done |
|
454 |
||
455 |
text{*Nonstandard continuity can be defined using NS Limit in |
|
456 |
similar fashion to standard definition of continuity*} |
|
457 |
||
458 |
lemma isNSContc_NSCLIM_iff: "(isNSContc f a) = (f -- a --NSC> (f a))" |
|
459 |
by (blast intro: isNSContc_NSCLIM NSCLIM_isNSContc) |
|
460 |
||
461 |
lemma isNSContc_CLIM_iff: "(isNSContc f a) = (f -- a --C> (f a))" |
|
462 |
by (simp add: CLIM_NSCLIM_iff isNSContc_NSCLIM_iff) |
|
463 |
||
464 |
(*** key result for continuity ***) |
|
465 |
lemma isNSContc_isContc_iff: "(isNSContc f a) = (isContc f a)" |
|
466 |
by (simp add: isContc_def isNSContc_CLIM_iff) |
|
467 |
||
468 |
lemma isContc_isNSContc: "isContc f a ==> isNSContc f a" |
|
469 |
by (erule isNSContc_isContc_iff [THEN iffD2]) |
|
470 |
||
471 |
lemma isNSContc_isContc: "isNSContc f a ==> isContc f a" |
|
472 |
by (erule isNSContc_isContc_iff [THEN iffD1]) |
|
473 |
||
474 |
||
475 |
text{*Alternative definition of continuity*} |
|
476 |
lemma NSCLIM_h_iff: "(f -- a --NSC> L) = ((%h. f(a + h)) -- 0 --NSC> L)" |
|
477 |
apply (simp add: NSCLIM_def, auto) |
|
478 |
apply (drule_tac x = "hcomplex_of_complex a + x" in spec) |
|
479 |
apply (drule_tac [2] x = "- hcomplex_of_complex a + x" in spec, safe, simp) |
|
480 |
apply (rule mem_cinfmal_iff [THEN iffD2, THEN CInfinitesimal_add_capprox_self [THEN capprox_sym]]) |
|
481 |
apply (rule_tac [4] capprox_minus_iff2 [THEN iffD1]) |
|
482 |
prefer 3 apply (simp add: compare_rls hcomplex_add_commute) |
|
483 |
apply (rule_tac [2] z = x in eq_Abs_hcomplex) |
|
484 |
apply (rule_tac [4] z = x in eq_Abs_hcomplex) |
|
485 |
apply (auto simp add: starfunC hcomplex_of_complex_def hcomplex_minus hcomplex_add) |
|
486 |
done |
|
487 |
||
488 |
lemma NSCLIM_isContc_iff: |
|
489 |
"(f -- a --NSC> f a) = ((%h. f(a + h)) -- 0 --NSC> f a)" |
|
490 |
by (rule NSCLIM_h_iff) |
|
491 |
||
492 |
lemma CLIM_isContc_iff: "(f -- a --C> f a) = ((%h. f(a + h)) -- 0 --C> f(a))" |
|
493 |
by (simp add: CLIM_NSCLIM_iff NSCLIM_isContc_iff) |
|
494 |
||
495 |
lemma isContc_iff: "(isContc f x) = ((%h. f(x + h)) -- 0 --C> f(x))" |
|
496 |
by (simp add: isContc_def CLIM_isContc_iff) |
|
497 |
||
498 |
lemma isContc_add: |
|
499 |
"[| isContc f a; isContc g a |] ==> isContc (%x. f(x) + g(x)) a" |
|
500 |
by (auto intro: capprox_add simp add: isNSContc_isContc_iff [symmetric] isNSContc_def) |
|
501 |
||
502 |
lemma isContc_mult: |
|
503 |
"[| isContc f a; isContc g a |] ==> isContc (%x. f(x) * g(x)) a" |
|
504 |
by (auto intro!: starfunC_mult_CFinite_capprox |
|
505 |
simp del: starfunC_mult [symmetric] |
|
506 |
simp add: isNSContc_isContc_iff [symmetric] isNSContc_def) |
|
507 |
||
508 |
||
509 |
lemma isContc_o: "[| isContc f a; isContc g (f a) |] ==> isContc (g o f) a" |
|
14469 | 510 |
by (simp add: isNSContc_isContc_iff [symmetric] isNSContc_def starfunC_o [symmetric]) |
14405 | 511 |
|
512 |
lemma isContc_o2: |
|
513 |
"[| isContc f a; isContc g (f a) |] ==> isContc (%x. g (f x)) a" |
|
514 |
by (auto dest: isContc_o simp add: o_def) |
|
515 |
||
516 |
lemma isNSContc_minus: "isNSContc f a ==> isNSContc (%x. - f x) a" |
|
517 |
by (simp add: isNSContc_def) |
|
518 |
||
519 |
lemma isContc_minus: "isContc f a ==> isContc (%x. - f x) a" |
|
520 |
by (simp add: isNSContc_isContc_iff [symmetric] isNSContc_minus) |
|
521 |
||
522 |
lemma isContc_inverse: |
|
523 |
"[| isContc f x; f x \<noteq> 0 |] ==> isContc (%x. inverse (f x)) x" |
|
524 |
by (simp add: isContc_def CLIM_inverse) |
|
525 |
||
526 |
lemma isNSContc_inverse: |
|
527 |
"[| isNSContc f x; f x \<noteq> 0 |] ==> isNSContc (%x. inverse (f x)) x" |
|
528 |
by (auto intro: isContc_inverse simp add: isNSContc_isContc_iff) |
|
529 |
||
530 |
lemma isContc_diff: |
|
531 |
"[| isContc f a; isContc g a |] ==> isContc (%x. f(x) - g(x)) a" |
|
14469 | 532 |
apply (simp add: diff_minus) |
14405 | 533 |
apply (auto intro: isContc_add isContc_minus) |
534 |
done |
|
535 |
||
536 |
lemma isContc_const [simp]: "isContc (%x. k) a" |
|
537 |
by (simp add: isContc_def) |
|
538 |
||
539 |
lemma isNSContc_const [simp]: "isNSContc (%x. k) a" |
|
540 |
by (simp add: isNSContc_def) |
|
541 |
||
542 |
||
543 |
subsection{*Functions from Complex to Reals*} |
|
544 |
||
545 |
lemma isNSContCRD: |
|
546 |
"[| isNSContCR f a; y @c= hcomplex_of_complex a |] |
|
547 |
==> ( *fcR* f) y @= hypreal_of_real (f a)" |
|
548 |
by (simp add: isNSContCR_def) |
|
549 |
||
550 |
lemma isNSContCR_NSCRLIM: "isNSContCR f a ==> f -- a --NSCR> (f a) " |
|
551 |
by (simp add: isNSContCR_def NSCRLIM_def) |
|
552 |
||
553 |
lemma NSCRLIM_isNSContCR: "f -- a --NSCR> (f a) ==> isNSContCR f a" |
|
554 |
apply (auto simp add: isNSContCR_def NSCRLIM_def) |
|
555 |
apply (case_tac "y = hcomplex_of_complex a", auto) |
|
556 |
done |
|
557 |
||
558 |
lemma isNSContCR_NSCRLIM_iff: "(isNSContCR f a) = (f -- a --NSCR> (f a))" |
|
559 |
by (blast intro: isNSContCR_NSCRLIM NSCRLIM_isNSContCR) |
|
560 |
||
561 |
lemma isNSContCR_CRLIM_iff: "(isNSContCR f a) = (f -- a --CR> (f a))" |
|
562 |
by (simp add: CRLIM_NSCRLIM_iff isNSContCR_NSCRLIM_iff) |
|
563 |
||
564 |
(*** another key result for continuity ***) |
|
565 |
lemma isNSContCR_isContCR_iff: "(isNSContCR f a) = (isContCR f a)" |
|
566 |
by (simp add: isContCR_def isNSContCR_CRLIM_iff) |
|
567 |
||
568 |
lemma isContCR_isNSContCR: "isContCR f a ==> isNSContCR f a" |
|
569 |
by (erule isNSContCR_isContCR_iff [THEN iffD2]) |
|
570 |
||
571 |
lemma isNSContCR_isContCR: "isNSContCR f a ==> isContCR f a" |
|
572 |
by (erule isNSContCR_isContCR_iff [THEN iffD1]) |
|
573 |
||
574 |
lemma isNSContCR_cmod [simp]: "isNSContCR cmod (a)" |
|
575 |
by (auto intro: capprox_hcmod_approx |
|
576 |
simp add: starfunCR_cmod hcmod_hcomplex_of_complex [symmetric] |
|
577 |
isNSContCR_def) |
|
578 |
||
579 |
lemma isContCR_cmod [simp]: "isContCR cmod (a)" |
|
14469 | 580 |
by (simp add: isNSContCR_isContCR_iff [symmetric]) |
14405 | 581 |
|
582 |
lemma isContc_isContCR_Re: "isContc f a ==> isContCR (%x. Re (f x)) a" |
|
583 |
by (simp add: isContc_def isContCR_def CLIM_CRLIM_Re) |
|
584 |
||
585 |
lemma isContc_isContCR_Im: "isContc f a ==> isContCR (%x. Im (f x)) a" |
|
586 |
by (simp add: isContc_def isContCR_def CLIM_CRLIM_Im) |
|
587 |
||
588 |
||
589 |
subsection{*Derivatives*} |
|
590 |
||
591 |
lemma CDERIV_iff: "(CDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --C> D)" |
|
592 |
by (simp add: cderiv_def) |
|
593 |
||
594 |
lemma CDERIV_NSC_iff: |
|
595 |
"(CDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NSC> D)" |
|
596 |
by (simp add: cderiv_def CLIM_NSCLIM_iff) |
|
597 |
||
598 |
lemma CDERIVD: "CDERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --C> D" |
|
599 |
by (simp add: cderiv_def) |
|
600 |
||
601 |
lemma NSC_DERIVD: "CDERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --NSC> D" |
|
602 |
by (simp add: cderiv_def CLIM_NSCLIM_iff) |
|
603 |
||
604 |
text{*Uniqueness*} |
|
605 |
lemma CDERIV_unique: "[| CDERIV f x :> D; CDERIV f x :> E |] ==> D = E" |
|
606 |
by (simp add: cderiv_def CLIM_unique) |
|
607 |
||
608 |
(*** uniqueness: a nonstandard proof ***) |
|
609 |
lemma NSCDeriv_unique: "[| NSCDERIV f x :> D; NSCDERIV f x :> E |] ==> D = E" |
|
610 |
apply (simp add: nscderiv_def) |
|
611 |
apply (auto dest!: bspec [where x = "hcomplex_of_hypreal epsilon"] |
|
612 |
intro!: inj_hcomplex_of_complex [THEN injD] dest: capprox_trans3) |
|
613 |
done |
|
13957 | 614 |
|
615 |
||
14405 | 616 |
subsection{* Differentiability*} |
617 |
||
618 |
lemma CDERIV_CLIM_iff: |
|
619 |
"((%h. (f(a + h) - f(a))/h) -- 0 --C> D) = |
|
620 |
((%x. (f(x) - f(a)) / (x - a)) -- a --C> D)" |
|
621 |
apply (simp add: CLIM_def) |
|
622 |
apply (rule_tac f=All in arg_cong) |
|
623 |
apply (rule ext) |
|
624 |
apply (rule imp_cong) |
|
625 |
apply (rule refl) |
|
626 |
apply (rule_tac f=Ex in arg_cong) |
|
627 |
apply (rule ext) |
|
628 |
apply (rule conj_cong) |
|
629 |
apply (rule refl) |
|
630 |
apply (rule trans) |
|
631 |
apply (rule all_shift [where a=a], simp) |
|
632 |
done |
|
633 |
||
634 |
lemma CDERIV_iff2: |
|
635 |
"(CDERIV f x :> D) = ((%z. (f(z) - f(x)) / (z - x)) -- x --C> D)" |
|
636 |
by (simp add: cderiv_def CDERIV_CLIM_iff) |
|
637 |
||
638 |
||
639 |
subsection{* Equivalence of NS and Standard Differentiation*} |
|
640 |
||
641 |
(*** first equivalence ***) |
|
642 |
lemma NSCDERIV_NSCLIM_iff: |
|
643 |
"(NSCDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NSC> D)" |
|
644 |
apply (simp add: nscderiv_def NSCLIM_def, auto) |
|
645 |
apply (drule_tac x = xa in bspec) |
|
646 |
apply (rule_tac [3] ccontr) |
|
647 |
apply (drule_tac [3] x = h in spec) |
|
648 |
apply (auto simp add: mem_cinfmal_iff starfunC_lambda_cancel) |
|
649 |
done |
|
650 |
||
651 |
(*** 2nd equivalence ***) |
|
652 |
lemma NSCDERIV_NSCLIM_iff2: |
|
653 |
"(NSCDERIV f x :> D) = ((%z. (f(z) - f(x)) / (z - x)) -- x --NSC> D)" |
|
654 |
by (simp add: NSCDERIV_NSCLIM_iff CDERIV_CLIM_iff CLIM_NSCLIM_iff [symmetric]) |
|
655 |
||
656 |
lemma NSCDERIV_iff2: |
|
657 |
"(NSCDERIV f x :> D) = |
|
658 |
(\<forall>xa. xa \<noteq> hcomplex_of_complex x & xa @c= hcomplex_of_complex x --> |
|
659 |
( *fc* (%z. (f z - f x) / (z - x))) xa @c= hcomplex_of_complex D)" |
|
660 |
by (simp add: NSCDERIV_NSCLIM_iff2 NSCLIM_def) |
|
661 |
||
662 |
lemma NSCDERIV_CDERIV_iff: "(NSCDERIV f x :> D) = (CDERIV f x :> D)" |
|
663 |
by (simp add: cderiv_def NSCDERIV_NSCLIM_iff CLIM_NSCLIM_iff) |
|
664 |
||
665 |
lemma NSCDERIV_isNSContc: "NSCDERIV f x :> D ==> isNSContc f x" |
|
666 |
apply (auto simp add: nscderiv_def isNSContc_NSCLIM_iff NSCLIM_def diff_minus) |
|
667 |
apply (drule capprox_minus_iff [THEN iffD1]) |
|
668 |
apply (subgoal_tac "xa + - (hcomplex_of_complex x) \<noteq> 0") |
|
669 |
prefer 2 apply (simp add: compare_rls) |
|
670 |
apply (drule_tac x = "- hcomplex_of_complex x + xa" in bspec) |
|
15013 | 671 |
prefer 2 apply (simp add: add_assoc [symmetric]) |
672 |
apply (auto simp add: mem_cinfmal_iff [symmetric] add_commute) |
|
14405 | 673 |
apply (drule_tac c = "xa + - hcomplex_of_complex x" in capprox_mult1) |
674 |
apply (auto intro: CInfinitesimal_subset_CFinite [THEN subsetD] |
|
675 |
simp add: mult_assoc) |
|
676 |
apply (drule_tac x3 = D in |
|
677 |
CFinite_hcomplex_of_complex [THEN [2] CInfinitesimal_CFinite_mult, |
|
678 |
THEN mem_cinfmal_iff [THEN iffD1]]) |
|
679 |
apply (blast intro: capprox_trans mult_commute [THEN subst] capprox_minus_iff [THEN iffD2]) |
|
680 |
done |
|
681 |
||
682 |
lemma CDERIV_isContc: "CDERIV f x :> D ==> isContc f x" |
|
683 |
by (simp add: NSCDERIV_CDERIV_iff [symmetric] isNSContc_isContc_iff [symmetric] NSCDERIV_isNSContc) |
|
684 |
||
685 |
text{* Differentiation rules for combinations of functions follow by clear, |
|
686 |
straightforard algebraic manipulations*} |
|
687 |
||
688 |
(* use simple constant nslimit theorem *) |
|
689 |
lemma NSCDERIV_const [simp]: "(NSCDERIV (%x. k) x :> 0)" |
|
690 |
by (simp add: NSCDERIV_NSCLIM_iff) |
|
691 |
||
692 |
lemma CDERIV_const [simp]: "(CDERIV (%x. k) x :> 0)" |
|
693 |
by (simp add: NSCDERIV_CDERIV_iff [symmetric]) |
|
694 |
||
695 |
lemma NSCDERIV_add: |
|
696 |
"[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |] |
|
697 |
==> NSCDERIV (%x. f x + g x) x :> Da + Db" |
|
698 |
apply (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def, clarify) |
|
699 |
apply (auto dest!: spec simp add: add_divide_distrib diff_minus) |
|
700 |
apply (drule_tac b = "hcomplex_of_complex Da" and d = "hcomplex_of_complex Db" in capprox_add) |
|
701 |
apply (auto simp add: add_ac) |
|
702 |
done |
|
703 |
||
704 |
lemma CDERIV_add: |
|
705 |
"[| CDERIV f x :> Da; CDERIV g x :> Db |] |
|
706 |
==> CDERIV (%x. f x + g x) x :> Da + Db" |
|
707 |
by (simp add: NSCDERIV_add NSCDERIV_CDERIV_iff [symmetric]) |
|
708 |
||
709 |
||
710 |
subsection{*Lemmas for Multiplication*} |
|
711 |
||
712 |
lemma lemma_nscderiv1: "((a::hcomplex)*b) - (c*d) = (b*(a - c)) + (c*(b - d))" |
|
713 |
by (simp add: right_diff_distrib) |
|
714 |
||
715 |
lemma lemma_nscderiv2: |
|
716 |
"[| (x + y) / z = hcomplex_of_complex D + yb; z \<noteq> 0; |
|
717 |
z : CInfinitesimal; yb : CInfinitesimal |] |
|
718 |
==> x + y @c= 0" |
|
719 |
apply (frule_tac c1 = z in hcomplex_mult_right_cancel [THEN iffD2], assumption) |
|
720 |
apply (erule_tac V = " (x + y) / z = hcomplex_of_complex D + yb" in thin_rl) |
|
721 |
apply (auto intro!: CInfinitesimal_CFinite_mult2 CFinite_add |
|
722 |
simp add: mem_cinfmal_iff [symmetric]) |
|
723 |
apply (erule CInfinitesimal_subset_CFinite [THEN subsetD]) |
|
724 |
done |
|
725 |
||
726 |
lemma NSCDERIV_mult: |
|
727 |
"[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |] |
|
728 |
==> NSCDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))" |
|
729 |
apply (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def, clarify) |
|
730 |
apply (auto dest!: spec |
|
731 |
simp add: starfunC_lambda_cancel lemma_nscderiv1) |
|
732 |
apply (simp (no_asm) add: add_divide_distrib) |
|
733 |
apply (drule bex_CInfinitesimal_iff2 [THEN iffD2])+ |
|
734 |
apply (auto simp del: times_divide_eq_right simp add: times_divide_eq_right [symmetric]) |
|
735 |
apply (simp add: diff_minus) |
|
736 |
apply (drule_tac D = Db in lemma_nscderiv2) |
|
737 |
apply (drule_tac [4] |
|
738 |
capprox_minus_iff [THEN iffD2, THEN bex_CInfinitesimal_iff2 [THEN iffD2]]) |
|
739 |
apply (auto intro!: capprox_add_mono1 simp add: left_distrib right_distrib mult_commute add_assoc) |
|
740 |
apply (rule_tac b1 = "hcomplex_of_complex Db * hcomplex_of_complex (f x) " in add_commute [THEN subst]) |
|
741 |
apply (auto intro!: CInfinitesimal_add_capprox_self2 [THEN capprox_sym] |
|
742 |
CInfinitesimal_add CInfinitesimal_mult |
|
743 |
CInfinitesimal_hcomplex_of_complex_mult |
|
744 |
CInfinitesimal_hcomplex_of_complex_mult2 |
|
15013 | 745 |
simp add: add_assoc [symmetric]) |
14405 | 746 |
done |
747 |
||
748 |
lemma CDERIV_mult: |
|
749 |
"[| CDERIV f x :> Da; CDERIV g x :> Db |] |
|
750 |
==> CDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))" |
|
751 |
by (simp add: NSCDERIV_mult NSCDERIV_CDERIV_iff [symmetric]) |
|
752 |
||
753 |
lemma NSCDERIV_cmult: "NSCDERIV f x :> D ==> NSCDERIV (%x. c * f x) x :> c*D" |
|
754 |
apply (simp add: times_divide_eq_right [symmetric] NSCDERIV_NSCLIM_iff |
|
14469 | 755 |
minus_mult_right right_distrib [symmetric] diff_minus |
14405 | 756 |
del: times_divide_eq_right minus_mult_right [symmetric]) |
757 |
apply (erule NSCLIM_const [THEN NSCLIM_mult]) |
|
758 |
done |
|
759 |
||
760 |
lemma CDERIV_cmult: "CDERIV f x :> D ==> CDERIV (%x. c * f x) x :> c*D" |
|
761 |
by (simp add: NSCDERIV_cmult NSCDERIV_CDERIV_iff [symmetric]) |
|
762 |
||
763 |
lemma NSCDERIV_minus: "NSCDERIV f x :> D ==> NSCDERIV (%x. -(f x)) x :> -D" |
|
14469 | 764 |
apply (simp add: NSCDERIV_NSCLIM_iff diff_minus) |
14405 | 765 |
apply (rule_tac t = "f x" in minus_minus [THEN subst]) |
766 |
apply (simp (no_asm_simp) add: minus_add_distrib [symmetric] |
|
767 |
del: minus_add_distrib minus_minus) |
|
768 |
apply (erule NSCLIM_minus) |
|
769 |
done |
|
770 |
||
771 |
lemma CDERIV_minus: "CDERIV f x :> D ==> CDERIV (%x. -(f x)) x :> -D" |
|
772 |
by (simp add: NSCDERIV_minus NSCDERIV_CDERIV_iff [symmetric]) |
|
773 |
||
774 |
lemma NSCDERIV_add_minus: |
|
775 |
"[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |] |
|
776 |
==> NSCDERIV (%x. f x + -g x) x :> Da + -Db" |
|
777 |
by (blast dest: NSCDERIV_add NSCDERIV_minus) |
|
778 |
||
779 |
lemma CDERIV_add_minus: |
|
780 |
"[| CDERIV f x :> Da; CDERIV g x :> Db |] |
|
781 |
==> CDERIV (%x. f x + -g x) x :> Da + -Db" |
|
782 |
by (blast dest: CDERIV_add CDERIV_minus) |
|
783 |
||
784 |
lemma NSCDERIV_diff: |
|
785 |
"[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |] |
|
786 |
==> NSCDERIV (%x. f x - g x) x :> Da - Db" |
|
14469 | 787 |
by (simp add: diff_minus NSCDERIV_add_minus) |
14405 | 788 |
|
789 |
lemma CDERIV_diff: |
|
790 |
"[| CDERIV f x :> Da; CDERIV g x :> Db |] |
|
791 |
==> CDERIV (%x. f x - g x) x :> Da - Db" |
|
14469 | 792 |
by (simp add: diff_minus CDERIV_add_minus) |
14405 | 793 |
|
794 |
||
795 |
subsection{*Chain Rule*} |
|
796 |
||
797 |
(* lemmas *) |
|
798 |
lemma NSCDERIV_zero: |
|
799 |
"[| NSCDERIV g x :> D; |
|
800 |
( *fc* g) (hcomplex_of_complex(x) + xa) = hcomplex_of_complex(g x); |
|
801 |
xa : CInfinitesimal; xa \<noteq> 0 |
|
802 |
|] ==> D = 0" |
|
803 |
apply (simp add: nscderiv_def) |
|
804 |
apply (drule bspec, auto) |
|
805 |
done |
|
806 |
||
807 |
lemma NSCDERIV_capprox: |
|
808 |
"[| NSCDERIV f x :> D; h: CInfinitesimal; h \<noteq> 0 |] |
|
809 |
==> ( *fc* f) (hcomplex_of_complex(x) + h) - hcomplex_of_complex(f x) @c= 0" |
|
810 |
apply (simp add: nscderiv_def mem_cinfmal_iff [symmetric]) |
|
811 |
apply (rule CInfinitesimal_ratio) |
|
812 |
apply (rule_tac [3] capprox_hcomplex_of_complex_CFinite, auto) |
|
813 |
done |
|
814 |
||
815 |
||
816 |
(*--------------------------------------------------*) |
|
817 |
(* from one version of differentiability *) |
|
818 |
(* *) |
|
819 |
(* f(x) - f(a) *) |
|
820 |
(* --------------- @= Db *) |
|
821 |
(* x - a *) |
|
822 |
(* -------------------------------------------------*) |
|
823 |
||
824 |
lemma NSCDERIVD1: |
|
825 |
"[| NSCDERIV f (g x) :> Da; |
|
826 |
( *fc* g) (hcomplex_of_complex(x) + xa) \<noteq> hcomplex_of_complex (g x); |
|
827 |
( *fc* g) (hcomplex_of_complex(x) + xa) @c= hcomplex_of_complex (g x)|] |
|
828 |
==> (( *fc* f) (( *fc* g) (hcomplex_of_complex(x) + xa)) |
|
829 |
- hcomplex_of_complex (f (g x))) / |
|
830 |
(( *fc* g) (hcomplex_of_complex(x) + xa) - hcomplex_of_complex (g x)) |
|
831 |
@c= hcomplex_of_complex (Da)" |
|
14469 | 832 |
by (simp add: NSCDERIV_NSCLIM_iff2 NSCLIM_def) |
14405 | 833 |
|
834 |
(*--------------------------------------------------*) |
|
835 |
(* from other version of differentiability *) |
|
836 |
(* *) |
|
837 |
(* f(x + h) - f(x) *) |
|
838 |
(* ----------------- @= Db *) |
|
839 |
(* h *) |
|
840 |
(*--------------------------------------------------*) |
|
841 |
||
842 |
lemma NSCDERIVD2: |
|
843 |
"[| NSCDERIV g x :> Db; xa: CInfinitesimal; xa \<noteq> 0 |] |
|
844 |
==> (( *fc* g) (hcomplex_of_complex x + xa) - hcomplex_of_complex(g x)) / xa |
|
845 |
@c= hcomplex_of_complex (Db)" |
|
14469 | 846 |
by (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def mem_cinfmal_iff starfunC_lambda_cancel) |
14405 | 847 |
|
848 |
lemma lemma_complex_chain: "(z::hcomplex) \<noteq> 0 ==> x*y = (x*inverse(z))*(z*y)" |
|
849 |
by auto |
|
850 |
||
851 |
||
852 |
text{*Chain rule*} |
|
853 |
theorem NSCDERIV_chain: |
|
854 |
"[| NSCDERIV f (g x) :> Da; NSCDERIV g x :> Db |] |
|
855 |
==> NSCDERIV (f o g) x :> Da * Db" |
|
856 |
apply (simp (no_asm_simp) add: NSCDERIV_NSCLIM_iff NSCLIM_def mem_cinfmal_iff [symmetric]) |
|
857 |
apply safe |
|
858 |
apply (frule_tac f = g in NSCDERIV_capprox) |
|
859 |
apply (auto simp add: starfunC_lambda_cancel2 starfunC_o [symmetric]) |
|
860 |
apply (case_tac "( *fc* g) (hcomplex_of_complex (x) + xa) = hcomplex_of_complex (g x) ") |
|
861 |
apply (drule_tac g = g in NSCDERIV_zero) |
|
862 |
apply (auto simp add: hcomplex_divide_def) |
|
863 |
apply (rule_tac z1 = "( *fc* g) (hcomplex_of_complex (x) + xa) - hcomplex_of_complex (g x) " and y1 = "inverse xa" in lemma_complex_chain [THEN ssubst]) |
|
864 |
apply (simp (no_asm_simp)) |
|
865 |
apply (rule capprox_mult_hcomplex_of_complex) |
|
866 |
apply (auto intro!: NSCDERIVD1 intro: capprox_minus_iff [THEN iffD2] |
|
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14405
diff
changeset
|
867 |
simp add: diff_minus [symmetric] divide_inverse [symmetric]) |
14405 | 868 |
apply (blast intro: NSCDERIVD2) |
869 |
done |
|
870 |
||
871 |
text{*standard version*} |
|
872 |
lemma CDERIV_chain: |
|
873 |
"[| CDERIV f (g x) :> Da; CDERIV g x :> Db |] |
|
874 |
==> CDERIV (f o g) x :> Da * Db" |
|
875 |
by (simp add: NSCDERIV_CDERIV_iff [symmetric] NSCDERIV_chain) |
|
876 |
||
877 |
lemma CDERIV_chain2: |
|
878 |
"[| CDERIV f (g x) :> Da; CDERIV g x :> Db |] |
|
879 |
==> CDERIV (%x. f (g x)) x :> Da * Db" |
|
880 |
by (auto dest: CDERIV_chain simp add: o_def) |
|
881 |
||
882 |
||
883 |
subsection{* Differentiation of Natural Number Powers*} |
|
884 |
||
885 |
lemma NSCDERIV_Id [simp]: "NSCDERIV (%x. x) x :> 1" |
|
15228 | 886 |
by (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def divide_self del: divide_self_if) |
14405 | 887 |
|
888 |
lemma CDERIV_Id [simp]: "CDERIV (%x. x) x :> 1" |
|
889 |
by (simp add: NSCDERIV_CDERIV_iff [symmetric]) |
|
890 |
||
891 |
lemmas isContc_Id = CDERIV_Id [THEN CDERIV_isContc, standard] |
|
13957 | 892 |
|
14405 | 893 |
text{*derivative of linear multiplication*} |
894 |
lemma CDERIV_cmult_Id [simp]: "CDERIV (op * c) x :> c" |
|
895 |
by (cut_tac c = c and x = x in CDERIV_Id [THEN CDERIV_cmult], simp) |
|
896 |
||
897 |
lemma NSCDERIV_cmult_Id [simp]: "NSCDERIV (op * c) x :> c" |
|
898 |
by (simp add: NSCDERIV_CDERIV_iff) |
|
899 |
||
900 |
lemma CDERIV_pow [simp]: |
|
901 |
"CDERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))" |
|
902 |
apply (induct_tac "n") |
|
903 |
apply (drule_tac [2] CDERIV_Id [THEN CDERIV_mult]) |
|
15013 | 904 |
apply (auto simp add: left_distrib real_of_nat_Suc) |
14405 | 905 |
apply (case_tac "n") |
906 |
apply (auto simp add: mult_ac add_commute) |
|
907 |
done |
|
908 |
||
909 |
text{*Nonstandard version*} |
|
910 |
lemma NSCDERIV_pow: |
|
911 |
"NSCDERIV (%x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))" |
|
912 |
by (simp add: NSCDERIV_CDERIV_iff) |
|
913 |
||
914 |
lemma lemma_CDERIV_subst: |
|
915 |
"[|CDERIV f x :> D; D = E|] ==> CDERIV f x :> E" |
|
916 |
by auto |
|
917 |
||
918 |
(*used once, in NSCDERIV_inverse*) |
|
919 |
lemma CInfinitesimal_add_not_zero: |
|
920 |
"[| h: CInfinitesimal; x \<noteq> 0 |] ==> hcomplex_of_complex x + h \<noteq> 0" |
|
921 |
apply clarify |
|
922 |
apply (drule equals_zero_I, auto) |
|
923 |
done |
|
924 |
||
925 |
text{*Can't relax the premise @{term "x \<noteq> 0"}: it isn't continuous at zero*} |
|
926 |
lemma NSCDERIV_inverse: |
|
927 |
"x \<noteq> 0 ==> NSCDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))" |
|
928 |
apply (simp add: nscderiv_def Ball_def, clarify) |
|
929 |
apply (frule CInfinitesimal_add_not_zero [where x=x]) |
|
14469 | 930 |
apply (auto simp add: starfunC_inverse_inverse diff_minus |
14405 | 931 |
simp del: minus_mult_left [symmetric] minus_mult_right [symmetric]) |
932 |
apply (simp add: hcomplex_add_commute numeral_2_eq_2 inverse_add |
|
933 |
inverse_mult_distrib [symmetric] inverse_minus_eq [symmetric] |
|
934 |
add_ac mult_ac |
|
15013 | 935 |
del: inverse_minus_eq inverse_mult_distrib |
936 |
minus_mult_right [symmetric] minus_mult_left [symmetric]) |
|
14405 | 937 |
apply (simp only: mult_assoc [symmetric] right_distrib) |
938 |
apply (rule_tac y = " inverse (- hcomplex_of_complex x * hcomplex_of_complex x) " in capprox_trans) |
|
939 |
apply (rule inverse_add_CInfinitesimal_capprox2) |
|
940 |
apply (auto dest!: hcomplex_of_complex_CFinite_diff_CInfinitesimal |
|
941 |
intro: CFinite_mult |
|
942 |
simp add: inverse_minus_eq [symmetric]) |
|
943 |
apply (rule CInfinitesimal_CFinite_mult2, auto) |
|
944 |
done |
|
945 |
||
946 |
lemma CDERIV_inverse: |
|
947 |
"x \<noteq> 0 ==> CDERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))" |
|
948 |
by (simp add: NSCDERIV_inverse NSCDERIV_CDERIV_iff [symmetric] |
|
949 |
del: complexpow_Suc) |
|
950 |
||
951 |
||
952 |
subsection{*Derivative of Reciprocals (Function @{term inverse})*} |
|
953 |
||
954 |
lemma CDERIV_inverse_fun: |
|
955 |
"[| CDERIV f x :> d; f(x) \<noteq> 0 |] |
|
956 |
==> CDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))" |
|
957 |
apply (rule mult_commute [THEN subst]) |
|
15013 | 958 |
apply (simp add: minus_mult_left power_inverse |
959 |
del: complexpow_Suc minus_mult_left [symmetric]) |
|
14405 | 960 |
apply (fold o_def) |
961 |
apply (blast intro!: CDERIV_chain CDERIV_inverse) |
|
962 |
done |
|
963 |
||
964 |
lemma NSCDERIV_inverse_fun: |
|
965 |
"[| NSCDERIV f x :> d; f(x) \<noteq> 0 |] |
|
966 |
==> NSCDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))" |
|
967 |
by (simp add: NSCDERIV_CDERIV_iff CDERIV_inverse_fun del: complexpow_Suc) |
|
968 |
||
969 |
||
970 |
subsection{* Derivative of Quotient*} |
|
971 |
||
972 |
lemma CDERIV_quotient: |
|
973 |
"[| CDERIV f x :> d; CDERIV g x :> e; g(x) \<noteq> 0 |] |
|
974 |
==> CDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)" |
|
14469 | 975 |
apply (simp add: diff_minus) |
14405 | 976 |
apply (drule_tac f = g in CDERIV_inverse_fun) |
977 |
apply (drule_tac [2] CDERIV_mult, assumption+) |
|
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14405
diff
changeset
|
978 |
apply (simp add: divide_inverse right_distrib power_inverse minus_mult_left |
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14405
diff
changeset
|
979 |
mult_ac |
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14405
diff
changeset
|
980 |
del: minus_mult_right [symmetric] minus_mult_left [symmetric] |
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14405
diff
changeset
|
981 |
complexpow_Suc) |
14405 | 982 |
done |
983 |
||
984 |
lemma NSCDERIV_quotient: |
|
985 |
"[| NSCDERIV f x :> d; NSCDERIV g x :> e; g(x) \<noteq> 0 |] |
|
986 |
==> NSCDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)" |
|
987 |
by (simp add: NSCDERIV_CDERIV_iff CDERIV_quotient del: complexpow_Suc) |
|
988 |
||
989 |
||
990 |
subsection{*Caratheodory Formulation of Derivative at a Point: Standard Proof*} |
|
991 |
||
992 |
lemma CLIM_equal: |
|
993 |
"[| \<forall>x. x \<noteq> a --> (f x = g x) |] ==> (f -- a --C> l) = (g -- a --C> l)" |
|
994 |
by (simp add: CLIM_def complex_add_minus_iff) |
|
995 |
||
996 |
lemma CLIM_trans: |
|
997 |
"[| (%x. f(x) + -g(x)) -- a --C> 0; g -- a --C> l |] ==> f -- a --C> l" |
|
998 |
apply (drule CLIM_add, assumption) |
|
999 |
apply (simp add: complex_add_assoc) |
|
1000 |
done |
|
1001 |
||
1002 |
lemma CARAT_CDERIV: |
|
1003 |
"(CDERIV f x :> l) = |
|
1004 |
(\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) & isContc g x & g x = l)" |
|
1005 |
apply safe |
|
1006 |
apply (rule_tac x = "%z. if z=x then l else (f (z) - f (x)) / (z-x)" in exI) |
|
1007 |
apply (auto simp add: mult_assoc isContc_iff CDERIV_iff) |
|
1008 |
apply (rule_tac [!] CLIM_equal [THEN iffD1], auto) |
|
1009 |
done |
|
1010 |
||
1011 |
||
1012 |
lemma CARAT_NSCDERIV: |
|
1013 |
"NSCDERIV f x :> l ==> |
|
1014 |
\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) & isNSContc g x & g x = l" |
|
14469 | 1015 |
by (simp add: NSCDERIV_CDERIV_iff isNSContc_isContc_iff CARAT_CDERIV) |
14405 | 1016 |
|
1017 |
(* FIXME tidy! How about a NS proof? *) |
|
1018 |
lemma CARAT_CDERIVD: |
|
1019 |
"(\<forall>z. f z - f x = g z * (z - x)) & isNSContc g x & g x = l |
|
1020 |
==> NSCDERIV f x :> l" |
|
1021 |
apply (simp only: NSCDERIV_iff2) |
|
1022 |
apply (tactic {*(auto_tac (claset(), |
|
1023 |
simpset() delsimprocs field_cancel_factor |
|
1024 |
addsimps [thm"NSCDERIV_iff2"])) *}) |
|
1025 |
apply (simp add: isNSContc_def) |
|
1026 |
done |
|
13957 | 1027 |
|
14405 | 1028 |
ML |
1029 |
{* |
|
1030 |
val complex_add_minus_iff = thm "complex_add_minus_iff"; |
|
1031 |
val complex_add_eq_0_iff = thm "complex_add_eq_0_iff"; |
|
1032 |
val NSCLIM_NSCRLIM_Re = thm "NSCLIM_NSCRLIM_Re"; |
|
1033 |
val NSCLIM_NSCRLIM_Im = thm "NSCLIM_NSCRLIM_Im"; |
|
1034 |
val CLIM_NSCLIM = thm "CLIM_NSCLIM"; |
|
1035 |
val eq_Abs_hcomplex_ALL = thm "eq_Abs_hcomplex_ALL"; |
|
1036 |
val lemma_CLIM = thm "lemma_CLIM"; |
|
1037 |
val lemma_skolemize_CLIM2 = thm "lemma_skolemize_CLIM2"; |
|
1038 |
val lemma_csimp = thm "lemma_csimp"; |
|
1039 |
val NSCLIM_CLIM = thm "NSCLIM_CLIM"; |
|
1040 |
val CLIM_NSCLIM_iff = thm "CLIM_NSCLIM_iff"; |
|
1041 |
val CRLIM_NSCRLIM = thm "CRLIM_NSCRLIM"; |
|
1042 |
val lemma_CRLIM = thm "lemma_CRLIM"; |
|
1043 |
val lemma_skolemize_CRLIM2 = thm "lemma_skolemize_CRLIM2"; |
|
1044 |
val lemma_crsimp = thm "lemma_crsimp"; |
|
1045 |
val NSCRLIM_CRLIM = thm "NSCRLIM_CRLIM"; |
|
1046 |
val CRLIM_NSCRLIM_iff = thm "CRLIM_NSCRLIM_iff"; |
|
1047 |
val CLIM_CRLIM_Re = thm "CLIM_CRLIM_Re"; |
|
1048 |
val CLIM_CRLIM_Im = thm "CLIM_CRLIM_Im"; |
|
1049 |
val CLIM_cnj = thm "CLIM_cnj"; |
|
1050 |
val CLIM_cnj_iff = thm "CLIM_cnj_iff"; |
|
1051 |
val NSCLIM_add = thm "NSCLIM_add"; |
|
1052 |
val CLIM_add = thm "CLIM_add"; |
|
1053 |
val NSCLIM_mult = thm "NSCLIM_mult"; |
|
1054 |
val CLIM_mult = thm "CLIM_mult"; |
|
1055 |
val NSCLIM_const = thm "NSCLIM_const"; |
|
1056 |
val CLIM_const = thm "CLIM_const"; |
|
1057 |
val NSCLIM_minus = thm "NSCLIM_minus"; |
|
1058 |
val CLIM_minus = thm "CLIM_minus"; |
|
1059 |
val NSCLIM_diff = thm "NSCLIM_diff"; |
|
1060 |
val CLIM_diff = thm "CLIM_diff"; |
|
1061 |
val NSCLIM_inverse = thm "NSCLIM_inverse"; |
|
1062 |
val CLIM_inverse = thm "CLIM_inverse"; |
|
1063 |
val NSCLIM_zero = thm "NSCLIM_zero"; |
|
1064 |
val CLIM_zero = thm "CLIM_zero"; |
|
1065 |
val NSCLIM_zero_cancel = thm "NSCLIM_zero_cancel"; |
|
1066 |
val CLIM_zero_cancel = thm "CLIM_zero_cancel"; |
|
1067 |
val NSCLIM_not_zero = thm "NSCLIM_not_zero"; |
|
1068 |
val NSCLIM_not_zeroE = thms "NSCLIM_not_zeroE"; |
|
1069 |
val CLIM_not_zero = thm "CLIM_not_zero"; |
|
1070 |
val NSCLIM_const_eq = thm "NSCLIM_const_eq"; |
|
1071 |
val CLIM_const_eq = thm "CLIM_const_eq"; |
|
1072 |
val NSCLIM_unique = thm "NSCLIM_unique"; |
|
1073 |
val CLIM_unique = thm "CLIM_unique"; |
|
1074 |
val NSCLIM_mult_zero = thm "NSCLIM_mult_zero"; |
|
1075 |
val CLIM_mult_zero = thm "CLIM_mult_zero"; |
|
1076 |
val NSCLIM_self = thm "NSCLIM_self"; |
|
1077 |
val CLIM_self = thm "CLIM_self"; |
|
1078 |
val NSCLIM_NSCRLIM_iff = thm "NSCLIM_NSCRLIM_iff"; |
|
1079 |
val CLIM_CRLIM_iff = thm "CLIM_CRLIM_iff"; |
|
1080 |
val NSCLIM_NSCRLIM_iff2 = thm "NSCLIM_NSCRLIM_iff2"; |
|
1081 |
val NSCLIM_NSCRLIM_Re_Im_iff = thm "NSCLIM_NSCRLIM_Re_Im_iff"; |
|
1082 |
val CLIM_CRLIM_Re_Im_iff = thm "CLIM_CRLIM_Re_Im_iff"; |
|
1083 |
val isNSContcD = thm "isNSContcD"; |
|
1084 |
val isNSContc_NSCLIM = thm "isNSContc_NSCLIM"; |
|
1085 |
val NSCLIM_isNSContc = thm "NSCLIM_isNSContc"; |
|
1086 |
val isNSContc_NSCLIM_iff = thm "isNSContc_NSCLIM_iff"; |
|
1087 |
val isNSContc_CLIM_iff = thm "isNSContc_CLIM_iff"; |
|
1088 |
val isNSContc_isContc_iff = thm "isNSContc_isContc_iff"; |
|
1089 |
val isContc_isNSContc = thm "isContc_isNSContc"; |
|
1090 |
val isNSContc_isContc = thm "isNSContc_isContc"; |
|
1091 |
val NSCLIM_h_iff = thm "NSCLIM_h_iff"; |
|
1092 |
val NSCLIM_isContc_iff = thm "NSCLIM_isContc_iff"; |
|
1093 |
val CLIM_isContc_iff = thm "CLIM_isContc_iff"; |
|
1094 |
val isContc_iff = thm "isContc_iff"; |
|
1095 |
val isContc_add = thm "isContc_add"; |
|
1096 |
val isContc_mult = thm "isContc_mult"; |
|
1097 |
val isContc_o = thm "isContc_o"; |
|
1098 |
val isContc_o2 = thm "isContc_o2"; |
|
1099 |
val isNSContc_minus = thm "isNSContc_minus"; |
|
1100 |
val isContc_minus = thm "isContc_minus"; |
|
1101 |
val isContc_inverse = thm "isContc_inverse"; |
|
1102 |
val isNSContc_inverse = thm "isNSContc_inverse"; |
|
1103 |
val isContc_diff = thm "isContc_diff"; |
|
1104 |
val isContc_const = thm "isContc_const"; |
|
1105 |
val isNSContc_const = thm "isNSContc_const"; |
|
1106 |
val isNSContCRD = thm "isNSContCRD"; |
|
1107 |
val isNSContCR_NSCRLIM = thm "isNSContCR_NSCRLIM"; |
|
1108 |
val NSCRLIM_isNSContCR = thm "NSCRLIM_isNSContCR"; |
|
1109 |
val isNSContCR_NSCRLIM_iff = thm "isNSContCR_NSCRLIM_iff"; |
|
1110 |
val isNSContCR_CRLIM_iff = thm "isNSContCR_CRLIM_iff"; |
|
1111 |
val isNSContCR_isContCR_iff = thm "isNSContCR_isContCR_iff"; |
|
1112 |
val isContCR_isNSContCR = thm "isContCR_isNSContCR"; |
|
1113 |
val isNSContCR_isContCR = thm "isNSContCR_isContCR"; |
|
1114 |
val isNSContCR_cmod = thm "isNSContCR_cmod"; |
|
1115 |
val isContCR_cmod = thm "isContCR_cmod"; |
|
1116 |
val isContc_isContCR_Re = thm "isContc_isContCR_Re"; |
|
1117 |
val isContc_isContCR_Im = thm "isContc_isContCR_Im"; |
|
1118 |
val CDERIV_iff = thm "CDERIV_iff"; |
|
1119 |
val CDERIV_NSC_iff = thm "CDERIV_NSC_iff"; |
|
1120 |
val CDERIVD = thm "CDERIVD"; |
|
1121 |
val NSC_DERIVD = thm "NSC_DERIVD"; |
|
1122 |
val CDERIV_unique = thm "CDERIV_unique"; |
|
1123 |
val NSCDeriv_unique = thm "NSCDeriv_unique"; |
|
1124 |
val CDERIV_CLIM_iff = thm "CDERIV_CLIM_iff"; |
|
1125 |
val CDERIV_iff2 = thm "CDERIV_iff2"; |
|
1126 |
val NSCDERIV_NSCLIM_iff = thm "NSCDERIV_NSCLIM_iff"; |
|
1127 |
val NSCDERIV_NSCLIM_iff2 = thm "NSCDERIV_NSCLIM_iff2"; |
|
1128 |
val NSCDERIV_iff2 = thm "NSCDERIV_iff2"; |
|
1129 |
val NSCDERIV_CDERIV_iff = thm "NSCDERIV_CDERIV_iff"; |
|
1130 |
val NSCDERIV_isNSContc = thm "NSCDERIV_isNSContc"; |
|
1131 |
val CDERIV_isContc = thm "CDERIV_isContc"; |
|
1132 |
val NSCDERIV_const = thm "NSCDERIV_const"; |
|
1133 |
val CDERIV_const = thm "CDERIV_const"; |
|
1134 |
val NSCDERIV_add = thm "NSCDERIV_add"; |
|
1135 |
val CDERIV_add = thm "CDERIV_add"; |
|
1136 |
val lemma_nscderiv1 = thm "lemma_nscderiv1"; |
|
1137 |
val lemma_nscderiv2 = thm "lemma_nscderiv2"; |
|
1138 |
val NSCDERIV_mult = thm "NSCDERIV_mult"; |
|
1139 |
val CDERIV_mult = thm "CDERIV_mult"; |
|
1140 |
val NSCDERIV_cmult = thm "NSCDERIV_cmult"; |
|
1141 |
val CDERIV_cmult = thm "CDERIV_cmult"; |
|
1142 |
val NSCDERIV_minus = thm "NSCDERIV_minus"; |
|
1143 |
val CDERIV_minus = thm "CDERIV_minus"; |
|
1144 |
val NSCDERIV_add_minus = thm "NSCDERIV_add_minus"; |
|
1145 |
val CDERIV_add_minus = thm "CDERIV_add_minus"; |
|
1146 |
val NSCDERIV_diff = thm "NSCDERIV_diff"; |
|
1147 |
val CDERIV_diff = thm "CDERIV_diff"; |
|
1148 |
val NSCDERIV_zero = thm "NSCDERIV_zero"; |
|
1149 |
val NSCDERIV_capprox = thm "NSCDERIV_capprox"; |
|
1150 |
val NSCDERIVD1 = thm "NSCDERIVD1"; |
|
1151 |
val NSCDERIVD2 = thm "NSCDERIVD2"; |
|
1152 |
val lemma_complex_chain = thm "lemma_complex_chain"; |
|
1153 |
val NSCDERIV_chain = thm "NSCDERIV_chain"; |
|
1154 |
val CDERIV_chain = thm "CDERIV_chain"; |
|
1155 |
val CDERIV_chain2 = thm "CDERIV_chain2"; |
|
1156 |
val NSCDERIV_Id = thm "NSCDERIV_Id"; |
|
1157 |
val CDERIV_Id = thm "CDERIV_Id"; |
|
1158 |
val isContc_Id = thms "isContc_Id"; |
|
1159 |
val CDERIV_cmult_Id = thm "CDERIV_cmult_Id"; |
|
1160 |
val NSCDERIV_cmult_Id = thm "NSCDERIV_cmult_Id"; |
|
1161 |
val CDERIV_pow = thm "CDERIV_pow"; |
|
1162 |
val NSCDERIV_pow = thm "NSCDERIV_pow"; |
|
1163 |
val lemma_CDERIV_subst = thm "lemma_CDERIV_subst"; |
|
1164 |
val CInfinitesimal_add_not_zero = thm "CInfinitesimal_add_not_zero"; |
|
1165 |
val NSCDERIV_inverse = thm "NSCDERIV_inverse"; |
|
1166 |
val CDERIV_inverse = thm "CDERIV_inverse"; |
|
1167 |
val CDERIV_inverse_fun = thm "CDERIV_inverse_fun"; |
|
1168 |
val NSCDERIV_inverse_fun = thm "NSCDERIV_inverse_fun"; |
|
1169 |
val lemma_complex_mult_inverse_squared = thm "lemma_complex_mult_inverse_squared"; |
|
1170 |
val CDERIV_quotient = thm "CDERIV_quotient"; |
|
1171 |
val NSCDERIV_quotient = thm "NSCDERIV_quotient"; |
|
1172 |
val CLIM_equal = thm "CLIM_equal"; |
|
1173 |
val CLIM_trans = thm "CLIM_trans"; |
|
1174 |
val CARAT_CDERIV = thm "CARAT_CDERIV"; |
|
1175 |
val CARAT_NSCDERIV = thm "CARAT_NSCDERIV"; |
|
1176 |
val CARAT_CDERIVD = thm "CARAT_CDERIVD"; |
|
1177 |
*} |
|
1178 |
||
1179 |
end |