Quelle sup_norm.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Properties of sup norm for functions
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------

sup_norm[T:TYPE]: THEORY

BEGIN

  epsilon: VAR posreal
  c:   VAR nnreal
  y:   VAR real
  x:   VAR T
  i,n: VAR nat

  IMPORTING reals@real_fun_ops_aux[T],
            reals@bounded_reals[real],
            structures@const_fun_def[T,real]

  bounded?(f:[T->real]):bool = EXISTS c: FORALL x: abs(f(x)) <= c

  bounded: TYPE+ = (bounded?) CONTAINING (LAMBDA x: 0)

  f,f1,f2: VAR bounded

  bounded_add:  JUDGEMENT +(f1,f2) HAS_TYPE bounded
  bounded_scal: JUDGEMENT *(y,f)   HAS_TYPE bounded
  bounded_opp:  JUDGEMENT -(f)     HAS_TYPE bounded
  bounded_diff: JUDGEMENT -(f1,f2) HAS_TYPE bounded

  sup_norm(f):nnreal = IF EXISTS x: TRUE THEN sup({c | EXISTS x: abs(f(x))=c})
                                         ELSE 0 ENDIF

  sup_norm_eq_0: LEMMA sup_norm(f) = 0 <=> f = const_fun[T,real](0)
  sup_norm_neg:  LEMMA sup_norm(-f) = sup_norm(f)
  sup_norm_sum:  LEMMA sup_norm(f1+f2) <= sup_norm(f1)+sup_norm(f2)

  sup_norm_prop: LEMMA
       (FORALL x: abs(f(x)) <= sup_norm(f)) AND
       (FORALL c: (FORALL x: abs(f(x)) <= c) => sup_norm(f) <= c)

  u: VAR sequence[bounded]

  sup_norm_converges_to?(u,f):bool
    = FORALL epsilon: EXISTS n: FORALL i: i >= n => sup_norm(u(i)-f) < epsilon

  sup_norm_convergent?(u):bool = EXISTS f: sup_norm_converges_to?(u,f)

  sup_norm_convergent: TYPE+ = (sup_norm_convergent?) CONTAINING
                                    (LAMBDA n: LAMBDA x: 0)

  IMPORTING pointwise_convergence[T]

  sup_norm_convergent_is_pointwise_convergent: JUDGEMENT
                            sup_norm_convergent SUBTYPE_OF pointwise_convergent

  sup_norm_converges_to_pointwise_convergence: LEMMA
     sup_norm_converges_to?(u,f) => pointwise_convergence?(u,f)

END sup_norm

quality95%

¤ 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.