| products/sources/formale Sprachen/PVS/analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: derivative_props.pvs Sprache: PVSOriginal von: PVS© |
|
||||||
|
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 % 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 : LEMMA 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 : LEMMA 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 : THEOREM 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 : LEMMA increasing?(g) IFF (FORALL x : deriv(g, x) >= 0) nonpos_derivative : LEMMA 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) 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.15 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.Bot Zugriff |
