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