:: Banach Space of Bounded Linear Operators :: by Yasunari Shidama :: :: Received December 22, 2003 :: Copyright (c) 2003-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XBOOLE_0, FUNCT_1, ZFMISC_1, FUNCOP_1, SUBSET_1, FUNCT_2, RELAT_1, PARTFUN1, ALGSTR_0, BINOP_1, STRUCT_0, RLVECT_1, REAL_1, SUPINF_2, ARYTM_3, ARYTM_1, FUNCSDOM, MONOID_0, TARSKI, MSSUBFAM, UNIALG_1, RLSUB_1, RSSPACE, NORMSP_1, NAT_1, PRE_TOPC, SEQ_2, ORDINAL2, XXREAL_0, CARD_1, COMPLEX1, XXREAL_2, SEQ_4, REWRITE1, RSSPACE3, SEQ_1, VALUED_1, LOPBAN_1, METRIC_1, RELAT_2, FCONT_1, ASYMPT_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_3, PRE_TOPC, DOMAIN_1, FUNCOP_1, BINOP_1, XXREAL_0, XXREAL_2, XCMPLX_0, COMPLEX1, REAL_1, ORDINAL1, NAT_1, STRUCT_0, ALGSTR_0, XREAL_0, NUMBERS, MONOID_0, RLVECT_1, RLSUB_1, NORMSP_0, NORMSP_1, RSSPACE, RSSPACE3, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SEQ_4, FUNCSDOM, VECTSP_1; constructors DOMAIN_1, FUNCT_3, XXREAL_0, REAL_1, NAT_1, COMPLEX1, SEQM_3, RLSUB_1, FUNCSDOM, MONOID_0, MEASURE6, RSSPACE3, XXREAL_2, NORMSP_1, SEQ_4, RELSET_1, BINOP_2, RVSUM_1, SEQ_2, COMSEQ_2, SEQ_1, NUMBERS; registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, RLVECT_1, NORMSP_1, MONOID_0, RSSPACE3, VALUED_1, VALUED_0, SEQ_4, FUNCT_1, NORMSP_0, NAT_1, SEQ_1, SEQ_2; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; begin :: Real Vector Space of Operators definition let X be set; let Y be non empty set; let F be Function of [:REAL, Y:], Y; let a be Real, f be Function of X, Y; redefine func F[;](a,f) -> Element of Funcs(X, Y); 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 :: 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); end; 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 :: LOPBAN_1:def 2 for a being Real, f being Element of Funcs(X,the carrier of Y), x being Element of X holds (it.[a,f]).x = a*(f.x); end; 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; end; reserve X for non empty set; reserve Y for RealLinearSpace; reserve f,g,h for Element of Funcs(X,the carrier of Y); theorem :: LOPBAN_1:1 for Y being non empty addLoopStr, 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; reserve a,b for Real; theorem :: LOPBAN_1:2 h = (FuncExtMult(X,Y)).[a,f] iff for x being Element of X holds h .x = a*(f.x); reserve u,v,w for VECTOR of RLSStruct(#Funcs(X,the carrier of Y), (FuncZero(X, Y)),FuncAdd(X,Y),FuncExtMult(X,Y)#); theorem :: LOPBAN_1:3 (FuncAdd(X,Y)).(f,g) = (FuncAdd(X,Y)).(g,f); theorem :: LOPBAN_1:4 (FuncAdd(X,Y)).(f,(FuncAdd(X,Y)).(g,h)) = (FuncAdd(X,Y)).(( FuncAdd(X,Y)).(f,g),h); theorem :: LOPBAN_1:5 (FuncAdd(X,Y)).(FuncZero(X,Y),f) = f; theorem :: LOPBAN_1:6 (FuncAdd(X,Y)).(f,(FuncExtMult(X,Y)).[-1,f]) = FuncZero(X,Y); theorem :: LOPBAN_1:7 (FuncExtMult(X,Y)).[1,f] = f; theorem :: LOPBAN_1:8 (FuncExtMult(X,Y)).[a,(FuncExtMult(X,Y)).[b,f]] = (FuncExtMult(X ,Y)).[a*b,f] ; theorem :: LOPBAN_1:9 (FuncAdd(X,Y)). ((FuncExtMult(X,Y)).[a,f],(FuncExtMult(X,Y)).[b, f]) = (FuncExtMult(X,Y)).[a+b,f]; theorem :: LOPBAN_1:10 RLSStruct(#Funcs(X,the carrier of Y), (FuncZero(X,Y)),FuncAdd(X, Y),FuncExtMult(X,Y)#) is RealLinearSpace; 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)#); end; registration let X be non empty set; let Y be RealLinearSpace; cluster RealVectSpace(X,Y) -> strict; end; registration let X be non empty set; let Y be RealLinearSpace; cluster RealVectSpace(X,Y) -> constituted-Functions; 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; redefine func f.x -> VECTOR of Y; end; theorem :: LOPBAN_1:11 for X be non empty set for Y be RealLinearSpace for f,g,h be VECTOR of RealVectSpace(X,Y) holds h = f+g iff for x be Element of X holds h.x = f.x + g. x; theorem :: LOPBAN_1:12 for X be non empty set for Y be RealLinearSpace for f,h be VECTOR of RealVectSpace(X,Y) for a be Real holds h = a*f iff for x be Element of X holds h.x = a * f.x; theorem :: LOPBAN_1:13 for X be non empty set for Y be RealLinearSpace holds 0.RealVectSpace( X,Y) = X --> 0.Y; begin :: Real Vector Space of Linear Operators definition let X, Y be non empty RLSStruct; let IT be Function of X,Y; attr IT is homogeneous means :: LOPBAN_1:def 5 for x being VECTOR of X, r being Real holds IT.(r*x) = r*IT.x; end; registration let X be non empty RLSStruct; let Y be RealLinearSpace; cluster additive homogeneous for Function of X,Y; 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 :: LOPBAN_1:def 6 for x being set holds x in it iff x is LinearOperator of X,Y; end; registration let X, Y be RealLinearSpace; cluster LinearOperators(X,Y) -> non empty functional; end; theorem :: LOPBAN_1:14 for X, Y be RealLinearSpace holds LinearOperators(X,Y) is linearly-closed; theorem :: LOPBAN_1:15 for X, Y be 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); 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)) #) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital; 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)) #); end; registration let X, Y be RealLinearSpace; cluster R_VectorSpace_of_LinearOperators(X,Y) -> strict; end; registration let X,Y be RealLinearSpace; cluster R_VectorSpace_of_LinearOperators(X,Y) -> constituted-Functions; end; definition let X,Y be RealLinearSpace; let f be Element of R_VectorSpace_of_LinearOperators(X,Y); let v be VECTOR of X; redefine func f.v -> VECTOR of Y; end; theorem :: LOPBAN_1:16 for X, Y be RealLinearSpace for f,g,h be VECTOR of R_VectorSpace_of_LinearOperators(X,Y) holds h = f+g iff for x be VECTOR of X holds h.x = f.x + g.x; theorem :: LOPBAN_1:17 for X, Y be RealLinearSpace for f,h be VECTOR of R_VectorSpace_of_LinearOperators(X,Y) for a be Real holds h = a*f iff for x be VECTOR of X holds h.x = a * f.x; theorem :: LOPBAN_1:18 for X, Y be RealLinearSpace holds 0. R_VectorSpace_of_LinearOperators(X,Y) = (the carrier of X) -->0.Y; theorem :: LOPBAN_1:19 for X,Y be RealLinearSpace holds (the carrier of X) --> 0.Y is LinearOperator of X,Y; begin :: Real Normed Linear Space of Bounded Linear Operators theorem :: LOPBAN_1:20 for X be RealNormSpace for seq be sequence of X for g be Point of X holds seq is convergent & lim seq = g implies ||.seq.|| is convergent & lim ||.seq.|| = ||.g.||; definition let X, Y be RealNormSpace; let IT be LinearOperator of X,Y; attr IT is Lipschitzian means :: LOPBAN_1:def 8 ex K being Real st 0 <= K & for x being VECTOR of X holds ||. IT.x .|| <= K * ||. x .||; end; theorem :: LOPBAN_1:21 for X, Y be RealNormSpace holds for f be LinearOperator of X,Y st (for x be VECTOR of X holds f.x=0.Y) holds f is Lipschitzian; registration let X, Y be RealNormSpace; cluster Lipschitzian for LinearOperator of X,Y; end; definition let X, Y be RealNormSpace; func BoundedLinearOperators(X,Y) -> Subset of R_VectorSpace_of_LinearOperators(X,Y) means :: LOPBAN_1:def 9 for x being set holds x in it iff x is Lipschitzian LinearOperator of X,Y; end; registration let X, Y be RealNormSpace; cluster BoundedLinearOperators(X,Y) -> non empty; end; theorem :: LOPBAN_1:22 for X, Y be RealNormSpace holds BoundedLinearOperators(X,Y) is linearly-closed; theorem :: LOPBAN_1:23 for X, Y be 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); 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)) #) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital; 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)) #); end; registration let X, Y be RealNormSpace; cluster R_VectorSpace_of_BoundedLinearOperators(X,Y) -> strict; end; registration let X,Y be RealNormSpace; cluster -> Function-like Relation-like for Element of R_VectorSpace_of_BoundedLinearOperators(X,Y); end; definition let X,Y be RealNormSpace; let f be Element of R_VectorSpace_of_BoundedLinearOperators(X,Y); let v be VECTOR of X; redefine func f.v -> VECTOR of Y; end; theorem :: LOPBAN_1:24 for X, Y be RealNormSpace for f,g,h be VECTOR of R_VectorSpace_of_BoundedLinearOperators(X,Y) holds h = f+g iff for x be VECTOR of X holds h.x = f.x + g.x; theorem :: LOPBAN_1:25 for X, Y be RealNormSpace for f,h be VECTOR of R_VectorSpace_of_BoundedLinearOperators(X,Y) for a be Real holds h = a*f iff for x be VECTOR of X holds h.x = a * f.x; theorem :: LOPBAN_1:26 for X, Y be RealNormSpace holds 0. R_VectorSpace_of_BoundedLinearOperators(X,Y) = (the carrier of X) --> 0.Y; definition let X, Y be RealNormSpace; let f be object such that :: !!! zastapic przez In(.,.) f in BoundedLinearOperators(X,Y); func modetrans(f,X,Y) -> Lipschitzian LinearOperator of X,Y equals :: LOPBAN_1:def 11 f; end; 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 }; end; theorem :: LOPBAN_1:27 for X, Y be RealNormSpace for g be Lipschitzian LinearOperator of X,Y holds PreNorms(g) is bounded_above; theorem :: LOPBAN_1:28 for X, Y be RealNormSpace for g be LinearOperator of X,Y holds g is Lipschitzian iff PreNorms(g) is bounded_above; definition let X, Y be RealNormSpace; func BoundedLinearOperatorsNorm(X,Y) -> Function of BoundedLinearOperators(X ,Y), REAL means :: LOPBAN_1:def 13 for x be object st x in BoundedLinearOperators(X,Y) holds it.x = upper_bound PreNorms(modetrans(x,X,Y)); end; theorem :: LOPBAN_1:29 for X, Y be RealNormSpace for f be Lipschitzian LinearOperator of X,Y holds modetrans(f,X,Y)=f; theorem :: LOPBAN_1:30 for X, Y be RealNormSpace for f be Lipschitzian LinearOperator of X,Y holds BoundedLinearOperatorsNorm(X,Y).f = upper_bound PreNorms(f); 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) #); end; theorem :: LOPBAN_1:31 for X, Y be RealNormSpace holds (the carrier of X) --> 0.Y = 0. R_NormSpace_of_BoundedLinearOperators(X,Y); theorem :: LOPBAN_1:32 for X, Y be RealNormSpace for f being Point of R_NormSpace_of_BoundedLinearOperators(X,Y) for g be Lipschitzian LinearOperator of X ,Y st g=f holds for t be VECTOR of X holds ||.g.t.|| <= ||.f.|| * ||.t.||; theorem :: LOPBAN_1:33 for X, Y be RealNormSpace for f being Point of R_NormSpace_of_BoundedLinearOperators(X,Y) holds 0 <= ||.f.||; theorem :: LOPBAN_1:34 for X, Y be RealNormSpace for f being Point of R_NormSpace_of_BoundedLinearOperators(X,Y) st f = 0. R_NormSpace_of_BoundedLinearOperators(X,Y) holds 0 = ||.f.||; registration let X,Y be RealNormSpace; cluster -> Function-like Relation-like for Element of R_NormSpace_of_BoundedLinearOperators(X,Y); end; definition let X,Y be RealNormSpace; let f be Element of R_NormSpace_of_BoundedLinearOperators(X,Y); let v be VECTOR of X; redefine func f.v -> VECTOR of Y; end; theorem :: LOPBAN_1:35 for X, Y be RealNormSpace for f,g,h be Point of R_NormSpace_of_BoundedLinearOperators(X,Y) holds h = f+g iff for x be VECTOR of X holds h.x = f.x + g.x; theorem :: LOPBAN_1:36 for X, Y be RealNormSpace for f,h be Point of R_NormSpace_of_BoundedLinearOperators(X,Y) for a be Real holds h = a*f iff for x be VECTOR of X holds h.x = a * f.x; theorem :: LOPBAN_1:37 for X be RealNormSpace for Y be RealNormSpace for f, g being Point of R_NormSpace_of_BoundedLinearOperators(X,Y) for a be Real holds ( ||.f .|| = 0 iff f = 0.R_NormSpace_of_BoundedLinearOperators(X,Y) ) & ||.a*f.|| = |.a.| * ||.f.|| & ||.f+g.|| <= ||.f.|| + ||.g.||; theorem :: LOPBAN_1:38 for X,Y be RealNormSpace holds R_NormSpace_of_BoundedLinearOperators(X,Y) is reflexive discerning RealNormSpace-like; theorem :: LOPBAN_1:39 for X, Y be RealNormSpace holds R_NormSpace_of_BoundedLinearOperators(X,Y) is RealNormSpace; registration let X, Y be RealNormSpace; cluster R_NormSpace_of_BoundedLinearOperators(X,Y) -> reflexive discerning RealNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable; end; theorem :: LOPBAN_1:40 for X, Y be RealNormSpace for f,g,h be Point of R_NormSpace_of_BoundedLinearOperators(X,Y) holds h = f-g iff for x be VECTOR of X holds h.x = f.x - g.x; begin :: Real Banach Space of Bounded Linear Operators definition let X be RealNormSpace; attr X is complete means :: LOPBAN_1:def 15 for seq be sequence of X holds seq is Cauchy_sequence_by_Norm implies seq is convergent; end; registration cluster complete for RealNormSpace; end; definition mode RealBanachSpace is complete RealNormSpace; end; theorem :: LOPBAN_1:41 for X be RealNormSpace for seq be sequence of X st seq is convergent holds ||.seq.|| is convergent & lim ||.seq.|| = ||.lim seq.||; theorem :: LOPBAN_1:42 for X, Y be RealNormSpace st Y is complete for seq be sequence of R_NormSpace_of_BoundedLinearOperators(X,Y) st seq is Cauchy_sequence_by_Norm holds seq is convergent; theorem :: LOPBAN_1:43 for X be RealNormSpace for Y be RealBanachSpace holds R_NormSpace_of_BoundedLinearOperators(X,Y) is RealBanachSpace; registration let X be RealNormSpace; let Y be RealBanachSpace; cluster R_NormSpace_of_BoundedLinearOperators (X,Y) -> complete; end;