:: Bidual Spaces and Reflexivity of Real Normed Spaces
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Copyright (c) 2014-2019 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 () st
( ( for x being Point of V st x in X holds
(Bound2Lipschitz (G,V)) . x = 0 ) & (Bound2Lipschitz (G,V)) . x0 = 1 & = 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 () 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 () st
( (Bound2Lipschitz (G,V)) . x0 = 1 & = 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 () st
( = 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 () st = 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 () : = 1 } & = upper_bound X ) & ex Y being non empty Subset of REAL st
( Y = { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of () : <= 1 } & = 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 ()) means :Def1: :: DUALSP02:def 1
for f being Point of () holds it . f = f . x;
existence
ex b1 being Point of (DualSp ()) st
for f being Point of () holds b1 . f = f . x
proof end;
uniqueness
for b1, b2 being Point of (DualSp ()) st ( for f being Point of () holds b1 . f = f . x ) & ( for f being Point of () 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 ()) holds
( b3 = BiDual x iff for f being Point of () holds b3 . f = f . x );

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

registration
let X be RealNormSpace;
coherence
proof end;
end;

registration
let X be RealNormSpace;
coherence
proof end;
end;

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

proof end;

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

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

definition
func RNS_Real -> RealNormSpace equals :: DUALSP02:def 3
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 () = the carrier of
proof end;

theorem :: DUALSP02:15
for X being RealNormSpace
for x, y being Point of ()
for v, w being Point of 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 ()
for v being Point of st x = v holds
a * x = a * v
proof end;

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

theorem LMN11: :: DUALSP02:18
for X being RealNormSpace
for x being Point of ()
for v being Point of st x = v holds
=
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 () 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
<= 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 () 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 = { 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 ()) ex x being Point of X st
for g being Point of () holds f . g = g . x )
proof end;

theorem :: DUALSP02:22
for X being RealNormSpace holds
( X is Reflexive iff Im () = DualSp () )
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 (),() st
( T is isomorphism & ( for x being Point of () 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 (),() st L is isomorphism & T is isomorphism & ( for x being Point of () holds T . x = x * (L ") ) holds
ex S being Lipschitzian LinearOperator of (),() st
( S is isomorphism & S = T " & ( for y being Point of () 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 ()) 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;