:: by Keiko Narita , Noboru Endou and Yasunari Shidama

::

:: Received November 29, 2014

:: Copyright (c) 2014-2016 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 ) )

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 )

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.|| )

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.|| )

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 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 ) )

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

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;

ex b_{1} being Point of (DualSp (DualSp X)) st

for f being Point of (DualSp X) holds b_{1} . f = f . x

for b_{1}, b_{2} being Point of (DualSp (DualSp X)) st ( for f being Point of (DualSp X) holds b_{1} . f = f . x ) & ( for f being Point of (DualSp X) holds b_{2} . f = f . x ) holds

b_{1} = b_{2}

end;
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 for f being Point of (DualSp X) holds it . f = f . x;

ex b

for f being Point of (DualSp X) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines BiDual DUALSP02:def 1 :

for X being RealNormSpace

for x being Point of X

for b_{3} being Point of (DualSp (DualSp X)) holds

( b_{3} = BiDual x iff for f being Point of (DualSp X) holds b_{3} . f = f . x );

for X being RealNormSpace

for x being Point of X

for b

( b

definition

let X be RealNormSpace;

ex b_{1} being Function of X,(DualSp (DualSp X)) st

for x being Point of X holds b_{1} . x = BiDual x

for b_{1}, b_{2} being Function of X,(DualSp (DualSp X)) st ( for x being Point of X holds b_{1} . x = BiDual x ) & ( for x being Point of X holds b_{2} . x = BiDual x ) holds

b_{1} = b_{2}

end;
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 for x being Point of X holds it . x = BiDual x;

ex b

for x being Point of X holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines BidualFunc DUALSP02:def 2 :

for X being RealNormSpace

for b_{2} being Function of X,(DualSp (DualSp X)) holds

( b_{2} = BidualFunc X iff for x being Point of X holds b_{2} . x = BiDual x );

for X being RealNormSpace

for b

( b

registration

let X be RealNormSpace;

coherence

( BidualFunc X is additive & BidualFunc X is homogeneous )

end;
coherence

( BidualFunc X is additive & BidualFunc X is homogeneous )

proof 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;

( 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).|| ) )

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

NORMSTR(# REAL,(In (0,REAL)),addreal,multreal,absreal #) is RealNormSpace
end;

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 #);

NORMSTR(# REAL,(In (0,REAL)),addreal,multreal,absreal #) is RealNormSpace

proof end;

:: deftheorem defines RNS_Real DUALSP02:def 3 :

RNS_Real = NORMSTR(# REAL,(In (0,REAL)),addreal,multreal,absreal #);

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

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 )

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 )

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

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

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

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.||

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 ) )

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 )

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
end;

:: deftheorem defines Reflexive DUALSP02:def 4 :

for X being RealNormSpace holds

( X is Reflexive iff BidualFunc X is onto );

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 )

( 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 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

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

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 ") ) )

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 ) )

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 )

( 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

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;