|
derivatives_alt [ T : TYPE FROM real ] : THEORY
BEGIN
ASSUMING
IMPORTING deriv_domain_def
deriv_domain : ASSUMPTION deriv_domain?[T]
not_one_element : ASSUMPTION not_one_element?[T]
ENDASSUMING
IMPORTING derivatives, continuous_functions_props
AUTO_REWRITE- abs_neg
f, fp : VAR [T -> real]
x, y, a, b, c : VAR T
D : VAR real
%--------------------------------------------
% Equivalent definitions of differentiation
%--------------------------------------------
derivative_equivalence1 : LEMMA (derivable?(f, x) AND deriv(f, x) = D)
IFF convergence(NQ(f, x), 0, D)
derivative_equivalence2 : LEMMA convergence(NQ(f, x), 0, D)
IFF (EXISTS (phi : [T -> real]) : convergence(phi, x, 0)
AND FORALL y : f(y) - f(x) = (y - x) * (D + phi(y)))
derivative_equivalence3 : LEMMA (derivable?(f,x) AND deriv(f,x) = D) %% Lester
IFF (EXISTS (psi : [T -> real]) : convergence(psi, x, D)
AND FORALL y : f(y) - f(x) = (y - x) * psi(y))
epsi_eq_0: LEMMA (FORALL (epsi: posreal): abs(x) < epsi) IFF x = 0
derivative_squeeze : LEMMA convergence(NQ(f, x), 0, fp(x)) %% Butler
IFF (EXISTS (HH: [(A(x)) -> real]):
convergence(HH,0,0) AND
HH = (LAMBDA (h: (A(x))): (NQ(f,x)(h) - fp(x))))
derivative_squeeze_delta: LEMMA convergence(NQ(f, x), 0, fp(x)) %% Butler
IFF (EXISTS (HH: [(A(x)) -> real]):
convergence(HH,0,0) AND
(EXISTS (delta: posreal):
(FORALL (h: (A(x))): (abs(h) < delta) IMPLIES
abs(NQ(f,x)(h) - fp(x)) <= HH(h))))
%------------------------------------
% f constant on [a, b]
%------------------------------------
deriv_constant1 : LEMMA a < c AND c < b AND
(FORALL x : a < x AND x < b IMPLIES f(x) = f(c))
IMPLIES convergence(NQ(f, c), 0, 0)
deriv_constant2 : LEMMA a < c AND c < b AND
(FORALL x : a < x AND x < b IMPLIES f(x) = f(c))
IMPLIES derivable?(f, c) AND deriv(f, c) = 0
END derivatives_alt
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
