Impressum convex_function_props.pvs

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