|
riesz_bounded_functionals[a:real,b: {bb:real | a < bb},
(importing riesz_function_sets[a,b])Funs:TYPE FROM [INTab->real]]: THEORY
%------------------------------------------------------------------------------
% Bounded linear functionals on a subtype of [real->real]. This is in direct
% support of the Riesz representation theorem.
%------------------------------------------------------------------------------
BEGIN
ASSUMING IMPORTING riesz_function_sets[a,b]
funs_subspace: ASSUMPTION bounded_linear_subspace?(fullset[Funs])
ENDASSUMING
IMPORTING riesz_linear_functionals[a,b,Funs], riesz_function_sets[a,b]
h,f,g: VAR Funs
c,y: VAR real
M: VAR nnreal
L: VAR Operator
bounded_op?(L) : bool = (EXISTS (M:nnreal): FORALL (f): abs(L(f)) <= M*fun_norm(f))
op_norm(L: (bounded_op?)): {M:nnreal | (FORALL (f:Funs): abs(L(f))<=M*fun_norm(f)) AND (FORALL (M1:real): M1 < M IMPLIES
EXISTS (f:Funs): abs(L(f)) > M1*fun_norm(f))}
op_norm_bound: LEMMA FORALL (L:(bounded_op?),f): abs(L(f)) <= op_norm(L)*fun_norm(f)
bounded_linear_operator?(L): bool = bounded_op?(L) AND linear_op?(L)
END riesz_bounded_functionals
¤ Dauer der Verarbeitung: 0.0 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.
|
