:: 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 b₁ being Point of (DualSp (DualSp X)) st
for f being Point of (DualSp X) holds b₁ . f = f . x

proof end;

uniqueness
for b₁, b₂ being Point of (DualSp (DualSp X)) st ( for f being Point of (DualSp X) holds b₁ . f = f . x ) & ( for f being Point of (DualSp X) holds b₂ . f = f . x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines BiDual DUALSP02:def 1 :
for X being RealNormSpace
for x being Point of X
for b₃ being Point of (DualSp (DualSp X)) holds
( b₃ = BiDual x iff for f being Point of (DualSp X) holds b₃ . 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 b₁ being Function of X,(DualSp (DualSp X)) st
for x being Point of X holds b₁ . x = BiDual x

proof end;

uniqueness
for b₁, b₂ being Function of X,(DualSp (DualSp X)) st ( for x being Point of X holds b₁ . x = BiDual x ) & ( for x being Point of X holds b₂ . x = BiDual x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines BidualFunc DUALSP02:def 2 :
for X being RealNormSpace
for b₂ being Function of X,(DualSp (DualSp X)) holds
( b₂ = BidualFunc X iff for x being Point of X holds b₂ . 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;