Quelle riesz_hahn_banach.pvs Sprache: PVS

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

quality95%

¤ Dauer der Verarbeitung: 0.13 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.