:: Bidual Spaces and Reflexivity of Real Normed Spaces
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received November 29, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users


theorem Th63: :: DUALSP02:1
for V being RealNormSpace
for X being SubRealNormSpace of V
for x0 being Point of V
for d being Real st ex Z being non empty Subset of REAL st
( Z = { ||.(x - x0).|| where x is Point of V : x in X } & d = lower_bound Z & lower_bound Z > 0 ) holds
( not x0 in X & ex G being Point of (DualSp V) st
( ( for x being Point of V st x in X holds
(Bound2Lipschitz (G,V)) . x = 0 ) & (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / d ) )
proof end;

theorem Lm64: :: DUALSP02:2
for V being RealNormSpace
for Y being non empty Subset of V
for x0 being Point of V st Y is linearly-closed & Y is closed & not x0 in Y holds
ex G being Point of (DualSp V) st
( ( for x being Point of V st x in Y holds
(Bound2Lipschitz (G,V)) . x = 0 ) & (Bound2Lipschitz (G,V)) . x0 = 1 )
proof end;

theorem Lm65a: :: DUALSP02:3
for V being RealNormSpace
for x0 being Point of V st x0 <> 0. V holds
ex G being Point of (DualSp V) st
( (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / ||.x0.|| )
proof end;

theorem Lm65: :: DUALSP02:4
for V being RealNormSpace
for x0 being Point of V st x0 <> 0. V holds
ex F being Point of (DualSp V) st
( ||.F.|| = 1 & (Bound2Lipschitz (F,V)) . x0 = ||.x0.|| )
proof end;

theorem Lm65A: :: DUALSP02:5
for V being RealNormSpace st not V is trivial holds
ex F being Point of (DualSp V) st ||.F.|| = 1
proof end;

theorem Lm65A1: :: DUALSP02:6
for V being RealNormSpace st not V is trivial holds
not DualSp V is trivial
proof end;

theorem Th71: :: DUALSP02:7
for V being RealNormSpace
for x being Point of V st not V is trivial holds
( ex X being non empty Subset of REAL st
( X = { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| = 1 } & ||.x.|| = upper_bound X ) & ex Y being non empty Subset of REAL st
( Y = { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| <= 1 } & ||.x.|| = upper_bound Y ) )
proof end;

theorem Lm72: :: DUALSP02:8
for V being RealNormSpace
for x being Point of V st ( for f being Lipschitzian linear-Functional of V holds f . x = 0 ) holds
x = 0. V
proof end;

definition
let X be RealNormSpace;
let x be Point of X;
func BiDual x -> Point of (DualSp (DualSp X)) means :Def1: :: DUALSP02:def 1
for f being Point of (DualSp X) holds it . f = f . x;
existence
ex b1 being Point of (DualSp (DualSp X)) st
for f being Point of (DualSp X) holds b1 . f = f . x
proof end;
uniqueness
for b1, b2 being Point of (DualSp (DualSp X)) st ( for f being Point of (DualSp X) holds b1 . f = f . x ) & ( for f being Point of (DualSp X) holds b2 . f = f . x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines BiDual DUALSP02:def 1 :
for X being RealNormSpace
for x being Point of X
for b3 being Point of (DualSp (DualSp X)) holds
( b3 = BiDual x iff for f being Point of (DualSp X) holds b3 . f = f . x );

definition
let X be RealNormSpace;
func BidualFunc X -> Function of X,(DualSp (DualSp X)) means :Def2: :: DUALSP02:def 2
for x being Point of X holds it . x = BiDual x;
existence
ex b1 being Function of X,(DualSp (DualSp X)) st
for x being Point of X holds b1 . x = BiDual x
proof end;
uniqueness
for b1, b2 being Function of X,(DualSp (DualSp X)) st ( for x being Point of X holds b1 . x = BiDual x ) & ( for x being Point of X holds b2 . x = BiDual x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines BidualFunc DUALSP02:def 2 :
for X being RealNormSpace
for b2 being Function of X,(DualSp (DualSp X)) holds
( b2 = BidualFunc X iff for x being Point of X holds b2 . x = BiDual x );

registration
let X be RealNormSpace;
cluster BidualFunc X -> additive homogeneous ;
coherence
( BidualFunc X is additive & BidualFunc X is homogeneous )
proof end;
end;

registration
let X be RealNormSpace;
cluster BidualFunc X -> one-to-one ;
coherence
BidualFunc X is one-to-one
proof end;
end;

LMNORM: for X being RealNormSpace
for x being Point of X st not X is trivial holds
||.x.|| = ||.((BidualFunc X) . x).||

proof end;

theorem :: DUALSP02:9
for X being RealNormSpace st not X is trivial holds
( BidualFunc X is LinearOperator of X,(DualSp (DualSp X)) & ( for x being Point of X holds ||.x.|| = ||.((BidualFunc X) . x).|| ) ) by LMNORM;

theorem IMDDX: :: DUALSP02:10
for X being RealNormSpace st not X is trivial holds
ex DuX being SubRealNormSpace of DualSp (DualSp X) ex L being Lipschitzian LinearOperator of X,DuX st
( L is bijective & DuX = Im (BidualFunc X) & ( for x being Point of X holds L . x = BiDual x ) & ( for x being Point of X holds ||.x.|| = ||.(L . x).|| ) )
proof end;

definition
func RNS_Real -> RealNormSpace equals :: DUALSP02:def 3
NORMSTR(# REAL,(In (0,REAL)),addreal,multreal,absreal #);
coherence
NORMSTR(# REAL,(In (0,REAL)),addreal,multreal,absreal #) is RealNormSpace
proof end;
end;

:: deftheorem defines RNS_Real DUALSP02:def 3 :
RNS_Real = NORMSTR(# REAL,(In (0,REAL)),addreal,multreal,absreal #);

theorem :: DUALSP02:11
for X being RealNormSpace
for x being Element of REAL
for v being Point of RNS_Real st x = v holds
- x = - v
proof end;

theorem LMN6: :: DUALSP02:12
for X being RealNormSpace
for x being object holds
( x is additive homogeneous Function of X,REAL iff x is additive homogeneous Function of X,RNS_Real )
proof end;

theorem LMN7: :: DUALSP02:13
for X being RealNormSpace
for x being object holds
( x is additive homogeneous Lipschitzian Function of X,REAL iff x is additive homogeneous Lipschitzian Function of X,RNS_Real )
proof end;

theorem Th75A: :: DUALSP02:14
for X being RealNormSpace holds the carrier of (DualSp X) = the carrier of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real))
proof end;

theorem :: DUALSP02:15
for X being RealNormSpace
for x, y being Point of (DualSp X)
for v, w being Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st x = v & y = w holds
x + y = v + w
proof end;

theorem LMN9: :: DUALSP02:16
for X being RealNormSpace
for a being Element of REAL
for x being Point of (DualSp X)
for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st x = v holds
a * x = a * v
proof end;

theorem :: DUALSP02:17
for X being RealNormSpace
for x being Point of (DualSp X)
for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st x = v holds
- x = - v
proof end;

theorem LMN11: :: DUALSP02:18
for X being RealNormSpace
for x being Point of (DualSp X)
for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st x = v holds
||.x.|| = ||.v.||
proof end;

theorem Th75: :: DUALSP02:19
for X being RealNormSpace
for L being Subset of X st not X is trivial & ( for f being Point of (DualSp X) ex Kf being Real st
( 0 <= Kf & ( for x being Point of X st x in L holds
|.(f . x).| <= Kf ) ) ) holds
ex M being Real st
( 0 <= M & ( for x being Point of X st x in L holds
||.x.|| <= M ) )
proof end;

theorem :: DUALSP02:20
for X being RealNormSpace
for L being non empty Subset of X st not X is trivial & ( for f being Point of (DualSp X) ex Y1 being Subset of REAL st
( Y1 = { |.(f . x).| where x is Point of X : x in L } & sup Y1 < +infty ) ) holds
ex Y being Subset of REAL st
( Y = { ||.x.|| where x is Point of X : x in L } & sup Y < +infty )
proof end;

definition
let X be RealNormSpace;
attr X is Reflexive means :: DUALSP02:def 4
BidualFunc X is onto ;
end;

:: deftheorem defines Reflexive DUALSP02:def 4 :
for X being RealNormSpace holds
( X is Reflexive iff BidualFunc X is onto );

theorem REFF1: :: DUALSP02:21
for X being RealNormSpace holds
( X is Reflexive iff for f being Point of (DualSp (DualSp X)) ex x being Point of X st
for g being Point of (DualSp X) holds f . g = g . x )
proof end;

theorem :: DUALSP02:22
for X being RealNormSpace holds
( X is Reflexive iff Im (BidualFunc X) = DualSp (DualSp X) )
proof end;

theorem :: DUALSP02:23
for X being RealNormSpace st not X is trivial & X is Reflexive holds
X is RealBanachSpace
proof end;

theorem Th76: :: DUALSP02:24
for X being RealBanachSpace
for M being non empty Subset of X st X is Reflexive & M is linearly-closed & M is closed holds
NLin M is Reflexive
proof end;

theorem NISOM08: :: DUALSP02:25
for X, Y being RealNormSpace
for L being Lipschitzian LinearOperator of X,Y
for y being Lipschitzian linear-Functional of Y holds y * L is Lipschitzian linear-Functional of X
proof end;

theorem NISOM09: :: DUALSP02:26
for X, Y being RealNormSpace
for L being Lipschitzian LinearOperator of X,Y st L is isomorphism holds
ex T being Lipschitzian LinearOperator of (DualSp X),(DualSp Y) st
( T is isomorphism & ( for x being Point of (DualSp X) holds T . x = x * (L ") ) )
proof end;

NISOM11: for X, Y being RealNormSpace st ex L being Lipschitzian LinearOperator of X,Y st L is isomorphism & X is Reflexive holds
Y is Reflexive

proof end;

theorem :: DUALSP02:27
for X, Y being RealNormSpace
for L being Lipschitzian LinearOperator of X,Y
for T being Lipschitzian LinearOperator of (DualSp X),(DualSp Y) st L is isomorphism & T is isomorphism & ( for x being Point of (DualSp X) holds T . x = x * (L ") ) holds
ex S being Lipschitzian LinearOperator of (DualSp Y),(DualSp X) st
( S is isomorphism & S = T " & ( for y being Point of (DualSp Y) holds S . y = y * L ) )
proof end;

theorem NISOM12: :: DUALSP02:28
for X, Y being RealNormSpace st ex L being Lipschitzian LinearOperator of X,Y st L is isomorphism holds
( X is Reflexive iff Y is Reflexive )
proof end;

theorem Th74A: :: DUALSP02:29
for X being RealNormSpace st not X is trivial holds
ex L being Lipschitzian LinearOperator of X,(Im (BidualFunc X)) st L is isomorphism
proof end;

Lm77R: for X being RealBanachSpace st not X is trivial & X is Reflexive holds
DualSp X is Reflexive

proof end;

theorem :: DUALSP02:30
for X being RealBanachSpace st not X is trivial holds
( X is Reflexive iff DualSp X is Reflexive )
proof end;