|
riesz_hahn_banach[a:real,b: {bb:real | a < bb}]: THEORY
%------------------------------------------------------------------------------
% The Hahn Banach theorem for the special case of extensions from C[a,b] to
% B[a,b].
%------------------------------------------------------------------------------
BEGIN
IMPORTING riesz_interval_funs[a,b],riesz_bounded_functionals
h: VAR [INTab -> real]
c,y: VAR real
M: VAR nnreal
%--------------%
C_Bounded_Linear_Operator : TYPE = (bounded_linear_operator?[a,b,(continuous_on_int?[a,b])])
B_Bounded_Linear_Operator : TYPE = (bounded_linear_operator?[a,b,(bounded_on_int?[a,b])])
LC : VAR C_Bounded_Linear_Operator
LB : VAR B_Bounded_Linear_Operator
Op_Pair: TYPE = [# space: (bounded_linear_subspace?[a,b]), Lop: (bounded_linear_operator?[a,b,(space)]) #]
OE,Ext : VAR Op_Pair
<=(OE,Ext) : bool = subset?(OE`space,Ext`space) AND (FORALL (ff:[INTab->real]): OE`space(ff) IMPLIES OE`Lop(ff) = Ext`Lop(ff))
AND op_norm[a,b,(OE`space)](OE`Lop) = op_norm[a,b,(Ext`space)](Ext`Lop)
Hahn_Banach_partial_order: LEMMA partial_order?[Op_Pair](<=)
IMPORTING orders@zorn
Op_Extension(OE) : TYPE = {Ext | OE <= Ext}
le(OE)(OEext1,OEext2:Op_Extension(OE)): bool = OEext1<=OEext2
Hahn_Banach_partial_order_sub: LEMMA partial_order?[Op_Extension(OE)](le(OE))
Op_Extension_exists: LEMMA FORALL (ff:Bounded_Function[a,b]): (NOT member(ff,OE`space) IMPLIES
EXISTS (Ext:Op_Extension(OE)): member(ff,Ext`space))
Hahn_Banach: THEOREM EXISTS (LB): op_norm[a,b,(bounded_on_int?[a,b])](LB) = op_norm[a,b,(continuous_on_int?[a,b])](LC)
AND (FORALL (f:Continuous_Function[a,b]): LB(f) = LC(f))
END riesz_hahn_banach
¤ Dauer der Verarbeitung: 0.1 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.
|
