|
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.19 Sekunden
(vorverarbeitet)
¤
|
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.
|
