Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/PVS/measure_integration/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 2 kB

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.