Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/PVS/reals/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 5 kB

Quelle quad_minmax.pvs Sprache: 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

quality89%

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

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.