DUALSP01: Dual Spaces and Hahn-Banach's Theorem

proof end;

end;

definition

let V be RealLinearSpace;
let f be Element of (V *');
let v be VECTOR of V;
:: original: .
redefine func f . v -> Element of REAL ;
coherence

proof end;

end;

theorem :: DUALSP01:6

for V being RealLinearSpace
for f, g, h being VECTOR of (V *') holds
( h = f + g iff for x being VECTOR of V holds h . x = (f . x) + (g . x) )

proof end;

theorem :: DUALSP01:7

for V being RealLinearSpace
for f, h being VECTOR of (V *')
for a being Real holds
( h = a * f iff for x being VECTOR of V holds h . x = a * (f . x) )

proof end;

theorem :: DUALSP01:8

for V being RealLinearSpace holds 0. (V *') = the carrier of V --> 0

proof end;

theorem Th23: :: DUALSP01:9

for X being RealLinearSpace holds the carrier of X --> 0 is linear-Functional of X

proof end;

definition

let X be RealLinearSpace;

func LinearFunctionals X -> Subset of (RealVectSpace the carrier of X) means :Def7: :: DUALSP01:def 6
for x being object holds
( x in it iff x is linear-Functional of X );

proof end;

proof end;

end;

:: deftheorem Def7 defines LinearFunctionals DUALSP01:def 6 :

registration

let X be RealNormSpace;

cluster LinearFunctionals X -> non empty ;

proof end;

end;

registration

let X be RealLinearSpace;

cluster LinearFunctionals X -> non empty functional ;

proof end;

end;

theorem Th17: :: DUALSP01:10

for X being RealLinearSpace holds LinearFunctionals X is linearly-closed

proof end;

theorem :: DUALSP01:11

for X being RealLinearSpace holds RLSStruct(# (LinearFunctionals X),(Zero_ ((LinearFunctionals X),(RealVectSpace the carrier of X))),(Add_ ((LinearFunctionals X),(RealVectSpace the carrier of X))),(Mult_ ((LinearFunctionals X),(RealVectSpace the carrier of X))) #) is Subspace of RealVectSpace the carrier of X by Th17, RSSPACE:11;

registration

let X be RealLinearSpace;

cluster RLSStruct(# (LinearFunctionals X),(Zero_ ((LinearFunctionals X),(RealVectSpace the carrier of X))),(Add_ ((LinearFunctionals X),(RealVectSpace the carrier of X))),(Mult_ ((LinearFunctionals X),(RealVectSpace the carrier of X))) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence by Th17, RSSPACE:11;

end;

definition

let X be RealLinearSpace;

func X *' -> strict RealLinearSpace equals :: DUALSP01:def 7
RLSStruct(# (LinearFunctionals X),(Zero_ ((LinearFunctionals X),(RealVectSpace the carrier of X))),(Add_ ((LinearFunctionals X),(RealVectSpace the carrier of X))),(Mult_ ((LinearFunctionals X),(RealVectSpace the carrier of X))) #);

end;

:: deftheorem defines *' DUALSP01:def 7 :

registration

let X be RealLinearSpace;

cluster X *' -> strict constituted-Functions ;

coherence by MONOID_0:80;

end;

definition

let X be RealLinearSpace;
let f be Element of (X *');
let v be VECTOR of X;
:: original: .
redefine func f . v -> Element of REAL ;
coherence

proof end;

end;

theorem Th20b: :: DUALSP01:12

for X being RealLinearSpace
for f, g, h being VECTOR of (X *') holds
( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )

proof end;

theorem Th21b: :: DUALSP01:13

for X being RealLinearSpace
for f, h being VECTOR of (X *')
for a being Real holds
( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )

proof end;

theorem Th22b: :: DUALSP01:14

for X being RealLinearSpace holds 0. (X *') = the carrier of X --> 0

proof end;

definition

let S be Real_Sequence;
let x be Real;

func S - x -> Real_Sequence means :Def14: :: DUALSP01:def 8
for n being Nat holds it . n = (S . n) - x;

proof end;

proof end;

end;

:: deftheorem Def14 defines - DUALSP01:def 8 :

theorem Th121: :: DUALSP01:15

for S being Real_Sequence
for x being Real st S is convergent holds
( S - x is convergent & lim (S - x) = (lim S) - x )

proof end;

definition

let X be RealNormSpace;
let IT be Functional of X;

attr IT is Lipschitzian means :Def8: :: DUALSP01:def 9
ex K being Real st
( 0 <= K & ( for x being VECTOR of X holds |.(IT . x).| <= K * ||.x.|| ) );

end;

:: deftheorem Def8 defines Lipschitzian DUALSP01:def 9 :

theorem Th21: :: DUALSP01:16

for X being RealNormSpace
for f being Functional of X st ( for x being VECTOR of X holds f . x = 0 ) holds
f is Lipschitzian

proof end;

Th21X: for X being RealNormSpace
for F being Functional of X st F = the carrier of X --> 0 holds
( F is linear-Functional of X & F is Lipschitzian )

proof end;

registration

let X be RealNormSpace;

cluster Relation-like the carrier of X -defined REAL -valued non empty Function-like V25( the carrier of X) quasi_total V156() V157() V158() subadditive additive homogeneous positively_homogeneous Lipschitzian for Element of bool [: the carrier of X,REAL:];

proof end;

end;

definition

let X be RealNormSpace;

func BoundedLinearFunctionals X -> Subset of (X *') means :Def9: :: DUALSP01:def 10
for x being set holds
( x in it iff x is Lipschitzian linear-Functional of X );

proof end;

proof end;

end;

:: deftheorem Def9 defines BoundedLinearFunctionals DUALSP01:def 10 :

registration

let X be RealNormSpace;

cluster BoundedLinearFunctionals X -> non empty ;

proof end;

end;

theorem Th22: :: DUALSP01:17

for X being RealNormSpace holds BoundedLinearFunctionals X is linearly-closed

proof end;

theorem :: DUALSP01:18

for X being RealNormSpace holds RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is Subspace of X *' by Th22, RSSPACE:11;

registration

let X be RealNormSpace;

cluster RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence by Th22, RSSPACE:11;

end;

definition

let X be RealNormSpace;

func R_VectorSpace_of_BoundedLinearFunctionals X -> strict RealLinearSpace equals :: DUALSP01:def 11
RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #);

end;

:: deftheorem defines R_VectorSpace_of_BoundedLinearFunctionals DUALSP01:def 11 :

registration

let X be RealNormSpace;

cluster -> Relation-like Function-like for Element of the carrier of (R_VectorSpace_of_BoundedLinearFunctionals X);

end;

definition

let X be RealNormSpace;
let f be Element of (R_VectorSpace_of_BoundedLinearFunctionals X);
let v be VECTOR of X;
:: original: .
redefine func f . v -> Element of REAL ;
coherence

proof end;

end;

theorem Th24: :: DUALSP01:19

for X being RealNormSpace
for f, g, h being VECTOR of (R_VectorSpace_of_BoundedLinearFunctionals X) holds
( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )

proof end;

theorem Th25: :: DUALSP01:20

for X being RealNormSpace
for f, h being VECTOR of (R_VectorSpace_of_BoundedLinearFunctionals X)
for a being Real holds
( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )

proof end;

theorem Th26: :: DUALSP01:21

for X being RealNormSpace holds 0. (R_VectorSpace_of_BoundedLinearFunctionals X) = the carrier of X --> 0

proof end;

definition

let X be RealNormSpace;
let f be object ;

func Bound2Lipschitz (f,X) -> Lipschitzian linear-Functional of X equals :: DUALSP01:def 12
In (f,(BoundedLinearFunctionals X));

coherence by Def9;

end;

:: deftheorem defines Bound2Lipschitz DUALSP01:def 12 :

definition

let X be RealNormSpace;
let u be linear-Functional of X;

func PreNorms u -> non empty Subset of REAL equals :: DUALSP01:def 13
{ |.(u . t).| where t is VECTOR of X : ||.t.|| <= 1 } ;

proof end;

end;

:: deftheorem defines PreNorms DUALSP01:def 13 :

Th27: for X being RealNormSpace
for g being Lipschitzian linear-Functional of X holds PreNorms g is bounded_above

proof end;

registration

let X be RealNormSpace;
let g be Lipschitzian linear-Functional of X;

cluster PreNorms g -> non empty bounded_above ;

coherence by Th27;

end;

theorem :: DUALSP01:22

for X being RealNormSpace
for g being linear-Functional of X holds
( g is Lipschitzian iff PreNorms g is bounded_above )

proof end;

definition

let X be RealNormSpace;

func BoundedLinearFunctionalsNorm X -> Function of (BoundedLinearFunctionals X),REAL means :Def13: :: DUALSP01:def 14
for x being object st x in BoundedLinearFunctionals X holds
it . x = upper_bound (PreNorms (Bound2Lipschitz (x,X)));

proof end;

proof end;

end;

:: deftheorem Def13 defines BoundedLinearFunctionalsNorm DUALSP01:def 14 :

theorem Th29: :: DUALSP01:23

for X being RealNormSpace
for f being Lipschitzian linear-Functional of X holds Bound2Lipschitz (f,X) = f

proof end;

theorem Th30: :: DUALSP01:24

for X being RealNormSpace
for f being Lipschitzian linear-Functional of X holds (BoundedLinearFunctionalsNorm X) . f = upper_bound (PreNorms f)

proof end;

definition

let X be RealNormSpace;

func DualSp X -> non empty NORMSTR equals :: DUALSP01:def 15
NORMSTR(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))),(BoundedLinearFunctionalsNorm X) #);

end;

:: deftheorem defines DualSp DUALSP01:def 15 :

theorem Th31: :: DUALSP01:25

for X being RealNormSpace holds the carrier of X --> 0 = 0. (DualSp X)

proof end;

theorem Th32: :: DUALSP01:26

for X being RealNormSpace
for f being Point of (DualSp X)
for g being Lipschitzian linear-Functional of X st g = f holds
for t being VECTOR of X holds |.(g . t).| <= ||.f.|| * ||.t.||

proof end;

theorem Th33: :: DUALSP01:27

for X being RealNormSpace
for f being Point of (DualSp X) holds 0 <= ||.f.||

proof end;

theorem Th34: :: DUALSP01:28

for X, Y being RealNormSpace
for f being Point of (DualSp X) st f = 0. (DualSp X) holds
0 = ||.f.||

proof end;

registration

let X be RealNormSpace;

cluster -> Relation-like Function-like for Element of the carrier of (DualSp X);

end;

definition

let X be RealNormSpace;
let f be Element of (DualSp X);
let v be VECTOR of X;
:: original: .
redefine func f . v -> Element of REAL ;
coherence

proof end;

end;

theorem Th35: :: DUALSP01:29

for X being RealNormSpace
for f, g, h being Point of (DualSp X) holds
( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )

proof end;

theorem Th36: :: DUALSP01:30

for X being RealNormSpace
for f, h being Point of (DualSp X)
for a being Real holds
( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )

proof end;

theorem Th37: :: DUALSP01:31

for X being RealNormSpace
for f, g being Point of (DualSp X)
for a being Real holds
( ( ||.f.|| = 0 implies f = 0. (DualSp X) ) & ( f = 0. (DualSp X) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )

proof end;

registration

let X be RealNormSpace;

cluster DualSp X -> non empty discerning reflexive RealNormSpace-like ;

correctness by Th37;

end;

theorem Th39: :: DUALSP01:32

for X being RealNormSpace holds DualSp X is RealNormSpace

proof end;

registration

let X be RealNormSpace;

cluster DualSp X -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ;

coherence by Th39;

end;

theorem Th40: :: DUALSP01:33

for X being RealNormSpace
for f, g, h being Point of (DualSp X) holds
( h = f - g iff for x being VECTOR of X holds h . x = (f . x) - (g . x) )

proof end;

Lm3: for e being Real
for seq being Real_Sequence st seq is convergent & ex k being Nat st
for i being Nat st k <= i holds
seq . i <= e holds
lim seq <= e

proof end;

definition

let X be RealNormSpace;
let s be sequence of (DualSp X);
let n be Nat;
:: original: .
redefine func s . n -> Element of (DualSp X);
coherence

proof end;

end;

theorem Th42: :: DUALSP01:34

for X being RealNormSpace
for seq being sequence of (DualSp X) st seq is Cauchy_sequence_by_Norm holds
seq is convergent

proof end;

theorem Th43: :: DUALSP01:35

for X being RealNormSpace holds DualSp X is RealBanachSpace

proof end;

registration

let X be RealNormSpace;

cluster DualSp X -> non empty complete ;

coherence by Th43;

end;

definition

let V be RealNormSpace;

mode SubRealNormSpace of V -> RealNormSpace means :DefSubSP: :: DUALSP01:def 16
( the carrier of it c= the carrier of V & 0. it = 0. V & the addF of it = the addF of V || the carrier of it & the Mult of it = the Mult of V | [:REAL, the carrier of it:] & the normF of it = the normF of V | the carrier of it );