| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis_ax/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 3 kB |
|
Quellcode-Bibliothek derivative_props.pvs Sprache: 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 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 ¤ 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.0.14Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28