Impressum convex_function_props.pvs Sprache: 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

quality87%

¤ 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.0.0Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Versionsinformation zu Columbo

Bemerkung:

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Anfrage:

Dauer der Verarbeitung:

Sekunden

sprechenden Kalenders