9 |
9 |
10 (*----------------------------------------------------------------------- |
10 (*----------------------------------------------------------------------- |
11 Limits, continuity and differentiation: standard and NS definitions |
11 Limits, continuity and differentiation: standard and NS definitions |
12 -----------------------------------------------------------------------*) |
12 -----------------------------------------------------------------------*) |
13 constdefs |
13 constdefs |
14 LIM :: [real=>real,real,real] => bool ("((_)/ -- (_)/ --> (_))" 60) |
14 LIM :: [real=>real,real,real] => bool |
15 "f -- a --> L == (ALL r. #0 < r --> |
15 ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) |
16 (EX s. #0 < s & (ALL x. (#0 < abs(x + -a) & (abs(x + -a) < s) |
16 "f -- a --> L == |
17 --> abs(f x + -L) < r))))" |
17 ALL r. #0 < r --> |
|
18 (EX s. #0 < s & (ALL x. (x ~= a & (abs(x + -a) < s) |
|
19 --> abs(f x + -L) < r)))" |
18 |
20 |
19 NSLIM :: [real=>real,real,real] => bool ("((_)/ -- (_)/ --NS> (_))" 60) |
21 NSLIM :: [real=>real,real,real] => bool |
|
22 ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) |
20 "f -- a --NS> L == (ALL x. (x ~= hypreal_of_real a & |
23 "f -- a --NS> L == (ALL x. (x ~= hypreal_of_real a & |
21 x @= hypreal_of_real a --> (*f* f) x @= hypreal_of_real L))" |
24 x @= hypreal_of_real a --> (*f* f) x @= hypreal_of_real L))" |
22 |
25 |
23 isCont :: [real=>real,real] => bool |
26 isCont :: [real=>real,real] => bool |
24 "isCont f a == (f -- a --> (f a))" |
27 "isCont f a == (f -- a --> (f a))" |
27 isNSCont :: [real=>real,real] => bool |
30 isNSCont :: [real=>real,real] => bool |
28 "isNSCont f a == (ALL y. y @= hypreal_of_real a --> |
31 "isNSCont f a == (ALL y. y @= hypreal_of_real a --> |
29 (*f* f) y @= hypreal_of_real (f a))" |
32 (*f* f) y @= hypreal_of_real (f a))" |
30 |
33 |
31 (* differentiation: D is derivative of function f at x *) |
34 (* differentiation: D is derivative of function f at x *) |
32 deriv:: [real=>real,real,real] => bool ("(DERIV (_)/ (_)/ :> (_))" 60) |
35 deriv:: [real=>real,real,real] => bool |
|
36 ("(DERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60) |
33 "DERIV f x :> D == ((%h. (f(x + h) + -f(x))*inverse(h)) -- #0 --> D)" |
37 "DERIV f x :> D == ((%h. (f(x + h) + -f(x))*inverse(h)) -- #0 --> D)" |
34 |
38 |
35 nsderiv :: [real=>real,real,real] => bool ("(NSDERIV (_)/ (_)/ :> (_))" 60) |
39 nsderiv :: [real=>real,real,real] => bool |
|
40 ("(NSDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60) |
36 "NSDERIV f x :> D == (ALL h: Infinitesimal - {0}. |
41 "NSDERIV f x :> D == (ALL h: Infinitesimal - {0}. |
37 ((*f* f)(hypreal_of_real x + h) + |
42 ((*f* f)(hypreal_of_real x + h) + |
38 -hypreal_of_real (f x))*inverse(h) @= hypreal_of_real D)" |
43 -hypreal_of_real (f x))*inverse(h) @= hypreal_of_real D)" |
39 |
44 |
40 differentiable :: [real=>real,real] => bool (infixl 60) |
45 differentiable :: [real=>real,real] => bool (infixl 60) |