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

quality93%

¤ 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.11Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.