:: by Keiko Narita , Noboru Endou and Yasunari Shidama

::

:: Received March 31, 2014

:: Copyright (c) 2014-2016 Association of Mizar Users

definition

let X be RealLinearSpace;

coherence

the Mult of X is Function of [: the carrier of F_Real, the carrier of X:], the carrier of X;

;

end;
func MultF_Real* X -> Function of [: the carrier of F_Real, the carrier of X:], the carrier of X equals :: DUALSP01:def 1

the Mult of X;

correctness the Mult of X;

coherence

the Mult of X is Function of [: the carrier of F_Real, the carrier of X:], the carrier of X;

;

:: deftheorem defines MultF_Real* DUALSP01:def 1 :

for X being RealLinearSpace holds MultF_Real* X = the Mult of X;

for X being RealLinearSpace holds MultF_Real* X = the Mult of X;

theorem Lm01: :: DUALSP01:1

for X being RealLinearSpace holds ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) is VectSp of F_Real

proof end;

definition

let X be RealLinearSpace;

coherence

ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) is VectSp of F_Real ;

by Lm01;

end;
func RLSp2RVSp X -> VectSp of F_Real equals :: DUALSP01:def 2

ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #);

correctness ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #);

coherence

ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) is VectSp of F_Real ;

by Lm01;

:: deftheorem defines RLSp2RVSp DUALSP01:def 2 :

for X being RealLinearSpace holds RLSp2RVSp X = ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #);

for X being RealLinearSpace holds RLSp2RVSp X = ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #);

definition

let X be ModuleStr over F_Real ;

coherence

the lmult of X is Function of [:REAL, the carrier of X:], the carrier of X;

;

end;
func MultReal* X -> Function of [:REAL, the carrier of X:], the carrier of X equals :: DUALSP01:def 3

the lmult of X;

correctness the lmult of X;

coherence

the lmult of X is Function of [:REAL, the carrier of X:], the carrier of X;

;

:: deftheorem defines MultReal* DUALSP01:def 3 :

for X being ModuleStr over F_Real holds MultReal* X = the lmult of X;

for X being ModuleStr over F_Real holds MultReal* X = the lmult of X;

theorem Lm02: :: DUALSP01:2

for X being VectSp of F_Real holds RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is RealLinearSpace

proof end;

definition

let X be VectSp of F_Real ;

coherence

RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is RealLinearSpace;

by Lm02;

end;
func RVSp2RLSp X -> RealLinearSpace equals :: DUALSP01:def 4

RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #);

correctness RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #);

coherence

RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is RealLinearSpace;

by Lm02;

:: deftheorem defines RVSp2RLSp DUALSP01:def 4 :

for X being VectSp of F_Real holds RVSp2RLSp X = RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #);

for X being VectSp of F_Real holds RVSp2RLSp X = RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #);

theorem :: DUALSP01:3

for X being RealLinearSpace

for v, w being Element of X

for v1, w1 being Element of (RLSp2RVSp X) st v = v1 & w = w1 holds

( v + w = v1 + w1 & v - w = v1 - w1 )

for v, w being Element of X

for v1, w1 being Element of (RLSp2RVSp X) st v = v1 & w = w1 holds

( v + w = v1 + w1 & v - w = v1 - w1 )

proof end;

theorem :: DUALSP01:4

for X being VectSp of F_Real

for v, w being Element of X

for v1, w1 being Element of (RVSp2RLSp X) st v = v1 & w = w1 holds

( v + w = v1 + w1 & v - w = v1 - w1 )

for v, w being Element of X

for v1, w1 being Element of (RVSp2RLSp X) st v = v1 & w = w1 holds

( v + w = v1 + w1 & v - w = v1 - w1 )

proof end;

definition

let V be RealLinearSpace;

existence

ex b_{1} being strict RealLinearSpace ex X being VectSp of F_Real st

