Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: convex_functions.pvs Sprache: PVS

Original von: PVS^©

convex_functions: THEORY
%------------------------------------------------------------------------------
% In This Theory, We Define Convex And Stricly Convex Functions. We Prove
%    That The Maximum Of Two Convex Functions Is Convex And That
%    A Convex Function Has At Most One Minimum
%
%     Authors: Anthony Narkawicz,  NASA Langley
%
%     Version 1.0         9/23/2009  Initial Version
%     Version 1.1   10/21/2009
%------------------------------------------------------------------------------
BEGIN

   IMPORTING quadratic, real_fun_ops

   f,g: VAR [real -> real]
   A,B,C,v,w,x,y,z,t,b,c,d: VAR real
   k  : VAR nat
   a,H: VAR posreal
   aaa: VAR nnreal

   % Convex

   convex?(f): bool = FORALL (x,y,t): 0 <= t and t <= 1 IMPLIES
                f(t*x + (1-t)*y) <= t*f(x) + (1-t)*f(y)

   % Basic Properties

   composition_of_convex: LEMMA (FORALL (x,y): x<=y IMPLIES g(x)<=g(y))
          AND convex?(f) AND convex?(g) IMPLIES convex?(g o f)

   max_of_convex: LEMMA convex?(f) AND convex?(g) IMPLIES
       convex?((LAMBDA (z): max(f(z),g(z))))

   sum_of_convex: LEMMA convex?(f) AND convex?(g) IMPLIES convex?(f+g)

   scal_convex:   LEMMA convex?(f) IMPLIES convex?(aaa*f)

   convex_function_right_lt: LEMMA convex?(f) AND A<C AND C<B
     IMPLIES f(B) >= ((B-A)/(C-A))*f(C) - ((B-C)/(C-A))*f(A)

   convex_function_left_lt: LEMMA convex?(f) AND A<C AND C<B
     IMPLIES f(A) >= ((B-A)/(B-C))*f(C) - ((C-A)/(B-C))*f(B)

   % The Following Theorem Can Help In Proofs Where Convexity Is Used
   % By Allowing The User To Escape The Construction Of A Specific t-value

   between_point_is_wtd_av: LEMMA FORALL (x,y,z: real): x<=z AND z<=y
          IMPLIES (EXISTS (t: real): 0<=t AND t<=1
            AND z = t*x + (1-t)*y)

   % Sometimes, it may be convenient to have the t as the coeff of x

   between_point_is_wtd_av2: LEMMA FORALL (x,y,z: real): x<=z AND z<=y
          IMPLIES (EXISTS (t: real): 0<=t AND t<=1
            AND z = (1-t)*x + t*y)

   % The Minima Of Convex Functions Have Certain Fun(ction) properties

   convex_const_on_connected_min: LEMMA convex?(f) AND x < y AND
     (FORALL (z): x<=z AND z<=y IMPLIES f(x) = f(z))
  IMPLIES
  (FORALL (w): f(x) <= f(w))

   convex_min_is_connected: LEMMA convex?(f) AND x < y AND f(x) = f(y)
          AND (FORALL (z): f(x) <= f(z))
       IMPLIES
       (FORALL (w): x<=w AND w<=y IMPLIES f(w) = f(x))

     % Part B: Local Minima Of Convex Functions....

   loc_convex_min_is_connected: LEMMA convex?(f) AND A<=x AND x<y AND y<=B AND
     f(x) = f(y) AND
     (FORALL (w): x<=w AND w<=y IMPLIES f(x) <= f(w)) IMPLIES
  (FORALL (w): x<=w AND w<=y IMPLIES f(w) = f(x))

   % Helpful results about convex functions

   convex_btw_pt_left_lt: LEMMA convex?(f) AND A<x AND x<=B AND f(A)<=c
           AND f(B)<c IMPLIES f(x) < c

   convex_btw_pt_right_lt: LEMMA convex?(f) AND A<=x AND x<B AND f(A)<c
           AND f(B)<=c IMPLIES f(x) < c

   convex_wtd_av_lt: LEMMA convex?(f) AND f(x)<c AND f(y) < c
             IMPLIES (FORALL (t): 0 <= t AND t <= 1 IMPLIES
                 f(t*x + (1-t)*y) < c)

   % If a convex function has x as its min, then it is increasing to the
   % right of x and decreasing to the left of x

   convex_increasing: LEMMA convex?(f) AND (FORALL (y): f(y)>=f(x))
           AND v>=x AND w>=v IMPLIES
        f(w)>=f(v)

   convex_decreasing: LEMMA convex?(f) AND (FORALL (y): f(y)>=f(x))
           AND w<=v AND v<=x IMPLIES
        f(w)>=f(v)

   % STRICTLY CONVEX FUNCTIONS

   strictly_convex?(f): bool = FORALL (x,y,t): 0 < t and t < 1 and x /= y IMPLIES
                 f(t*x + (1-t)*y) < t*f(x) + (1-t)*f(y)

   strictly_convex_implies_convex: LEMMA strictly_convex?(f) IMPLIES convex?(f)

   strictly_convex_unique_min: LEMMA strictly_convex?(f) AND (FORALL (z):
             f(x) <= f(z) AND f(y) <= f(z)) IMPLIES
          x = y

   strictly_conv_uniq_intv_min: LEMMA strictly_convex?(f) AND
       (A <= x AND x <= B) AND
    (A <= y AND y <= B) AND
    (FORALL (z): (A <= z and z <= B) IMPLIES
     f(x) <= f(z) AND f(y) <= f(z))
    IMPLIES
    x = y

   % Basic Properties

   composition_of_strictly_convex: LEMMA (FORALL (x,y): x<=y IMPLIES g(x)<g(y))
          AND convex?(f) AND strictly_convex?(g)
       IMPLIES strictly_convex?(g o f)

   max_of_strictly_convex: LEMMA strictly_convex?(f) AND
         strictly_convex?(g) IMPLIES
    strictly_convex?((LAMBDA (z): max(f(z),g(z))))

   sum_of_strictly_convex: LEMMA strictly_convex?(f) AND strictly_convex?(g)
         IMPLIES strictly_convex?(f+g)

   scal_strictly_convex:  LEMMA strictly_convex?(f) IMPLIES strictly_convex?(a*f)

   % Helpful results about strictly convex functions

   strictly_convex_btw_pt_lt: LEMMA strictly_convex?(f) AND A<x AND x<B AND f(A)<=c
           AND f(B)<=c IMPLIES f(x) < c

   % Special Case: Quadratics

   quad_convex: LEMMA convex?(quadratic(aaa,b,c))

   quad_strictly_convex: LEMMA strictly_convex?(quadratic(a,b,c))

   abs_linear_convex: LEMMA convex?((LAMBDA (t): abs(x + t*y)-H))

   quad_linear_max_convex: LEMMA LET maxfun = (LAMBDA (t): max(quadratic(a,b,c)(t),
            abs(x + t*y)-H))
          IN convex?(maxfun)

   quad_linear_max_glob_min: LEMMA LET maxfun = (LAMBDA (t): max(quadratic(a,b,c)(t),
            abs(x + t*y)-H))
          IN y /= 0 AND maxfun(w) = 0 AND maxfun(v) = 0 AND
             (FORALL (z): 0 <= maxfun(z))
      IMPLIES
      v = w

   quad_linear_max_loc_min: LEMMA LET maxfun = (LAMBDA (t): max(quadratic(a,b,c)(t),
            abs(x + t*y)-H))
          IN y /= 0 AND
             (A <= w AND w <= B) AND (A <= v AND v <= B) AND
             maxfun(w) = 0 AND maxfun(v) = 0 AND
             (FORALL (z): (A <= z AND z <= B) IMPLIES 0 <= maxfun(z))
      IMPLIES
      v = w

   % Special Case: Exponentials Of Convex Functions

   power_of_convex: LEMMA convex?(f) AND (FORALL (x): f(x)>=0)
     IMPLIES convex?(LAMBDA (x): f(x)^k)

   power_of_strictly_convex: LEMMA strictly_convex?(f) AND (FORALL (x): f(x)>=0)
     IMPLIES strictly_convex?(LAMBDA (x): f(x)^(k+1))

END convex_functions

¤ Dauer der Verarbeitung: 0.18 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.