:: Banach Space of Bounded Linear Operators :: by Yasunari Shidama :: :: Received December 22, 2003 :: Copyright (c) 2003-2012 Association of Mizar Users begin definition let X be set ; let Y be non empty set ; let F be Function of [:REAL,Y:],Y; let a be real number ; let f be Function of X,Y; :: original:[;] redefine funcF [;] (a,f) -> Element of Funcs (X,Y); coherence F [;] (a,f) is Element of Funcs (X,Y) proofend; end; definition let X be non empty set ; let Y be non empty addLoopStr ; func FuncAdd (X,Y) -> BinOp of (Funcs (X, the carrier of Y)) means :Def1: :: LOPBAN_1:def 1 for f, g being Element of Funcs (X, the carrier of Y) holds it . (f,g) = the addF of Y .: (f,g); existence ex b1 being BinOp of (Funcs (X, the carrier of Y)) st for f, g being Element of Funcs (X, the carrier of Y) holds b1 . (f,g) = the addF of Y .: (f,g) proofend; uniqueness for b1, b2 being BinOp of (Funcs (X, the carrier of Y)) st ( for f, g being Element of Funcs (X, the carrier of Y) holds b1 . (f,g) = the addF of Y .: (f,g) ) & ( for f, g being Element of Funcs (X, the carrier of Y) holds b2 . (f,g) = the addF of Y .: (f,g) ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines FuncAdd LOPBAN_1:def_1_:_ for X being non empty set for Y being non empty addLoopStr for b3 being BinOp of (Funcs (X, the carrier of Y)) holds ( b3 = FuncAdd (X,Y) iff for f, g being Element of Funcs (X, the carrier of Y) holds b3 . (f,g) = the addF of Y .: (f,g) ); definition let X be non empty set ; let Y be RealLinearSpace; func FuncExtMult (X,Y) -> Function of [:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) means :Def2: :: LOPBAN_1:def 2 for a being Real for f being Element of Funcs (X, the carrier of Y) for x being Element of X holds (it . [a,f]) . x = a * (f . x); existence ex b1 being Function of [:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) st for a being Real for f being Element of Funcs (X, the carrier of Y) for x being Element of X holds (b1 . [a,f]) . x = a * (f . x) proofend; uniqueness for b1, b2 being Function of [:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) st ( for a being Real for f being Element of Funcs (X, the carrier of Y) for x being Element of X holds (b1 . [a,f]) . x = a * (f . x) ) & ( for a being Real for f being Element of Funcs (X, the carrier of Y) for x being Element of X holds (b2 . [a,f]) . x = a * (f . x) ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines FuncExtMult LOPBAN_1:def_2_:_ for X being non empty set for Y being RealLinearSpace for b3 being Function of [:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) holds ( b3 = FuncExtMult (X,Y) iff for a being Real for f being Element of Funcs (X, the carrier of Y) for x being Element of X holds (b3 . [a,f]) . x = a * (f . x) ); definition let X be set ; let Y be non empty ZeroStr ; func FuncZero (X,Y) -> Element of Funcs (X, the carrier of Y) equals :: LOPBAN_1:def 3 X --> (0. Y); coherence X --> (0. Y) is Element of Funcs (X, the carrier of Y) by FUNCT_2:8; end; :: deftheorem defines FuncZero LOPBAN_1:def_3_:_ for X being set for Y being non empty ZeroStr holds FuncZero (X,Y) = X --> (0. Y); Lm1: for A, B being non empty set for x being Element of A for f being Function of A,B holds x in dom f proofend; theorem Th1: :: LOPBAN_1:1 for X being non empty set for Y being non empty addLoopStr for f, g, h being Element of Funcs (X, the carrier of Y) holds ( h = (FuncAdd (X,Y)) . (f,g) iff for x being Element of X holds h . x = (f . x) + (g . x) ) proofend; theorem Th2: :: LOPBAN_1:2 for X being non empty set for Y being RealLinearSpace for h, f being Element of Funcs (X, the carrier of Y) for a being Real holds ( h = (FuncExtMult (X,Y)) . [a,f] iff for x being Element of X holds h . x = a * (f . x) ) proofend; theorem Th3: :: LOPBAN_1:3 for X being non empty set for Y being RealLinearSpace for f, g being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,g) = (FuncAdd (X,Y)) . (g,f) proofend; theorem Th4: :: LOPBAN_1:4 for X being non empty set for Y being RealLinearSpace for f, g, h being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,((FuncAdd (X,Y)) . (g,h))) = (FuncAdd (X,Y)) . (((FuncAdd (X,Y)) . (f,g)),h) proofend; theorem Th5: :: LOPBAN_1:5 for X being non empty set for Y being RealLinearSpace for f being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . ((FuncZero (X,Y)),f) = f proofend; theorem Th6: :: LOPBAN_1:6 for X being non empty set for Y being RealLinearSpace for f being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1),f])) = FuncZero (X,Y) proofend; theorem Th7: :: LOPBAN_1:7 for X being non empty set for Y being RealLinearSpace for f being Element of Funcs (X, the carrier of Y) holds (FuncExtMult (X,Y)) . [1,f] = f proofend; theorem Th8: :: LOPBAN_1:8 for X being non empty set for Y being RealLinearSpace for f being Element of Funcs (X, the carrier of Y) for a, b being Real holds (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f] proofend; theorem Th9: :: LOPBAN_1:9 for X being non empty set for Y being RealLinearSpace for f being Element of Funcs (X, the carrier of Y) for a, b being Real holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [b,f])) = (FuncExtMult (X,Y)) . [(a + b),f] proofend; Lm2: for X being non empty set for Y being RealLinearSpace for f, g being Element of Funcs (X, the carrier of Y) for a being Real holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [a,g])) = (FuncExtMult (X,Y)) . [a,((FuncAdd (X,Y)) . (f,g))] proofend; theorem Th10: :: LOPBAN_1:10 for X being non empty set for Y being RealLinearSpace holds RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is RealLinearSpace proofend; definition let X be non empty set ; let Y be RealLinearSpace; func RealVectSpace (X,Y) -> RealLinearSpace equals :: LOPBAN_1:def 4 RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #); coherence RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is RealLinearSpace by Th10; end; :: deftheorem defines RealVectSpace LOPBAN_1:def_4_:_ for X being non empty set for Y being RealLinearSpace holds RealVectSpace (X,Y) = RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #); registration let X be non empty set ; let Y be RealLinearSpace; cluster RealVectSpace (X,Y) -> strict ; coherence RealVectSpace (X,Y) is strict ; end; registration let X be non empty set ; let Y be RealLinearSpace; cluster RealVectSpace (X,Y) -> constituted-Functions ; coherence RealVectSpace (X,Y) is constituted-Functions by MONOID_0:80; end; definition let X be non empty set ; let Y be RealLinearSpace; let f be VECTOR of (RealVectSpace (X,Y)); let x be Element of X; :: original:. redefine funcf . x -> VECTOR of Y; coherence f . x is VECTOR of Y proofend; end; theorem :: LOPBAN_1:11 for X being non empty set for Y being RealLinearSpace for f, g, h being VECTOR of (RealVectSpace (X,Y)) holds ( h = f + g iff for x being Element of X holds h . x = (f . x) + (g . x) ) by Th1; theorem :: LOPBAN_1:12 for X being non empty set for Y being RealLinearSpace for f, h being VECTOR of (RealVectSpace (X,Y)) for a being Real holds ( h = a * f iff for x being Element of X holds h . x = a * (f . x) ) by Th2; theorem :: LOPBAN_1:13 for X being non empty set for Y being RealLinearSpace holds 0. (RealVectSpace (X,Y)) = X --> (0. Y) ; begin definition let X, Y be non empty RLSStruct ; let IT be Function of X,Y; attrIT is homogeneous means :Def5: :: LOPBAN_1:def 5 for x being VECTOR of X for r being Real holds IT . (r * x) = r * (IT . x); end; :: deftheorem Def5 defines homogeneous LOPBAN_1:def_5_:_ for X, Y being non empty RLSStruct for IT being Function of X,Y holds ( IT is homogeneous iff for x being VECTOR of X for r being Real holds IT . (r * x) = r * (IT . x) ); registration let X be non empty RLSStruct ; let Y be RealLinearSpace; cluster non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like total quasi_total additive homogeneous for Element of bool [: the carrier of X, the carrier of Y:]; existence ex b1 being Function of X,Y st ( b1 is additive & b1 is homogeneous ) proofend; end; definition let X, Y be RealLinearSpace; mode LinearOperator of X,Y is additive homogeneous Function of X,Y; end; definition let X, Y be RealLinearSpace; func LinearOperators (X,Y) -> Subset of (RealVectSpace ( the carrier of X,Y)) means :Def6: :: LOPBAN_1:def 6 for x being set holds ( x in it iff x is LinearOperator of X,Y ); existence ex b1 being Subset of (RealVectSpace ( the carrier of X,Y)) st for x being set holds ( x in b1 iff x is LinearOperator of X,Y ) proofend; uniqueness for b1, b2 being Subset of (RealVectSpace ( the carrier of X,Y)) st ( for x being set holds ( x in b1 iff x is LinearOperator of X,Y ) ) & ( for x being set holds ( x in b2 iff x is LinearOperator of X,Y ) ) holds b1 = b2 proofend; end; :: deftheorem Def6 defines LinearOperators LOPBAN_1:def_6_:_ for X, Y being RealLinearSpace for b3 being Subset of (RealVectSpace ( the carrier of X,Y)) holds ( b3 = LinearOperators (X,Y) iff for x being set holds ( x in b3 iff x is LinearOperator of X,Y ) ); registration let X, Y be RealLinearSpace; cluster LinearOperators (X,Y) -> non empty functional ; coherence ( not LinearOperators (X,Y) is empty & LinearOperators (X,Y) is functional ) proofend; end; theorem Th14: :: LOPBAN_1:14 for X, Y being RealLinearSpace holds LinearOperators (X,Y) is linearly-closed proofend; theorem :: LOPBAN_1:15 for X, Y being RealLinearSpace holds RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is Subspace of RealVectSpace ( the carrier of X,Y) by Th14, RSSPACE:11; registration let X, Y be RealLinearSpace; cluster RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ; coherence ( RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is Abelian & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is add-associative & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is right_zeroed & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is right_complementable & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is vector-distributive & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is scalar-distributive & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is scalar-associative & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is scalar-unital ) by Th14, RSSPACE:11; end; definition let X, Y be RealLinearSpace; func R_VectorSpace_of_LinearOperators (X,Y) -> RealLinearSpace equals :: LOPBAN_1:def 7 RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #); coherence RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is RealLinearSpace ; end; :: deftheorem defines R_VectorSpace_of_LinearOperators LOPBAN_1:def_7_:_ for X, Y being RealLinearSpace holds R_VectorSpace_of_LinearOperators (X,Y) = RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #); registration let X, Y be RealLinearSpace; cluster R_VectorSpace_of_LinearOperators (X,Y) -> strict ; coherence R_VectorSpace_of_LinearOperators (X,Y) is strict ; end; registration let X, Y be RealLinearSpace; cluster R_VectorSpace_of_LinearOperators (X,Y) -> constituted-Functions ; coherence R_VectorSpace_of_LinearOperators (X,Y) is constituted-Functions by MONOID_0:80; end; definition let X, Y be RealLinearSpace; let f be Element of (R_VectorSpace_of_LinearOperators (X,Y)); let v be VECTOR of X; :: original:. redefine funcf . v -> VECTOR of Y; coherence f . v is VECTOR of Y proofend; end; theorem Th16: :: LOPBAN_1:16 for X, Y being RealLinearSpace for f, g, h being VECTOR of (R_VectorSpace_of_LinearOperators (X,Y)) holds ( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) ) proofend; theorem Th17: :: LOPBAN_1:17 for X, Y being RealLinearSpace for f, h being VECTOR of (R_VectorSpace_of_LinearOperators (X,Y)) for a being Real holds ( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) ) proofend; theorem Th18: :: LOPBAN_1:18 for X, Y being RealLinearSpace holds 0. (R_VectorSpace_of_LinearOperators (X,Y)) = the carrier of X --> (0. Y) proofend; theorem Th19: :: LOPBAN_1:19 for X, Y being RealLinearSpace holds the carrier of X --> (0. Y) is LinearOperator of X,Y proofend; begin theorem Th20: :: LOPBAN_1:20 for X being RealNormSpace for seq being sequence of X for g being Point of X st seq is convergent & lim seq = g holds ( ||.seq.|| is convergent & lim ||.seq.|| = ||.g.|| ) proofend; definition let X, Y be RealNormSpace; let IT be LinearOperator of X,Y; attrIT is Lipschitzian means :Def8: :: LOPBAN_1:def 8 ex K being Real st ( 0 <= K & ( for x being VECTOR of X holds ||.(IT . x).|| <= K * ||.x.|| ) ); end; :: deftheorem Def8 defines Lipschitzian LOPBAN_1:def_8_:_ for X, Y being RealNormSpace for IT being LinearOperator of X,Y 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: :: LOPBAN_1:21 for X, Y being RealNormSpace for f being LinearOperator of X,Y st ( for x being VECTOR of X holds f . x = 0. Y ) holds f is Lipschitzian proofend; registration let X, Y be RealNormSpace; cluster non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like total quasi_total additive homogeneous Lipschitzian for Element of bool [: the carrier of X, the carrier of Y:]; existence ex b1 being LinearOperator of X,Y st b1 is Lipschitzian proofend; end; definition let X, Y be RealNormSpace; func BoundedLinearOperators (X,Y) -> Subset of (R_VectorSpace_of_LinearOperators (X,Y)) means :Def9: :: LOPBAN_1:def 9 for x being set holds ( x in it iff x is Lipschitzian LinearOperator of X,Y ); existence ex b1 being Subset of (R_VectorSpace_of_LinearOperators (X,Y)) st for x being set holds ( x in b1 iff x is Lipschitzian LinearOperator of X,Y ) proofend; uniqueness for b1, b2 being Subset of (R_VectorSpace_of_LinearOperators (X,Y)) st ( for x being set holds ( x in b1 iff x is Lipschitzian LinearOperator of X,Y ) ) & ( for x being set holds ( x in b2 iff x is Lipschitzian LinearOperator of X,Y ) ) holds b1 = b2 proofend; end; :: deftheorem Def9 defines BoundedLinearOperators LOPBAN_1:def_9_:_ for X, Y being RealNormSpace for b3 being Subset of (R_VectorSpace_of_LinearOperators (X,Y)) holds ( b3 = BoundedLinearOperators (X,Y) iff for x being set holds ( x in b3 iff x is Lipschitzian LinearOperator of X,Y ) ); registration let X, Y be RealNormSpace; cluster BoundedLinearOperators (X,Y) -> non empty ; coherence not BoundedLinearOperators (X,Y) is empty proofend; end; theorem Th22: :: LOPBAN_1:22 for X, Y being RealNormSpace holds BoundedLinearOperators (X,Y) is linearly-closed proofend; theorem :: LOPBAN_1:23 for X, Y being RealNormSpace holds RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is Subspace of R_VectorSpace_of_LinearOperators (X,Y) by Th22, RSSPACE:11; registration let X, Y be RealNormSpace; cluster RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ; coherence ( RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is Abelian & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is add-associative & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is right_zeroed & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is right_complementable & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is vector-distributive & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is scalar-distributive & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is scalar-associative & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is scalar-unital ) by Th22, RSSPACE:11; end; definition let X, Y be RealNormSpace; func R_VectorSpace_of_BoundedLinearOperators (X,Y) -> RealLinearSpace equals :: LOPBAN_1:def 10 RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #); coherence RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is RealLinearSpace ; end; :: deftheorem defines R_VectorSpace_of_BoundedLinearOperators LOPBAN_1:def_10_:_ for X, Y being RealNormSpace holds R_VectorSpace_of_BoundedLinearOperators (X,Y) = RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #); registration let X, Y be RealNormSpace; cluster R_VectorSpace_of_BoundedLinearOperators (X,Y) -> strict ; coherence R_VectorSpace_of_BoundedLinearOperators (X,Y) is strict ; end; registration let X, Y be RealNormSpace; cluster -> Relation-like Function-like for Element of the carrier of (R_VectorSpace_of_BoundedLinearOperators (X,Y)); coherence for b1 being Element of (R_VectorSpace_of_BoundedLinearOperators (X,Y)) holds ( b1 is Function-like & b1 is Relation-like ) ; end; definition let X, Y be RealNormSpace; let f be Element of (R_VectorSpace_of_BoundedLinearOperators (X,Y)); let v be VECTOR of X; :: original:. redefine funcf . v -> VECTOR of Y; coherence f . v is VECTOR of Y proofend; end; theorem Th24: :: LOPBAN_1:24 for X, Y being RealNormSpace for f, g, h being VECTOR of (R_VectorSpace_of_BoundedLinearOperators (X,Y)) holds ( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) ) proofend; theorem Th25: :: LOPBAN_1:25 for X, Y being RealNormSpace for f, h being VECTOR of (R_VectorSpace_of_BoundedLinearOperators (X,Y)) for a being Real holds ( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) ) proofend; theorem Th26: :: LOPBAN_1:26 for X, Y being RealNormSpace holds 0. (R_VectorSpace_of_BoundedLinearOperators (X,Y)) = the carrier of X --> (0. Y) proofend; definition let X, Y be RealNormSpace; let f be set ; assume A1: f in BoundedLinearOperators (X,Y) ; func modetrans (f,X,Y) -> Lipschitzian LinearOperator of X,Y equals :Def11: :: LOPBAN_1:def 11 f; coherence f is Lipschitzian LinearOperator of X,Y by A1, Def9; end; :: deftheorem Def11 defines modetrans LOPBAN_1:def_11_:_ for X, Y being RealNormSpace for f being set st f in BoundedLinearOperators (X,Y) holds modetrans (f,X,Y) = f; definition let X, Y be RealNormSpace; let u be LinearOperator of X,Y; func PreNorms u -> non empty Subset of REAL equals :: LOPBAN_1:def 12 { ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1 } ; coherence { ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1 } is non empty Subset of REAL proofend; end; :: deftheorem defines PreNorms LOPBAN_1:def_12_:_ for X, Y being RealNormSpace for u being LinearOperator of X,Y holds PreNorms u = { ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1 } ; theorem Th27: :: LOPBAN_1:27 for X, Y being RealNormSpace for g being Lipschitzian LinearOperator of X,Y holds PreNorms g is bounded_above proofend; theorem :: LOPBAN_1:28 for X, Y being RealNormSpace for g being LinearOperator of X,Y holds ( g is Lipschitzian iff PreNorms g is bounded_above ) proofend; definition let X, Y be RealNormSpace; func BoundedLinearOperatorsNorm (X,Y) -> Function of (BoundedLinearOperators (X,Y)),REAL means :Def13: :: LOPBAN_1:def 13 for x being set st x in BoundedLinearOperators (X,Y) holds it . x = upper_bound (PreNorms (modetrans (x,X,Y))); existence ex b1 being Function of (BoundedLinearOperators (X,Y)),REAL st for x being set st x in BoundedLinearOperators (X,Y) holds b1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) proofend; uniqueness for b1, b2 being Function of (BoundedLinearOperators (X,Y)),REAL st ( for x being set st x in BoundedLinearOperators (X,Y) holds b1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being set st x in BoundedLinearOperators (X,Y) holds b2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) holds b1 = b2 proofend; end; :: deftheorem Def13 defines BoundedLinearOperatorsNorm LOPBAN_1:def_13_:_ for X, Y being RealNormSpace for b3 being Function of (BoundedLinearOperators (X,Y)),REAL holds ( b3 = BoundedLinearOperatorsNorm (X,Y) iff for x being set st x in BoundedLinearOperators (X,Y) holds b3 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ); theorem Th29: :: LOPBAN_1:29 for X, Y being RealNormSpace for f being Lipschitzian LinearOperator of X,Y holds modetrans (f,X,Y) = f proofend; theorem Th30: :: LOPBAN_1:30 for X, Y being RealNormSpace for f being Lipschitzian LinearOperator of X,Y holds (BoundedLinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms f) proofend; definition let X, Y be RealNormSpace; func R_NormSpace_of_BoundedLinearOperators (X,Y) -> non empty NORMSTR equals :: LOPBAN_1:def 14 NORMSTR(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(BoundedLinearOperatorsNorm (X,Y)) #); coherence NORMSTR(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(BoundedLinearOperatorsNorm (X,Y)) #) is non empty NORMSTR ; end; :: deftheorem defines R_NormSpace_of_BoundedLinearOperators LOPBAN_1:def_14_:_ for X, Y being RealNormSpace holds R_NormSpace_of_BoundedLinearOperators (X,Y) = NORMSTR(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(BoundedLinearOperatorsNorm (X,Y)) #); theorem Th31: :: LOPBAN_1:31 for X, Y being RealNormSpace holds the carrier of X --> (0. Y) = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) proofend; theorem Th32: :: LOPBAN_1:32 for X, Y being RealNormSpace for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) for g being Lipschitzian LinearOperator of X,Y st g = f holds for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.|| proofend; theorem Th33: :: LOPBAN_1:33 for X, Y being RealNormSpace for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds 0 <= ||.f.|| proofend; theorem Th34: :: LOPBAN_1:34 for X, Y being RealNormSpace for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds 0 = ||.f.|| proofend; registration let X, Y be RealNormSpace; cluster -> Relation-like Function-like for Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)); coherence for b1 being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds ( b1 is Function-like & b1 is Relation-like ) ; end; definition let X, Y be RealNormSpace; let f be Element of (R_NormSpace_of_BoundedLinearOperators (X,Y)); let v be VECTOR of X; :: original:. redefine funcf . v -> VECTOR of Y; coherence f . v is VECTOR of Y proofend; end; theorem Th35: :: LOPBAN_1:35 for X, Y being RealNormSpace for f, g, h being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds ( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) ) proofend; theorem Th36: :: LOPBAN_1:36 for X, Y being RealNormSpace for f, h being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) for a being Real holds ( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) ) proofend; theorem Th37: :: LOPBAN_1:37 for X, Y being RealNormSpace for f, g being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) for a being Real holds ( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) ) & ( f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) implies ||.f.|| = 0 ) & ||.(a * f).|| = (abs a) * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| ) proofend; theorem Th38: :: LOPBAN_1:38 for X, Y being RealNormSpace holds ( R_NormSpace_of_BoundedLinearOperators (X,Y) is reflexive & R_NormSpace_of_BoundedLinearOperators (X,Y) is discerning & R_NormSpace_of_BoundedLinearOperators (X,Y) is RealNormSpace-like ) proofend; theorem Th39: :: LOPBAN_1:39 for X, Y being RealNormSpace holds R_NormSpace_of_BoundedLinearOperators (X,Y) is RealNormSpace proofend; registration let X, Y be RealNormSpace; cluster R_NormSpace_of_BoundedLinearOperators (X,Y) -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ; coherence ( R_NormSpace_of_BoundedLinearOperators (X,Y) is reflexive & R_NormSpace_of_BoundedLinearOperators (X,Y) is discerning & R_NormSpace_of_BoundedLinearOperators (X,Y) is RealNormSpace-like & R_NormSpace_of_BoundedLinearOperators (X,Y) is vector-distributive & R_NormSpace_of_BoundedLinearOperators (X,Y) is scalar-distributive & R_NormSpace_of_BoundedLinearOperators (X,Y) is scalar-associative & R_NormSpace_of_BoundedLinearOperators (X,Y) is scalar-unital & R_NormSpace_of_BoundedLinearOperators (X,Y) is Abelian & R_NormSpace_of_BoundedLinearOperators (X,Y) is add-associative & R_NormSpace_of_BoundedLinearOperators (X,Y) is right_zeroed & R_NormSpace_of_BoundedLinearOperators (X,Y) is right_complementable ) by Th39; end; theorem Th40: :: LOPBAN_1:40 for X, Y being RealNormSpace for f, g, h being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds ( h = f - g iff for x being VECTOR of X holds h . x = (f . x) - (g . x) ) proofend; begin definition let X be RealNormSpace; attrX is complete means :Def15: :: LOPBAN_1:def 15 for seq being sequence of X st seq is Cauchy_sequence_by_Norm holds seq is convergent ; end; :: deftheorem Def15 defines complete LOPBAN_1:def_15_:_ for X being RealNormSpace holds ( X is complete iff for seq being sequence of X st seq is Cauchy_sequence_by_Norm holds seq is convergent ); registration cluster non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V104() discerning reflexive RealNormSpace-like complete for NORMSTR ; existence ex b1 being RealNormSpace st b1 is complete proofend; end; definition mode RealBanachSpace is complete RealNormSpace; end; Lm3: for e being Real for seq being Real_Sequence st seq is convergent & ex k being Element of NAT st for i being Element of NAT st k <= i holds seq . i <= e holds lim seq <= e proofend; theorem Th41: :: LOPBAN_1:41 for X being RealNormSpace for seq being sequence of X st seq is convergent holds ( ||.seq.|| is convergent & lim ||.seq.|| = ||.(lim seq).|| ) proofend; theorem Th42: :: LOPBAN_1:42 for X, Y being RealNormSpace st Y is complete holds for seq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds seq is convergent proofend; theorem Th43: :: LOPBAN_1:43 for X being RealNormSpace for Y being RealBanachSpace holds R_NormSpace_of_BoundedLinearOperators (X,Y) is RealBanachSpace proofend; registration let X be RealNormSpace; let Y be RealBanachSpace; cluster R_NormSpace_of_BoundedLinearOperators (X,Y) -> non empty complete ; coherence R_NormSpace_of_BoundedLinearOperators (X,Y) is complete by Th43; end;