( X = RLSp2RVSp V & b_{1} = RVSp2RLSp (X *') );

uniqueness

for b_{1}, b_{2} being strict RealLinearSpace st ex X being VectSp of F_Real st

( X = RLSp2RVSp V & b_{1} = RVSp2RLSp (X *') ) & ex X being VectSp of F_Real st

( X = RLSp2RVSp V & b_{2} = RVSp2RLSp (X *') ) holds

b_{1} = b_{2};

end;
func V *' -> strict RealLinearSpace means :def2: :: DUALSP01:def 5

ex X being VectSp of F_Real st

( X = RLSp2RVSp V & it = RVSp2RLSp (X *') );

correctness ex X being VectSp of F_Real st

( X = RLSp2RVSp V & it = RVSp2RLSp (X *') );

existence

ex b

( X = RLSp2RVSp V & b

uniqueness

for b

( X = RLSp2RVSp V & b

( X = RLSp2RVSp V & b

b

proof end;

:: deftheorem def2 defines *' DUALSP01:def 5 :

for V being RealLinearSpace

for b_{2} being strict RealLinearSpace holds

( b_{2} = V *' iff ex X being VectSp of F_Real st

( X = RLSp2RVSp V & b_{2} = RVSp2RLSp (X *') ) );

for V being RealLinearSpace

for b

( b

( X = RLSp2RVSp V & b

theorem Th1: :: DUALSP01:5

for V being RealLinearSpace

for x being object holds

( x in the carrier of (V *') iff x is linear-Functional of V )

for x being object holds

( x in the carrier of (V *') iff x is linear-Functional of V )

proof 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

f . v is Element of REAL

end;
let f be Element of (V *');

let v be VECTOR of V;

:: original: .

redefine func f . v -> Element of REAL ;

coherence

f . v is Element of REAL

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

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

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;

definition

let X be RealLinearSpace;

ex b_{1} being Subset of (RealVectSpace the carrier of X) st

for x being object holds

( x in b_{1} iff x is linear-Functional of X )

for b_{1}, b_{2} being Subset of (RealVectSpace the carrier of X) st ( for x being object holds

( x in b_{1} iff x is linear-Functional of X ) ) & ( for x being object holds

( x in b_{2} iff x is linear-Functional of X ) ) holds

b_{1} = b_{2}

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

existence for x being object holds

( x in it iff x is linear-Functional of X );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def7 defines LinearFunctionals DUALSP01:def 6 :

for X being RealLinearSpace

for b_{2} being Subset of (RealVectSpace the carrier of X) holds

( b_{2} = LinearFunctionals X iff for x being object holds

( x in b_{2} iff x is linear-Functional of X ) );

for X being RealLinearSpace

for b

( b

( x in b

registration

let X be RealLinearSpace;

coherence

( not LinearFunctionals X is empty & LinearFunctionals X is functional )

end;
coherence

( not LinearFunctionals X is empty & LinearFunctionals X is functional )

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;

( 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 Abelian & 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 add-associative & 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 right_zeroed & 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 right_complementable & 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 scalar-distributive & 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 vector-distributive & 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 scalar-associative & 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 scalar-unital ) by Th17, RSSPACE:11;

end;
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 ( 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 Abelian & 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 add-associative & 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 right_zeroed & 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 right_complementable & 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 scalar-distributive & 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 vector-distributive & 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 scalar-associative & 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 scalar-unital ) by Th17, RSSPACE:11;

definition

let X be RealLinearSpace;

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 strict RealLinearSpace ;

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

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

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 strict RealLinearSpace ;

:: deftheorem defines *' DUALSP01:def 7 :

for X being RealLinearSpace holds X *' = 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))) #);

for X being RealLinearSpace holds X *' = 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))) #);

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

f . v is Element of REAL

end;
let f be Element of (X *');

let v be VECTOR of X;

:: original: .

redefine func f . v -> Element of REAL ;

coherence

f . v is Element of REAL

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

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

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;

definition

let S be Real_Sequence;

let x be Real;

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = (S . n) - x

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = (S . n) - x ) & ( for n being Nat holds b_{2} . n = (S . n) - x ) holds

b_{1} = b_{2}

end;
let x be Real;

func S - x -> Real_Sequence means :Def14: :: DUALSP01:def 8

for n being Nat holds it . n = (S . n) - x;

existence for n being Nat holds it . n = (S . n) - x;

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def14 defines - DUALSP01:def 8 :

for S being Real_Sequence

for x being Real

for b_{3} being Real_Sequence holds

( b_{3} = S - x iff for n being Nat holds b_{3} . n = (S . n) - x );

for S being Real_Sequence

for x being Real

for b

( b

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 )

for x being Real st S is convergent holds

( S - x is convergent & lim (S - x) = (lim S) - x )

proof end;

:: deftheorem Def8 defines Lipschitzian DUALSP01:def 9 :

for X being RealNormSpace

for IT being Functional of X holds

( IT is Lipschitzian iff ex K being Real st

( 0 <= K & ( for x being VECTOR of X holds |.(IT . x).| <= K * ||.x.|| ) ) );

for X being RealNormSpace

for IT being Functional of X holds

( IT is Lipschitzian iff ex K being Real st

( 0 <= K & ( for x being VECTOR of X holds |.(IT . x).| <= K * ||.x.|| ) ) );

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

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;

ex b_{1} being linear-Functional of X st b_{1} is Lipschitzian

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

existence ex b

proof end;

definition

let X be RealNormSpace;

ex b_{1} being Subset of (X *') st

for x being set holds

( x in b_{1} iff x is Lipschitzian linear-Functional of X )

for b_{1}, b_{2} being Subset of (X *') st ( for x being set holds

( x in b_{1} iff x is Lipschitzian linear-Functional of X ) ) & ( for x being set holds

( x in b_{2} iff x is Lipschitzian linear-Functional of X ) ) holds

b_{1} = b_{2}

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

existence for x being set holds

( x in it iff x is Lipschitzian linear-Functional of X );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def9 defines BoundedLinearFunctionals DUALSP01:def 10 :

for X being RealNormSpace

for b_{2} being Subset of (X *') holds

( b_{2} = BoundedLinearFunctionals X iff for x being set holds

( x in b_{2} iff x is Lipschitzian linear-Functional of X ) );

for X being RealNormSpace

for b

( b

( x in b

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

( RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is Abelian & RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is add-associative & RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is right_zeroed & RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is right_complementable & RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is vector-distributive & RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is scalar-distributive & RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is scalar-associative & RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is scalar-unital ) by Th22, RSSPACE:11;

end;
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 ( RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is Abelian & RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is add-associative & RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is right_zeroed & RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is right_complementable & RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is vector-distributive & RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is scalar-distributive & RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is scalar-associative & RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is scalar-unital ) by Th22, RSSPACE:11;

definition

let X be RealNormSpace;

RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is strict RealLinearSpace ;

end;
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 *'))) #);

coherence RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #);

RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is strict RealLinearSpace ;

:: deftheorem defines R_VectorSpace_of_BoundedLinearFunctionals DUALSP01:def 11 :

for X being RealNormSpace holds R_VectorSpace_of_BoundedLinearFunctionals X = RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #);

for X being RealNormSpace holds R_VectorSpace_of_BoundedLinearFunctionals X = RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #);

registration

let X be RealNormSpace;

for b_{1} being Element of (R_VectorSpace_of_BoundedLinearFunctionals X) holds

( b_{1} is Function-like & b_{1} is Relation-like )
;

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

coherence for b

( b

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

f . v is Element of REAL

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

f . v is Element of REAL

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

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

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 ;

In (f,(BoundedLinearFunctionals X)) is Lipschitzian linear-Functional of X by Def9;

end;
let f be object ;

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

In (f,(BoundedLinearFunctionals X));

coherence In (f,(BoundedLinearFunctionals X));

In (f,(BoundedLinearFunctionals X)) is Lipschitzian linear-Functional of X by Def9;

:: deftheorem defines Bound2Lipschitz DUALSP01:def 12 :

for X being RealNormSpace

for f being object holds Bound2Lipschitz (f,X) = In (f,(BoundedLinearFunctionals X));

for X being RealNormSpace

for f being object holds Bound2Lipschitz (f,X) = In (f,(BoundedLinearFunctionals X));

definition

let X be RealNormSpace;

let u be linear-Functional of X;

{ |.(u . t).| where t is VECTOR of X : ||.t.|| <= 1 } is non empty Subset of REAL

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

coherence { |.(u . t).| where t is VECTOR of X : ||.t.|| <= 1 } ;

{ |.(u . t).| where t is VECTOR of X : ||.t.|| <= 1 } is non empty Subset of REAL

proof end;

:: deftheorem defines PreNorms DUALSP01:def 13 :

for X being RealNormSpace

for u being linear-Functional of X holds PreNorms u = { |.(u . t).| where t is VECTOR of X : ||.t.|| <= 1 } ;

for X being RealNormSpace

for u being linear-Functional of X holds PreNorms u = { |.(u . t).| where t is VECTOR of X : ||.t.|| <= 1 } ;

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;

coherence

PreNorms g is bounded_above by Th27;

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

coherence

PreNorms g is bounded_above by Th27;

theorem :: DUALSP01:22

for X being RealNormSpace

for g being linear-Functional of X holds

( g is Lipschitzian iff PreNorms g is bounded_above )

for g being linear-Functional of X holds

( g is Lipschitzian iff PreNorms g is bounded_above )

proof end;

definition

let X be RealNormSpace;

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

for x being object st x in BoundedLinearFunctionals X holds

b_{1} . x = upper_bound (PreNorms (Bound2Lipschitz (x,X)))

for b_{1}, b_{2} being Function of (BoundedLinearFunctionals X),REAL st ( for x being object st x in BoundedLinearFunctionals X holds

b_{1} . x = upper_bound (PreNorms (Bound2Lipschitz (x,X))) ) & ( for x being object st x in BoundedLinearFunctionals X holds

b_{2} . x = upper_bound (PreNorms (Bound2Lipschitz (x,X))) ) holds

b_{1} = b_{2}

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

existence for x being object st x in BoundedLinearFunctionals X holds

it . x = upper_bound (PreNorms (Bound2Lipschitz (x,X)));

ex b

for x being object st x in BoundedLinearFunctionals X holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def13 defines BoundedLinearFunctionalsNorm DUALSP01:def 14 :

for X being RealNormSpace

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

( b_{2} = BoundedLinearFunctionalsNorm X iff for x being object st x in BoundedLinearFunctionals X holds

b_{2} . x = upper_bound (PreNorms (Bound2Lipschitz (x,X))) );

for X being RealNormSpace

for b

( b

b

theorem Th29: :: DUALSP01:23

for X being RealNormSpace

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

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)

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

proof end;

definition

let X be RealNormSpace;

NORMSTR(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))),(BoundedLinearFunctionalsNorm X) #) is non empty NORMSTR ;

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

coherence NORMSTR(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))),(BoundedLinearFunctionalsNorm X) #);

NORMSTR(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))),(BoundedLinearFunctionalsNorm X) #) is non empty NORMSTR ;

:: deftheorem defines DualSp DUALSP01:def 15 :

for X being RealNormSpace holds DualSp X = NORMSTR(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))),(BoundedLinearFunctionalsNorm X) #);

for X being RealNormSpace holds DualSp X = NORMSTR(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))),(BoundedLinearFunctionalsNorm X) #);

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

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;

registration

let X be RealNormSpace;

coherence

for b_{1} being Element of (DualSp X) holds

( b_{1} is Function-like & b_{1} is Relation-like )
;

end;
coherence

for b

( b

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

f . v is Element of REAL

end;
let f be Element of (DualSp X);

let v be VECTOR of X;

:: original: .

redefine func f . v -> Element of REAL ;

coherence

f . v is Element of REAL

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

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

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

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;

correctness

coherence

( DualSp X is reflexive & DualSp X is discerning & DualSp X is RealNormSpace-like );

by Th37;

end;
correctness

coherence

( DualSp X is reflexive & DualSp X is discerning & DualSp X is RealNormSpace-like );

by Th37;

registration

let X be RealNormSpace;

( DualSp X is reflexive & DualSp X is discerning & DualSp X is RealNormSpace-like & DualSp X is vector-distributive & DualSp X is scalar-distributive & DualSp X is scalar-associative & DualSp X is scalar-unital & DualSp X is Abelian & DualSp X is add-associative & DualSp X is right_zeroed & DualSp X is right_complementable ) by Th39;

end;
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 ( DualSp X is reflexive & DualSp X is discerning & DualSp X is RealNormSpace-like & DualSp X is vector-distributive & DualSp X is scalar-distributive & DualSp X is scalar-associative & DualSp X is scalar-unital & DualSp X is Abelian & DualSp X is add-associative & DualSp X is right_zeroed & DualSp X is right_complementable ) by Th39;

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

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

s . n is Element of (DualSp X)

end;
let s be sequence of (DualSp X);

let n be Nat;

:: original: .

redefine func s . n -> Element of (DualSp X);

coherence

s . n is Element of (DualSp X)

proof 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

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

seq is convergent

proof end;

definition

let V be RealNormSpace;

ex b_{1} being RealNormSpace st

( the carrier of b_{1} c= the carrier of V & 0. b_{1} = 0. V & the addF of b_{1} = the addF of V || the carrier of b_{1} & the Mult of b_{1} = the Mult of V | [:REAL, the carrier of b_{1}:] & the normF of b_{1} = the normF of V | the carrier of b_{1} )

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

existence ( 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 );

ex b

( the carrier of b

proof end;

:: deftheorem DefSubSP defines SubRealNormSpace DUALSP01:def 16 :

for V, b_{2} being RealNormSpace holds

( b_{2} is SubRealNormSpace of V iff ( the carrier of b_{2} c= the carrier of V & 0. b_{2} = 0. V & the addF of b_{2} = the addF of V || the carrier of b_{2} & the Mult of b_{2} = the Mult of V | [:REAL, the carrier of b_{2}:] & the normF of b_{2} = the normF of V | the carrier of b_{2} ) );

for V, b

( b

theorem Th44: :: DUALSP01:36

for V being RealNormSpace

for X being SubRealNormSpace of V

for f being Lipschitzian linear-Functional of X

for F being Point of (DualSp X) st f = F holds

ex g being Lipschitzian linear-Functional of V ex G being Point of (DualSp V) st

( g = G & g | the carrier of X = f & ||.G.|| = ||.F.|| )

for X being SubRealNormSpace of V

for f being Lipschitzian linear-Functional of X

for F being Point of (DualSp X) st f = F holds

ex g being Lipschitzian linear-Functional of V ex G being Point of (DualSp V) st

( g = G & g | the carrier of X = f & ||.G.|| = ||.F.|| )

proof end;

:: Hahn-Banach's extension theorem (real normed spaces)

theorem :: DUALSP01:37

for V being RealNormSpace

for X being SubRealNormSpace of V

for f being Lipschitzian linear-Functional of X

for F being Point of (DualSp X) st f = F & ( for x being VECTOR of X

for v being VECTOR of V st x = v holds

f . x <= ||.v.|| ) holds

ex g being Lipschitzian linear-Functional of V ex G being Point of (DualSp V) st

( g = G & g | the carrier of X = f & ( for x being VECTOR of V holds

( g . x <= ||.x.|| & ||.G.|| = ||.F.|| ) ) )

for X being SubRealNormSpace of V

for f being Lipschitzian linear-Functional of X

for F being Point of (DualSp X) st f = F & ( for x being VECTOR of X

for v being VECTOR of V st x = v holds

f . x <= ||.v.|| ) holds

ex g being Lipschitzian linear-Functional of V ex G being Point of (DualSp V) st

( g = G & g | the carrier of X = f & ( for x being VECTOR of V holds

( g . x <= ||.x.|| & ||.G.|| = ||.F.|| ) ) )

proof end;