|
derivative_props [ T : TYPE FROM real ] : THEORY
BEGIN
ASSUMING
IMPORTING deriv_domain_def
connected_domain : ASSUMPTION connected?[T]
not_one_element : ASSUMPTION not_one_element?[T]
ENDASSUMING
% IMPORTING derivatives_alt[T], continuous_functions_props
IMPORTING derivatives, continuous_functions_props
% AUTO_REWRITE- abs_0
% AUTO_REWRITE- abs_neg
deriv_domain: LEMMA deriv_domain?[T]
f, fp : VAR [T -> real]
x, y, a, b, c : VAR T
D : VAR real
%--------------------------------------
deriv_maximum : AXIOM
a < c AND c < b AND derivable?(f, c) AND
(FORALL x : a < x AND x < b IMPLIES f(x) <= f(c))
IMPLIES deriv(f, c) = 0
deriv_minimum : LEMMA
a < c AND c < b AND derivable?(f, c) AND
(FORALL x : a < x AND x < b IMPLIES f(c) <= f(x))
IMPLIES deriv(f, c) = 0
%-----------------------
% Mean value theorem
%-----------------------
mean_value_aux : AXIOM derivable?(f) AND a < b AND f(a) = f(b) IMPLIES
EXISTS c : a < c AND c < b AND deriv(f, c) = 0
mean_value : THEOREM derivable?(f) AND a < b IMPLIES
EXISTS c : a < c AND c < b AND
deriv(f, c) * (b - a) = f(b) - f(a)
mean_value_abs : AXIOM derivable?(f) AND a /= b IMPLIES % BUTLER
EXISTS c: min(a,b) < c AND c < max(a,b) AND
abs(deriv(f, c)) * abs(b - a) = abs(f(b) - f(a))
%------------------------------------------
% Applications of the mean value theorem
%------------------------------------------
g : VAR deriv_fun[T]
nonneg_derivative : AXIOM increasing?(g) IFF (FORALL x : deriv(g, x) >= 0)
nonpos_derivative : AXIOM decreasing?(g) IFF (FORALL x : deriv(g, x) <= 0)
positive_derivative : LEMMA (FORALL x: deriv(g, x) > 0)
IMPLIES strict_increasing?(g)
negative_derivative : LEMMA (FORALL x : deriv(g, x) < 0)
IMPLIES strict_decreasing?(g)
null_derivative : LEMMA constant?(g) IFF (FORALL x : deriv(g, x) = 0)
%% --- David Lester Additions ---
minimum_derivative: LEMMA deriv(g)(x) = 0 AND x /= y AND
(FORALL (y:T): y /= x IMPLIES deriv(g)(y)*(y-x) > 0)
IMPLIES g(x) < g(y)
maximum_derivative: LEMMA deriv(g)(x) = 0 AND x /= y AND
(FORALL (y:T): y /= x IMPLIES deriv(g)(y)*(y-x) < 0)
IMPLIES g(y) < g(x)
strict_minimum_derivative: LEMMA strict_increasing?(deriv(g)) AND
deriv(g)(x) = 0 AND x /= y
IMPLIES g(x) < g(y)
strict_maximum_derivative: LEMMA strict_decreasing?(deriv(g)) AND
deriv(g)(x) = 0 AND x /= y
IMPLIES g(y) < g(x)
% — moved from derivatives_more
monotonic_antideriv: LEMMA FORALL (a, b: T, f, g: deriv_fun[T]):
(FORALL (x:T): deriv(f)(x) >= deriv(g)(x)) AND
a <= b =>
f(b) - f(a) >= g(b) - g(a)
% derivative_alt : LEMMA FORALL (D: real, ff: [T -> real], x: T):
% convergence(NQ(ff, x), 0, D)
% IFF convergence(LAMBDA (y: {yy:T|yy/=x}): (ff(y) - ff(x))/(y - x), x, D)
% derivative_fun_alt : LEMMA FORALL (ff, gg: [T -> real]):
% derivable?(ff) AND deriv(ff) = gg
% IFF (FORALL x: convergence(LAMBDA (y: {yy:T|yy/=x}):
% (ff(y) - ff(x))/(y - x), x, gg(x)))
epsi_lt_le: LEMMA (FORALL (epsilon: posreal): x < epsilon) IFF
(FORALL (epsilon: posreal): x <= epsilon)
END derivative_props
¤ Dauer der Verarbeitung: 0.16 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.
|
