Quelle cross_metric_real_fun.pvs Sprache: PVS

%---------------------------------------------------------------------------------------------------------
%
%       One-Variable Uniform Continuity of Real Valued Functions on Product Metric Spaces
%
%       Author: Anthony Narkawicz, NASA Langley
%
%
%       Version 1.0                     August 27, 2009
%
%---------------------------------------------------------------------------------------------------------

cross_metric_real_fun[T1:Type+,d1:[T1,T1->nnreal],
                  T2:Type+,d2:[T2,T2->nnreal]]: THEORY

BEGIN

    ASSUMING IMPORTING metric_spaces

        fullset_metric_space1: ASSUMPTION metric_space?[T1,d1](fullset[T1])
        fullset_metric_space2: ASSUMPTION metric_space?[T2,d2](fullset[T2])

    ENDASSUMING

  IMPORTING real_metric_space,cross_metric_uniform_continuity[T1,d1,T2,d2,real,real_dist], continuity_ms[T2,d2,real,real_dist], real_fun_on_compact_sets[T1,d1]

  X: VAR set[T1]
  Y: VAR set[T2]
  f: VAR [[T1,T2] -> real]

  % If X is compact, then the function unif_min_first(f,X) = (LAMBDA (t: T2) = min({r: real | EXISTS (x: (X)): r = f(x,t)}))
  % is continuous.

  IMPORTING reals@bounded_reals[real]

  % The main TCC:

  curried_min_exists: LEMMA nonempty?(X) AND continuous?(f,fullset[[(X),(Y)]]) AND compact?(X)
     IMPLIES (FORALL (t: T2): Y(t) IMPLIES
         nonempty?[real]({r: real | EXISTS (x: (X)): r = f(x, t)}) AND
          below_bounded[real]({r: real | EXISTS (x: (X)): r = f(x, t)}) AND
           ext[real]({r: real | EXISTS (x: (X)): r = f(x, t)})(inf[real]({r: real | EXISTS (x: (X)): r = f(x, t)}))
    AND (EXISTS (x: (X)): FORALL (y: (X)): f(x,t) <= f(y,t)))

  curried_min_is_cont: THEOREM (compact?(X) AND continuous?(f,fullset[[(X),(Y)]]) AND nonempty?(X)) IMPLIES
           LET unif_min_first(t: T2): real = IF Y(t) THEN min({r: real | EXISTS (x: (X)): r = f(x,t)}) ELSE 0 ENDIF
         IN  continuous?(unif_min_first,Y)



END cross_metric_real_fun

quality91%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.