33 "isNSCont f a == (\<forall>y. y @= hypreal_of_real a --> |
33 "isNSCont f a == (\<forall>y. y @= hypreal_of_real a --> |
34 ( *f* f) y @= hypreal_of_real (f a))" |
34 ( *f* f) y @= hypreal_of_real (f a))" |
35 |
35 |
36 (* differentiation: D is derivative of function f at x *) |
36 (* differentiation: D is derivative of function f at x *) |
37 deriv:: "[real=>real,real,real] => bool" |
37 deriv:: "[real=>real,real,real] => bool" |
38 ("(DERIV (_)/ (_)/ :> (_))" [0, 0, 60] 60) |
38 ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) |
39 "DERIV f x :> D == ((%h. (f(x + h) + -f x)/h) -- 0 --> D)" |
39 "DERIV f x :> D == ((%h. (f(x + h) + -f x)/h) -- 0 --> D)" |
40 |
40 |
41 nsderiv :: "[real=>real,real,real] => bool" |
41 nsderiv :: "[real=>real,real,real] => bool" |
42 ("(NSDERIV (_)/ (_)/ :> (_))" [0, 0, 60] 60) |
42 ("(NSDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) |
43 "NSDERIV f x :> D == (\<forall>h \<in> Infinitesimal - {0}. |
43 "NSDERIV f x :> D == (\<forall>h \<in> Infinitesimal - {0}. |
44 (( *f* f)(hypreal_of_real x + h) + |
44 (( *f* f)(hypreal_of_real x + h) + |
45 - hypreal_of_real (f x))/h @= hypreal_of_real D)" |
45 - hypreal_of_real (f x))/h @= hypreal_of_real D)" |
46 |
46 |
47 differentiable :: "[real=>real,real] => bool" (infixl "differentiable" 60) |
47 differentiable :: "[real=>real,real] => bool" (infixl "differentiable" 60) |