|
%------------------------------------------------------------------------------
% 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
¤ Dauer der Verarbeitung: 0.6 Sekunden
(vorverarbeitet)
¤
|
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.
|
