|
convex_function_props: THEORY
%------------------------------------------------------------------------------
% In this theory, we prove basic analytic properties of convex functions. In
% particular, they are continuous.
%
% Authors: Anthony Narkawicz, NASA Langley
%
% Version 1.0 10/23/2009 Initial Version
%------------------------------------------------------------------------------
BEGIN
IMPORTING real_metric_space, continuity_ms_def, reals@convex_functions
f: VAR [real -> real]
A,B,C,X,Y: VAR real
convex_functions_locally_bounded: LEMMA convex?(f) IMPLIES FORALL (A, B: real):
A<=B IMPLIES EXISTS (M: nat): FORALL (x: real): A<=x AND x<=B IMPLIES abs(f(x)) < M
convex_diff_quot_left_lt: LEMMA convex?(f) IMPLIES FORALL(A,B,C):
A<B AND B<C IMPLIES (f(C)-f(B))/(C-B) >= (f(C)-f(A))/(C-A)
convex_diff_quot_right_lt: LEMMA convex?(f) IMPLIES FORALL(A,B,C):
A<B AND B<C IMPLIES (f(B)-f(A))/(B-A) <= (f(C)-f(A))/(C-A)
convex_diff_quot_increasing: LEMMA convex?(f) IMPLIES FORALL(A,B,C):
A<B AND B<C IMPLIES (f(B)-f(A))/(B-A) <= (f(C)-f(B))/(C-B)
convex_diff_quot_bounded: LEMMA convex?(f) IMPLIES
FORALL (x: real): FORALL (epsil: posreal): EXISTS (M: nat):
FORALL (delta: nzreal):
abs(delta)<=epsil IMPLIES abs(f(x+delta)-f(x))/abs(delta) < M
convex_functions_continuous: LEMMA convex?(f) IMPLIES
continuous?[real,real_dist,real,real_dist](f)
END convex_function_props
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
