Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Sprache: PVS

Original von: PVS^©

quad_minmax: THEORY
%----------------------------------------------------------------------------
%
%  Minimums and Maximums of quadratic functions:
%
%        quadratic(a,b,c)(x): real = a*sq(x) + b*x + c
%
%  This theory is derived from quadratic_minmax.  This theory has the same
%  theorems but used a more convenient LET ... IN form that reduces the
%  number of free variables.
%
%----------------------------------------------------------------------------
BEGIN

  IMPORTING quadratic        %% quadratic_minmax deprecated

  a   : VAR nonzero_real
  b,c: VAR real
  x,y  : VAR real
  xl,xu,t: VAR real
  f: VAR [real -> real]
  epsil: VAR posreal

% ---------- Following apply to both min and max cases -----------

  quad_minmaxpt_delta: LEMMA LET f = quadratic(a,b,c), m = -b/(2*a) IN
                               f(m + t) = f(m - t)

  quad_minmaxpt_midpt: LEMMA LET f = quadratic(a,b,c), m = -b/(2*a) IN
                 x /= y AND f(x) = f(y) IMPLIES m = (x + y)/2

% ---- is_minimum? is also defined in real_fun_preds in analysis library

%  is_minimum?(x:real, f: [real -> real]): bool = FORALL y : f(x) <= f(y)

  is_minimum?(x, f): bool = FORALL y : f(x) <= f(y)

  quad_min : LEMMA  LET f = quadratic(a,b,c),
                            minpt = -b/(2*a) IN
                          a > 0 IMPLIES
                             is_minimum?(minpt,f)

  quad_min_val : LEMMA LET f = quadratic(a,b,c),
                           minpt = -b/(2*a) IN
                            a > 0
                              IMPLIES f(x) >= (4*a*c-sq(b))/(4*a)

  quad_min_mono_inc : LEMMA LET f = quadratic(a,b,c),
                                minpt = -b/(2*a) IN
                             a > 0 IMPLIES
                             x > y AND y >= minpt
                             IMPLIES
                             f(x) > f(y)

  quad_min_mono_dec : LEMMA  LET f = quadratic(a,b,c),
                                 minpt = -b/(2*a) IN
                              a > 0 AND
                              x < y AND y <= minpt
                              IMPLIES
                                 f(x) > f(y)

  quad_min_eq_intv: LEMMA a > 0 AND
                           quadratic(a,b,c)(xl) = quadratic(a,b,c)(xu) AND
                           xl < t AND t < xu
                               IMPLIES
                                  quadratic(a,b,c)(t) < quadratic(a,b,c)(xu)

  quad_min_eq_is_in: LEMMA a > 0 AND
                           quadratic(a,b,c)(xl) = quadratic(a,b,c)(xu) AND
                           quadratic(a,b,c)(t) < quadratic(a,b,c)(xu) AND
                           xl < xu
                               IMPLIES
                                 (xl < t AND t < xu)

  quad_loc_min_is_glob_min: LEMMA a > 0 AND (FORALL (y): (x-epsil < y AND
            y < x+epsil) IMPLIES
      quadratic(a,b,c)(y) >= quadratic(a,b,c)(x))
      IMPLIES
      x = -b/(2*a)

% ---- is_maximum? is also defined in real_fun_preds in analysis library

%  is_maximum?(x:real, f: [real -> real]): bool = FORALL y : f(x) >= f(y)

  is_maximum?(x, f): bool = FORALL y : f(x) >= f(y)

  quad_max : LEMMA LET f = quadratic(a,b,c),
                       maxpt = -b/(2*a) IN
                         a < 0
                           IMPLIES is_maximum?(maxpt,f)

  quad_max_val : LEMMA LET f = quadratic(a,b,c),
                           maxpt = -b/(2*a) IN
                              a < 0
                                IMPLIES f(x) <= (4*a*c-sq(b))/(4*a)

  quad_max_mono_inc : LEMMA LET f = quadratic(a,b,c),
                                maxpt = -b/(2*a) IN
                             a < 0 AND
                             x < y AND y <= maxpt
                             IMPLIES
                                 f(x) < f(y)

  quad_max_mono_dec : LEMMA LET f = quadratic(a,b,c),
                                maxpt = -b/(2*a) IN
                                  a < 0 AND
                                  x > y AND y >= maxpt
                                  IMPLIES
                                      f(x) < f(y)

  quad_max_eq_intv: LEMMA a < 0 AND
                           quadratic(a,b,c)(xl) = quadratic(a,b,c)(xu) AND
                           xl < t AND t < xu
                               IMPLIES
                                  quadratic(a,b,c)(t) > quadratic(a,b,c)(xu)

  quad_max_eq_is_in: LEMMA a < 0 AND
                           quadratic(a,b,c)(xl) = quadratic(a,b,c)(xu) AND
                           quadratic(a,b,c)(t) > quadratic(a,b,c)(xu) AND
                           xl < xu
                               IMPLIES
                                 (xl < t AND t < xu)

  quad_loc_max_is_glob_max: LEMMA a < 0 AND (FORALL (y): (x-epsil < y AND
          y < x+epsil) IMPLIES
    quadratic(a,b,c)(y) <= quadratic(a,b,c)(x))
    IMPLIES
    x = -b/(2*a)

  quad_intv_max_at_endpoint: LEMMA a>0 AND xl<=xu IMPLIES
    (FORALL (t): xl<=t AND t<=xu IMPLIES quadratic(a,b,c)(t)<=quadratic(a,b,c)(xl))
    OR
    (FORALL (t): xl<=t AND t<=xu IMPLIES quadratic(a,b,c)(t)<=quadratic(a,b,c)(xu))

  quad_intv_increasing_from_min: LEMMA a > 0 AND abs(x-(-b/(2*a))) <= abs(y-(-b/(2*a)))
    IMPLIES quadratic(a,b,c)(x) <= quadratic(a,b,c)(y)

END quad_minmax

¤ Dauer der Verarbeitung: 0.23 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.