:: Complex {B}anach Space of Bounded Linear Operators :: by Noboru Endou :: :: Received February 24, 2004 :: Copyright (c) 2004-2019 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, XCMPLX_0, FUNCOP_1, SUBSET_1, FUNCT_2, RELAT_1, PARTFUN1, CLVECT_1, STRUCT_0, RLVECT_1, LOPBAN_1, SUPINF_2, ARYTM_3, ARYTM_1, COMPLEX1, ALGSTR_0, MONOID_0, TARSKI, MSSUBFAM, UNIALG_1, RLSUB_1, RSSPACE, NAT_1, PRE_TOPC, SEQ_2, ORDINAL2, NORMSP_1, XXREAL_0, CARD_1, REAL_1, XXREAL_2, SEQ_4, REWRITE1, RSSPACE3, SEQ_1, VALUED_1, CLOPBAN1, 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, XCMPLX_0, XXREAL_0, XXREAL_2, XREAL_0, COMPLEX1, REAL_1, ORDINAL1, NAT_1, STRUCT_0, ALGSTR_0, MONOID_0, NUMBERS, RLVECT_1, NORMSP_0, NORMSP_1, VALUED_1, SEQ_1, SEQ_2, SEQ_4, FUNCSDOM, CLVECT_1, CSSPACE, CSSPACE3, LOPBAN_1, VECTSP_1; constructors DOMAIN_1, REAL_1, COMPLEX1, FUNCSDOM, MONOID_0, LOPBAN_1, CSSPACE3, SEQ_4, RELSET_1, BINOP_2, SEQ_2, COMSEQ_2, FUNCT_3, SEQ_1; registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, MONOID_0, CLVECT_1, CSSPACE3, VALUED_1, VALUED_0, SEQ_4, FUNCT_1, NAT_1, SEQ_1, SEQ_2; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; definitions FUNCT_1, ALGSTR_0, VECTSP_1, NORMSP_0, XXREAL_2; equalities BINOP_1, STRUCT_0, ALGSTR_0, NORMSP_0; expansions FUNCT_1, BINOP_1, NORMSP_0; theorems ALGSTR_0, XBOOLE_0, TARSKI, ABSVALUE, RLVECT_1, FUNCOP_1, XREAL_0, XCMPLX_0, SEQ_1, SEQ_2, FUNCT_1, NAT_1, FUNCT_2, SEQ_4, FUNCT_3, CLVECT_1, LOPBAN_1, CSSPACE, COMPLEX1, CSSPACE3, MONOID_0, XREAL_1, XXREAL_0, NORMSP_1, VECTSP_1, NORMSP_0, ORDINAL1; schemes SEQ_1, FUNCT_2, XBOOLE_0, BINOP_1; begin :: Complex Vector Space of Operators definition let X be set; let Y be non empty set; let F be Function of [:COMPLEX, Y:], Y; let c be Complex, f be Function of X, Y; redefine func F[;](c,f) -> Element of Funcs(X, Y); coherence proof A1: dom f = X by FUNCT_2:def 1; c in COMPLEX by XCMPLX_0:def 2; then dom f --> c is Function of X,COMPLEX by A1,FUNCOP_1:45; then reconsider g = <:dom f --> c, f:> as Function of X,[:COMPLEX, Y:] by FUNCT_3:58; F[;](c,f) = F * g by FUNCOP_1:def 5; hence thesis by FUNCT_2:8; end; end; definition let X be non empty set; let Y be ComplexLinearSpace; func FuncExtMult(X,Y) -> Function of [:COMPLEX,Funcs(X,the carrier of Y):], Funcs(X,the carrier of Y) means :Def1: for c being Complex, f being Element of Funcs(X,the carrier of Y), x being Element of X holds (it.[c,f]).x = c*(f.x); existence proof deffunc F(Complex,Element of Funcs(X,the carrier of Y)) = ((the Mult of Y) [;](\$1,\$2)); consider F being Function of [:COMPLEX,Funcs(X,the carrier of Y):], Funcs(X, the carrier of Y) such that A1: for c be Element of COMPLEX, f being Element of Funcs(X,the carrier of Y) holds F.(c,f) = F(c,f) from BINOP_1:sch 4; take F; let c be Complex,f be Element of Funcs(X,the carrier of Y), x be Element of X; reconsider c1 = c as Element of COMPLEX by XCMPLX_0:def 2; A2: dom (F.[c1,f]) = X by FUNCT_2:92; F.(c1,f) = ((the Mult of Y)[;](c1,f)) by A1; hence (F.[c,f]).x = (the Mult of Y).(c,f.x) by A2,FUNCOP_1:32 .= c*(f.x) by CLVECT_1:def 1; end; uniqueness proof let it1,it2 be Function of [:COMPLEX,Funcs(X,the carrier of Y):], Funcs(X, the carrier of Y) such that A3: for c being Complex, f being Element of Funcs(X,the carrier of Y), x being Element of X holds (it1.[c,f]).x = c*(f.x) and A4: for c being Complex, f being Element of Funcs(X,the carrier of Y), x being Element of X holds (it2.[c,f]).x = c*(f.x); now let c be Element of COMPLEX, f be Element of Funcs(X,the carrier of Y ); now let x be Element of X; thus (it1.[c,f]).x = c*(f.x) by A3 .= (it2.[c,f]).x by A4; end; hence it1.(c,f) = it2.(c,f) by FUNCT_2:63; end; hence thesis; end; end; reserve X for non empty set; reserve Y for ComplexLinearSpace; reserve f,g,h for Element of Funcs(X,the carrier of Y); theorem Th1: for x being Element of X holds (FuncZero(X,Y)).x = 0.Y proof let x be Element of X; thus (FuncZero(X,Y)).x = (X --> 0.Y).x by LOPBAN_1:def 3 .= 0.Y by FUNCOP_1:7; end; reserve a,b for Complex; theorem Th2: h = (FuncExtMult(X,Y)).[a,f] iff for x being Element of X holds h .x = a*(f.x) proof thus h = (FuncExtMult(X,Y)).[a,f] implies for x being Element of X holds h.x = a*(f.x) by Def1; reconsider a as Element of COMPLEX by XCMPLX_0:def 2; now assume A1: for x being Element of X holds h.x = a*(f.x); for x being Element of X holds h.x = ((FuncExtMult(X,Y)).[a,f]).x proof let x be Element of X; thus h.x = a*(f.x) by A1 .= ((FuncExtMult(X,Y)).[a,f]).x by Def1; end; hence h = (FuncExtMult(X,Y)).[a,f] by FUNCT_2:63; end; hence thesis; end; reserve u,v,w for VECTOR of CLSStruct(#Funcs(X,the carrier of Y), (FuncZero(X, Y)),FuncAdd(X,Y),FuncExtMult(X,Y)#); theorem Th3: (FuncAdd(X,Y)).(f,g) = (FuncAdd(X,Y)).(g,f) proof now let x be Element of X; thus ((FuncAdd(X,Y)).(f,g)).x = g.x + f.x by LOPBAN_1:1 .= ((FuncAdd(X,Y)).(g,f)).x by LOPBAN_1:1; end; hence thesis by FUNCT_2:63; end; theorem Th4: (FuncAdd(X,Y)).(f,(FuncAdd(X,Y)).(g,h)) = (FuncAdd(X,Y)).(( FuncAdd(X,Y)).(f,g),h) proof now let x be Element of X; thus ((FuncAdd(X,Y)).(f,(FuncAdd(X,Y)).(g,h))).x = f.x + ((FuncAdd(X,Y)).( g,h)).x by LOPBAN_1:1 .= f.x + (g.x + h.x) by LOPBAN_1:1 .= (f.x + g.x) + h.x by RLVECT_1:def 3 .= ((FuncAdd(X,Y)).(f,g)).x + h.x by LOPBAN_1:1 .= ((FuncAdd(X,Y)).((FuncAdd(X,Y)).(f,g),h)).x by LOPBAN_1:1; end; hence thesis by FUNCT_2:63; end; theorem Th5: (FuncAdd(X,Y)).(FuncZero(X,Y),f) = f proof now let x be Element of X; thus ((FuncAdd(X,Y)).(FuncZero(X,Y),f)).x = (FuncZero(X,Y)).x + f.x by LOPBAN_1:1 .= 0.Y + f.x by Th1 .= f.x by RLVECT_1:def 4; end; hence thesis by FUNCT_2:63; end; theorem Th6: (FuncAdd(X,Y)).(f,(FuncExtMult(X,Y)).[-1r,f]) = FuncZero(X,Y) proof reconsider mj = -1r as Element of COMPLEX by XCMPLX_0:def 2; now let x be Element of X; set y=f.x; thus ((FuncAdd(X,Y)).(f,(FuncExtMult(X,Y)).[mj,f])).x = f.x + ((FuncExtMult(X,Y)).[mj,f]).x by LOPBAN_1:1 .= f.x + ((-1r)*y) by Th2 .= f.x + (-y) by CLVECT_1:3 .= 0.Y by RLVECT_1:5 .= (FuncZero(X,Y)).x by Th1; end; then (FuncAdd(X,Y)).(f,(FuncExtMult(X,Y)).[mj,f]) = FuncZero(X,Y) by FUNCT_2:63; hence thesis; end; theorem Th7: (FuncExtMult(X,Y)).[1r,f] = f proof now let x be Element of X; thus ((FuncExtMult(X,Y)).[1r,f]).x = 1r*(f.x) by Th2 .= f.x by CLVECT_1:def 5; end; hence thesis by FUNCT_2:63; end; theorem Th8: (FuncExtMult(X,Y)).[a,(FuncExtMult(X,Y)).[b,f]] = (FuncExtMult(X, Y)).[a*b,f] proof reconsider a1=a,b1=b, ab = a*b as Element of COMPLEX by XCMPLX_0:def 2; now let x be Element of X; thus ((FuncExtMult(X,Y)).[a1,(FuncExtMult(X,Y)).[b1,f]]).x = a1*(((FuncExtMult(X,Y)).[b1,f]).x) by Th2 .= a*(b*(f.x)) by Th2 .= (a*b)*(f.x) by CLVECT_1:def 4 .= ((FuncExtMult(X,Y)).[ab,f]).x by Th2; end; then (FuncExtMult(X,Y)).[a,(FuncExtMult(X,Y)).[b,f]] = (FuncExtMult(X, Y)).[ab,f] by FUNCT_2:63; hence thesis; end; theorem Th9: (FuncAdd(X,Y)).((FuncExtMult(X,Y)).[a,f],(FuncExtMult(X,Y)).[b,f ]) = (FuncExtMult(X,Y)).[a+b,f] proof reconsider a1=a,b1=b, ab=a+b as Element of COMPLEX by XCMPLX_0:def 2; now let x be Element of X; thus ((FuncAdd(X,Y)). ((FuncExtMult(X,Y)).[a1,f],(FuncExtMult(X,Y)).[b1,f])).x = ((FuncExtMult(X,Y)).[a1,f]).x + ((FuncExtMult(X,Y)).[b1,f]).x by LOPBAN_1:1 .= a1*(f.x) + ((FuncExtMult(X,Y)).[b1,f]).x by Th2 .= a*(f.x) + b*(f.x) by Th2 .= (a+b)*(f.x) by CLVECT_1:def 3 .= ((FuncExtMult(X,Y)).[ab,f]).x by Th2; end; then (FuncAdd(X,Y)).((FuncExtMult(X,Y)).[a,f],(FuncExtMult(X,Y)).[b,f ]) = (FuncExtMult(X,Y)).[a+b,f] by FUNCT_2:63; hence thesis; end; Lm1: (FuncAdd(X,Y)).((FuncExtMult(X,Y)).[a,f],(FuncExtMult(X,Y)).[a,g]) = ( FuncExtMult(X,Y)).[a,(FuncAdd(X,Y)).(f,g)] proof reconsider a1=a as Element of COMPLEX by XCMPLX_0:def 2; now let x be Element of X; thus ((FuncAdd(X,Y)). ((FuncExtMult(X,Y)).[a1,f],(FuncExtMult(X,Y)).[a1,g])).x = ((FuncExtMult(X,Y)).[a1,f]).x + ((FuncExtMult(X,Y)).[a1,g]).x by LOPBAN_1:1 .= a1*(f.x) + ((FuncExtMult(X,Y)).[a1,g]).x by Th2 .= a*(f.x) + a*(g.x) by Th2 .= a*(f.x + g.x) by CLVECT_1:def 2 .= a*(((FuncAdd(X,Y)).(f,g)).x) by LOPBAN_1:1 .= ((FuncExtMult(X,Y)).[a1,(FuncAdd(X,Y)).(f,g)]).x by Th2; end; hence thesis by FUNCT_2:63; end; theorem Th10: CLSStruct(#Funcs(X,the carrier of Y),(FuncZero(X,Y)),FuncAdd(X,Y ), FuncExtMult(X,Y)#) is ComplexLinearSpace proof set IT = CLSStruct(#Funcs(X,the carrier of Y),(FuncZero(X,Y)), FuncAdd(X,Y), FuncExtMult(X,Y)#); A1: (u+v)+w = u+(v+w) by Th4; A2: u is right_complementable proof reconsider u9 = u as Element of Funcs(X,the carrier of Y); reconsider mj=-1r as Element of COMPLEX by XCMPLX_0:def 2; reconsider w = (FuncExtMult(X,Y)).[mj,u9] as VECTOR of IT; take w; thus thesis by Th6; end; A3: for a be Complex, u,v be VECTOR of IT holds a * (u + v) = a * u + a * v proof let a be Complex; let u,v be VECTOR of IT; reconsider a as Element of COMPLEX by XCMPLX_0:def 2; a * (u + v) = a * u + a * v proof reconsider v9 = v, u9 = u as Element of Funcs(X,the carrier of Y); reconsider w = (FuncExtMult(X,Y)).[a,u9], w9 = (FuncExtMult(X,Y)).[a,v9] as VECTOR of IT; a*(u+v) = (FuncExtMult(X,Y)).[a,(FuncAdd(X,Y)).(u9,v9)] by CLVECT_1:def 1 .=(FuncAdd(X,Y)).(w,w9) by Lm1 .= w + (a*v) by CLVECT_1:def 1 .= a*u + a*v by CLVECT_1:def 1; hence thesis; end; hence thesis; end; A4: for a,b be Complex, v be VECTOR of IT holds (a*b)*v = a*(b*v) proof let a,b be Complex; let v be VECTOR of IT; reconsider v9=v as Element of Funcs(X,the carrier of Y); thus (a*b)*v = (FuncExtMult(X,Y)).[a*b,v9] by CLVECT_1:def 1 .= (FuncExtMult(X,Y)).[a,(FuncExtMult(X,Y)).[b,v9]] by Th8 .= (FuncExtMult(X,Y)).[a,b*v] by CLVECT_1:def 1 .= a*(b*v) by CLVECT_1:def 1; end; A5: for a,b be Complex, v be VECTOR of IT holds (a+b)*v = a*v + b*v proof let a,b be Complex; let v be VECTOR of IT; reconsider a,b as Element of COMPLEX by XCMPLX_0:def 2; reconsider v9 = v as Element of Funcs(X,the carrier of Y); reconsider w = (FuncExtMult(X,Y)).[a,v9],w9 = (FuncExtMult(X,Y)).[b,v9] as VECTOR of IT; (a+b)*v = (FuncExtMult(X,Y)).[a+b,v9] by CLVECT_1:def 1 .= (FuncAdd(X,Y)).(w,w9) by Th9 .= w + (b*v) by CLVECT_1:def 1 .= (a*v) + (b*v) by CLVECT_1:def 1; hence thesis; end; A6: u+0.IT = u proof reconsider u9=u as Element of Funcs(X,the carrier of Y); thus u+0.IT = (FuncAdd(X,Y)).(FuncZero(X,Y),u9) by Th3 .= u by Th5; end; A7: for v be VECTOR of IT holds 1r*v = v proof let v be VECTOR of IT; reconsider v9=v as Element of Funcs(X,the carrier of Y); thus 1r*v = (FuncExtMult(X,Y)).[1r,v9] by CLVECT_1:def 1 .= v by Th7; end; u+v = v+u by Th3; hence thesis by A1,A6,A2,A3,A5,A4,A7,ALGSTR_0:def 16,CLVECT_1:def 2,def 3 ,def 4,def 5,RLVECT_1:def 2,def 3,def 4; end; definition let X be non empty set; let Y be ComplexLinearSpace; func ComplexVectSpace(X,Y) -> ComplexLinearSpace equals CLSStruct(#Funcs(X, the carrier of Y), (FuncZero(X,Y)),FuncAdd(X,Y),FuncExtMult(X,Y)#); coherence by Th10; end; registration let X be non empty set; let Y be ComplexLinearSpace; cluster ComplexVectSpace(X,Y) -> strict; coherence; end; registration let X be non empty set; let Y be ComplexLinearSpace; cluster ComplexVectSpace(X,Y) -> constituted-Functions; coherence by MONOID_0:80; end; definition let X be non empty set; let Y be ComplexLinearSpace; let f be VECTOR of ComplexVectSpace(X,Y); let x be Element of X; redefine func f.x -> VECTOR of Y; coherence proof consider g being Function such that A1: f = g and A2: dom g = X and A3: rng g c= the carrier of Y by FUNCT_2:def 2; f.x in rng g by A1,A2,FUNCT_1:def 3; hence thesis by A3; end; end; theorem for X be non empty set, Y be ComplexLinearSpace, f,g,h be VECTOR of ComplexVectSpace(X,Y) holds h = f+g iff for x be Element of X holds h.x = f.x + g.x by LOPBAN_1:1; theorem Th12: for X be non empty set, Y be ComplexLinearSpace, f,h be VECTOR of ComplexVectSpace(X,Y), c be Complex holds h = c*f iff for x be Element of X holds h.x = c * f.x proof let X be non empty set; let Y be ComplexLinearSpace; let f,h be VECTOR of ComplexVectSpace(X,Y); let c be Complex; reconsider f9=f,h9=h as Element of Funcs(X, the carrier of Y); hereby assume A1: h = c*f; let x be Element of X; h= (FuncExtMult(X, Y)).[c,f9] by A1,CLVECT_1:def 1; hence h.x = c*f.x by Th2; end; assume for x be Element of X holds h.x=c*f.x; then h9=(FuncExtMult(X, Y)).[c,f9] by Th2; hence thesis by CLVECT_1:def 1; end; begin :: Complex Vector Space of Linear Operators definition let X, Y be non empty CLSStruct; let IT be Function of X,Y; attr IT is homogeneous means :Def3: for x being VECTOR of X, r being Complex holds IT.(r*x) = r*IT.x; end; registration let X be non empty CLSStruct; let Y be ComplexLinearSpace; cluster additive homogeneous for Function of X,Y; existence proof set f = (the carrier of X) --> 0.Y; reconsider f as Function of X,Y; take f; hereby let x,y be VECTOR of X; thus f.(x+y) = 0.Y by FUNCOP_1:7 .= 0.Y+0.Y by RLVECT_1:4 .= f.x+0.Y by FUNCOP_1:7 .= f.x+f.y by FUNCOP_1:7; end; hereby let x be VECTOR of X, c be Complex; thus f.(c*x) = 0.Y by FUNCOP_1:7 .= c*0.Y by CLVECT_1:1 .= c*f.x by FUNCOP_1:7; end; end; end; definition let X, Y be ComplexLinearSpace; mode LinearOperator of X,Y is additive homogeneous Function of X,Y; end; definition let X, Y be ComplexLinearSpace; func LinearOperators(X,Y) -> Subset of ComplexVectSpace(the carrier of X, Y) means :Def4: for x being set holds x in it iff x is LinearOperator of X,Y; existence proof defpred P[object] means \$1 is LinearOperator of X,Y; consider IT being set such that A1: for x being object holds x in IT iff x in Funcs(the carrier of X,the carrier of Y) & P[x] from XBOOLE_0:sch 1; take IT; for x be object st x in IT holds x in Funcs(the carrier of X,the carrier of Y) by A1; hence IT is Subset of ComplexVectSpace(the carrier of X, Y) by TARSKI:def 3 ; let x be set; thus x in IT implies x is LinearOperator of X,Y by A1; assume A2: x is LinearOperator of X,Y; then x in Funcs(the carrier of X,the carrier of Y) by FUNCT_2:8; hence thesis by A1,A2; end; uniqueness proof let X1,X2 be Subset of ComplexVectSpace(the carrier of X, Y); assume that A3: for x being set holds x in X1 iff x is LinearOperator of X,Y and A4: for x being set holds x in X2 iff x is LinearOperator of X,Y; for x being object st x in X2 holds x in X1 proof let x be object; assume x in X2; then x is LinearOperator of X,Y by A4; hence thesis by A3; end; then A5: X2 c= X1 by TARSKI:def 3; for x being object st x in X1 holds x in X2 proof let x be object; assume x in X1; then x is LinearOperator of X,Y by A3; hence thesis by A4; end; then X1 c= X2 by TARSKI:def 3; hence thesis by A5,XBOOLE_0:def 10; end; end; registration let X, Y be ComplexLinearSpace; cluster LinearOperators(X,Y) -> non empty functional; coherence proof set f = (the carrier of X) --> 0.Y; A1: f is homogeneous proof let x be VECTOR of X, c be Complex; thus f.(c*x) = 0.Y by FUNCOP_1:7 .= c*0.Y by CLVECT_1:1 .= c*f.x by FUNCOP_1:7; end; f is additive proof let x,y be VECTOR of X; thus f.(x+y) = 0.Y by FUNCOP_1:7 .=0.Y+0.Y by RLVECT_1:4 .= f.x+0.Y by FUNCOP_1:7 .= f.x+f.y by FUNCOP_1:7; end; hence LinearOperators(X,Y) is non empty by A1,Def4; let x be object; thus thesis; end; end; theorem Th13: for X,Y be ComplexLinearSpace holds LinearOperators(X,Y) is linearly-closed proof let X, Y be ComplexLinearSpace; set W = LinearOperators(X,Y); A1: for c be Complex for v be VECTOR of ComplexVectSpace(the carrier of X,Y ) st v in W holds c * v in W proof let c be Complex; let v be VECTOR of ComplexVectSpace(the carrier of X,Y) such that A2: v in W; c*v is LinearOperator of X,Y proof reconsider f=c*v as Function of X,Y by FUNCT_2:66; A3: f is homogeneous proof reconsider v9 = v as Element of Funcs(the carrier of X,the carrier of Y); let x be VECTOR of X, s be Complex; A4: v9 is LinearOperator of X,Y by A2,Def4; A5: f= (FuncExtMult(the carrier of X,Y)).[c,v9] by CLVECT_1:def 1; hence f.(s*x) =c*v9.(s*x) by Th2 .=c*(s*(v9.x)) by A4,Def3 .=c*s*v9.x by CLVECT_1:def 4 .=s*(c*v9.x) by CLVECT_1:def 4 .=s*f.x by A5,Th2; end; f is additive proof reconsider v9 = v as Element of Funcs(the carrier of X,the carrier of Y); let x,y be VECTOR of X; A6: v9 is LinearOperator of X,Y by A2,Def4; A7: f= (FuncExtMult(the carrier of X,Y)).[c,v9] by CLVECT_1:def 1; hence f.(x+y) = c*(v9.(x+y)) by Th2 .=c*(v9.x+v9.y) by A6,VECTSP_1:def 20 .=c*v9.x+c*v9.y by CLVECT_1:def 2 .=f.x+c*v9.y by A7,Th2 .=f.x+ f.y by A7,Th2; end; hence thesis by A3; end; hence thesis by Def4; end; for v,u be VECTOR of ComplexVectSpace(the carrier of X, Y) st v in LinearOperators(X,Y) & u in LinearOperators(X,Y) holds v + u in LinearOperators (X,Y) proof let v,u be VECTOR of ComplexVectSpace(the carrier of X,Y) such that A8: v in W and A9: u in W; v+u is LinearOperator of X,Y proof reconsider f=v+u as Function of X,Y by FUNCT_2:66; A10: f is homogeneous proof reconsider v9 = v, u9 = u as Element of Funcs(the carrier of X,the carrier of Y); let x be VECTOR of X, s be Complex; A11: u9 is LinearOperator of X,Y by A9,Def4; A12: v9 is LinearOperator of X,Y by A8,Def4; thus f.(s*x) =u9.(s*x)+v9.(s*x) by LOPBAN_1:1 .=(s*(u9.x))+v9.(s*x) by A11,Def3 .=s*u9.x+s*v9.x by A12,Def3 .=s*(u9.x+v9.x) by CLVECT_1:def 2 .= s*f.x by LOPBAN_1:1; end; f is additive proof reconsider v9 = v, u9 = u as Element of Funcs(the carrier of X,the carrier of Y); let x,y be VECTOR of X; A13: u9 is LinearOperator of X,Y by A9,Def4; A14: v9 is LinearOperator of X,Y by A8,Def4; thus f.(x+y) =u9.(x+y)+v9.(x+y) by LOPBAN_1:1 .=(u9.x+u9.y)+v9.(x+y) by A13,VECTSP_1:def 20 .=u9.x+u9.y+(v9.x+v9.y) by A14,VECTSP_1:def 20 .=u9.x+u9.y+v9.x+v9.y by RLVECT_1:def 3 .=u9.x+v9.x+u9.y+v9.y by RLVECT_1:def 3 .= f.x+ u9.y+v9.y by LOPBAN_1:1 .= f.x+ (u9.y+v9.y) by RLVECT_1:def 3 .= f.x+f.y by LOPBAN_1:1; end; hence thesis by A10; end; hence thesis by Def4; end; hence thesis by A1,CLVECT_1:def 7; end; theorem for X,Y be ComplexLinearSpace holds CLSStruct (# LinearOperators(X,Y), Zero_(LinearOperators(X,Y),ComplexVectSpace(the carrier of X,Y)), Add_( LinearOperators(X,Y), ComplexVectSpace(the carrier of X,Y)), Mult_( LinearOperators(X,Y), ComplexVectSpace(the carrier of X,Y)) #) is Subspace of ComplexVectSpace(the carrier of X,Y) by Th13,CSSPACE:11; registration let X,Y be ComplexLinearSpace; cluster CLSStruct (# LinearOperators(X,Y), Zero_(LinearOperators(X,Y), ComplexVectSpace(the carrier of X,Y)), Add_(LinearOperators(X,Y), ComplexVectSpace(the carrier of X,Y)), Mult_(LinearOperators(X,Y), ComplexVectSpace(the carrier of X,Y)) #) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital; coherence by Th13,CSSPACE:11; end; definition let X, Y be ComplexLinearSpace; func C_VectorSpace_of_LinearOperators(X,Y) -> ComplexLinearSpace equals CLSStruct (# LinearOperators(X,Y), Zero_(LinearOperators(X,Y),ComplexVectSpace( the carrier of X,Y)), Add_(LinearOperators(X,Y), ComplexVectSpace(the carrier of X,Y)), Mult_(LinearOperators(X,Y), ComplexVectSpace(the carrier of X,Y)) #); coherence; end; registration let X, Y be ComplexLinearSpace; cluster C_VectorSpace_of_LinearOperators(X,Y) -> strict; coherence; end; registration let X,Y be ComplexLinearSpace; cluster C_VectorSpace_of_LinearOperators(X,Y) -> constituted-Functions; coherence by MONOID_0:80; end; definition let X,Y be ComplexLinearSpace; let f be Element of C_VectorSpace_of_LinearOperators(X,Y); let v be VECTOR of X; redefine func f.v -> VECTOR of Y; coherence proof reconsider f as LinearOperator of X,Y by Def4; f.v is VECTOR of Y; hence thesis; end; end; theorem Th15: for X,Y be ComplexLinearSpace, f,g,h be VECTOR of C_VectorSpace_of_LinearOperators(X,Y) holds h = f+g iff for x be VECTOR of X holds h.x = f.x + g.x proof let X, Y be ComplexLinearSpace; let f,g,h be VECTOR of C_VectorSpace_of_LinearOperators(X,Y); reconsider f9=f,g9=g,h9=h as LinearOperator of X,Y by Def4; A1: C_VectorSpace_of_LinearOperators(X,Y) is Subspace of ComplexVectSpace( the carrier of X,Y) by Th13,CSSPACE:11; then reconsider f1 = f as VECTOR of ComplexVectSpace(the carrier of X,Y) by CLVECT_1:29; reconsider h1 = h as VECTOR of ComplexVectSpace(the carrier of X,Y) by A1, CLVECT_1:29; reconsider g1 = g as VECTOR of ComplexVectSpace(the carrier of X,Y) by A1, CLVECT_1:29; A2: now assume A3: h = f+g; let x be Element of X; h1 = f1 + g1 by A1,A3,CLVECT_1:32; hence h9.x=f9.x+g9.x by LOPBAN_1:1; end; now assume for x be Element of X holds h9.x=f9.x+g9.x; then h1 = f1 + g1 by LOPBAN_1:1; hence h =f+g by A1,CLVECT_1:32; end; hence thesis by A2; end; theorem Th16: for X,Y be ComplexLinearSpace, f,h be VECTOR of C_VectorSpace_of_LinearOperators(X,Y), c be Complex holds h = c*f iff for x be VECTOR of X holds h.x = c * f.x proof let X,Y be ComplexLinearSpace; let f,h be VECTOR of C_VectorSpace_of_LinearOperators(X,Y); reconsider f9=f,h9=h as LinearOperator of X,Y by Def4; let c be Complex; A1: C_VectorSpace_of_LinearOperators(X,Y) is Subspace of ComplexVectSpace( the carrier of X,Y) by Th13,CSSPACE:11; then reconsider f1=f as VECTOR of ComplexVectSpace(the carrier of X,Y) by CLVECT_1:29; reconsider h1=h as VECTOR of ComplexVectSpace(the carrier of X,Y) by A1, CLVECT_1:29; A2: now assume A3: h = c*f; let x be Element of X; h1 = c*f1 by A1,A3,CLVECT_1:33; hence h9.x=c*f9.x by Th12; end; now assume for x be Element of X holds h9.x=c*f9.x; then h1=c*f1 by Th12; hence h =c*f by A1,CLVECT_1:33; end; hence thesis by A2; end; theorem Th17: for X,Y be ComplexLinearSpace holds 0. C_VectorSpace_of_LinearOperators(X,Y) = (the carrier of X) -->0.Y proof let X,Y be ComplexLinearSpace; A1: 0.ComplexVectSpace(the carrier of X,Y) =((the carrier of X) -->0.Y) by LOPBAN_1:def 3; C_VectorSpace_of_LinearOperators(X,Y) is Subspace of ComplexVectSpace( the carrier of X,Y) by Th13,CSSPACE:11; hence thesis by A1,CLVECT_1:30; end; theorem Th18: for X,Y be ComplexLinearSpace holds (the carrier of X) --> 0.Y is LinearOperator of X,Y proof let X,Y be ComplexLinearSpace; set f=(the carrier of X) --> 0.Y; reconsider f as Function of X,Y; A1: f is homogeneous proof let x be VECTOR of X, c be Complex; thus f.(c*x) =0.Y by FUNCOP_1:7 .=c*0.Y by CLVECT_1:1 .= c*f.x by FUNCOP_1:7; end; f is additive proof let x,y be VECTOR of X; thus f.(x+y) = 0.Y by FUNCOP_1:7 .=0.Y+0.Y by RLVECT_1:4 .= f.x+0.Y by FUNCOP_1:7 .= f.x+f.y by FUNCOP_1:7; end; hence thesis by A1; end; begin :: Complex Normed Linear Space of Bounded Linear Operators theorem Th19: for X be ComplexNormSpace, seq be sequence of X, g be Point of X holds seq is convergent & lim seq = g implies ||.seq.|| is convergent & lim ||. seq.|| = ||.g.|| proof let X be ComplexNormSpace; let seq be sequence of X; let g be Point of X; assume that A1: seq is convergent and A2: lim seq = g; A3: now let r be Real; assume A4: r > 0; consider m1 be Nat such that A5: for n be Nat st n >= m1 holds ||.(seq.n) - g.|| < r by A1,A2,A4, CLVECT_1:def 16; take k = m1; now let n be Nat; assume n >= k; then A6: ||.(seq.n) - g.|| < r by A5; |.||.(seq.n).|| - ||.g.||.| <= ||.(seq.n) - g.|| by CLVECT_1:110; then |.||.(seq.n).|| - ||.g.||.| < r by A6,XXREAL_0:2; hence |.||.seq.||.n - ||.g.||.| < r by NORMSP_0:def 4; end; hence for n be Nat st k <= n holds |.||.seq.||.n - ||.g.||.| < r; end; ||.seq.|| is convergent by A1,CLVECT_1:117; hence thesis by A3,SEQ_2:def 7; end; definition let X, Y be ComplexNormSpace; let IT be LinearOperator of X,Y; attr IT is Lipschitzian means :Def6: ex K being Real st 0 <= K & for x being VECTOR of X holds ||. IT.x .|| <= K * ||. x .||; end; theorem Th20: for X,Y be ComplexNormSpace holds for f be LinearOperator of X,Y st (for x be VECTOR of X holds f.x=0.Y) holds f is Lipschitzian proof let X,Y be ComplexNormSpace; let f be LinearOperator of X,Y such that A1: for x be VECTOR of X holds f.x=0.Y; A2: now let x be VECTOR of X; thus ||. f.x .|| = ||. 0.Y .|| by A1 .=0*||. x .|| by CLVECT_1:102; end; take 0; thus thesis by A2; end; registration let X, Y be ComplexNormSpace; cluster Lipschitzian for LinearOperator of X,Y; existence proof set f=(the carrier of X) --> 0.Y; reconsider f as LinearOperator of X,Y by Th18; take f; for x be VECTOR of X holds f.x =0.Y by FUNCOP_1:7; hence thesis by Th20; end; end; definition let X,Y be ComplexNormSpace; func BoundedLinearOperators(X,Y) -> Subset of C_VectorSpace_of_LinearOperators(X,Y) means :Def7: for x being set holds x in it iff x is Lipschitzian LinearOperator of X,Y; existence proof defpred P[object] means \$1 is Lipschitzian LinearOperator of X,Y; consider IT being set such that A1: for x being object holds x in IT iff x in LinearOperators(X,Y) & P[x] from XBOOLE_0:sch 1; take IT; for x be object st x in IT holds x in LinearOperators(X,Y) by A1; hence IT is Subset of C_VectorSpace_of_LinearOperators(X,Y) by TARSKI:def 3 ; let x be set; thus x in IT implies x is Lipschitzian LinearOperator of X,Y by A1; assume A2: x is Lipschitzian LinearOperator of X,Y; then x in LinearOperators(X,Y) by Def4; hence thesis by A1,A2; end; uniqueness proof let X1,X2 be Subset of C_VectorSpace_of_LinearOperators(X,Y); assume that A3: for x being set holds x in X1 iff x is Lipschitzian LinearOperator of X,Y and A4: for x being set holds x in X2 iff x is Lipschitzian LinearOperator of X,Y; for x being object st x in X2 holds x in X1 proof let x be object; assume x in X2; then x is Lipschitzian LinearOperator of X,Y by A4; hence thesis by A3; end; then A5: X2 c= X1 by TARSKI:def 3; for x being object st x in X1 holds x in X2 proof let x be object; assume x in X1; then x is Lipschitzian LinearOperator of X,Y by A3; hence thesis by A4; end; then X1 c= X2 by TARSKI:def 3; hence thesis by A5,XBOOLE_0:def 10; end; end; registration let X, Y be ComplexNormSpace; cluster BoundedLinearOperators(X,Y) -> non empty; coherence proof set f=(the carrier of X) --> 0.Y; reconsider f as LinearOperator of X,Y by Th18; for x be VECTOR of X holds f.x =0.Y by FUNCOP_1:7; then f is Lipschitzian by Th20; hence thesis by Def7; end; end; theorem Th21: for X,Y be ComplexNormSpace holds BoundedLinearOperators(X,Y) is linearly-closed proof let X,Y be ComplexNormSpace; set W = BoundedLinearOperators(X,Y); A1: for v,u be VECTOR of C_VectorSpace_of_LinearOperators(X,Y) st v in W & u in W holds v + u in W proof let v,u be VECTOR of C_VectorSpace_of_LinearOperators(X,Y) such that A2: v in W and A3: u in W; reconsider f=v+u as LinearOperator of X,Y by Def4; f is Lipschitzian proof reconsider v1=v as Lipschitzian LinearOperator of X,Y by A2,Def7; consider K2 be Real such that A4: 0 <= K2 and A5: for x be VECTOR of X holds ||. v1.x .|| <= K2*||.x.|| by Def6; reconsider u1=u as Lipschitzian LinearOperator of X,Y by A3,Def7; consider K1 be Real such that A6: 0 <= K1 and A7: for x be VECTOR of X holds ||. u1.x .|| <= K1*||.x.|| by Def6; take K3=K1+K2; now let x be VECTOR of X; A8: ||. u1.x+v1.x .|| <= ||. u1.x .||+ ||. v1.x .|| by CLVECT_1:def 13; A9: ||. v1.x .|| <= K2*||. x .|| by A5; ||. u1.x .|| <= K1*||. x .|| by A7; then A10: ||. u1.x .|| + ||. v1.x .|| <= K1*||. x .|| +K2*||. x .|| by A9, XREAL_1:7; ||. f.x .|| =||. u1.x+v1.x .|| by Th15; hence ||. f.x .|| <= K3*||. x .|| by A8,A10,XXREAL_0:2; end; hence thesis by A6,A4; end; hence thesis by Def7; end; for c be Complex, v be VECTOR of C_VectorSpace_of_LinearOperators(X,Y) st v in W holds c * v in W proof let c be Complex; let v be VECTOR of C_VectorSpace_of_LinearOperators(X,Y) such that A11: v in W; reconsider f=c*v as LinearOperator of X,Y by Def4; f is Lipschitzian proof reconsider v1=v as Lipschitzian LinearOperator of X,Y by A11,Def7; consider K be Real such that A12: 0 <= K and A13: for x be VECTOR of X holds ||. v1.x .|| <= K*||. x .|| by Def6; take |.c.| * K; A14: now let x be VECTOR of X; 0 <=|.c.| by COMPLEX1:46; then A15: |.c.| * ||. v1.x .|| <= |.c.| * (K*||. x .||) by A13,XREAL_1:64; ||. c*v1.x .|| = |.c.|* ||. v1.x .|| by CLVECT_1:def 13; hence ||. f.x .|| <= |.c.| * K*||. x .|| by A15,Th16; end; 0 <=|.c.| by COMPLEX1:46; hence thesis by A12,A14; end; hence thesis by Def7; end; hence thesis by A1,CLVECT_1:def 7; end; theorem for X,Y be ComplexNormSpace holds CLSStruct (# BoundedLinearOperators( X,Y), Zero_(BoundedLinearOperators(X,Y), C_VectorSpace_of_LinearOperators(X,Y)) , Add_(BoundedLinearOperators(X,Y), C_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y),C_VectorSpace_of_LinearOperators(X,Y)) #) is Subspace of C_VectorSpace_of_LinearOperators(X,Y) by Th21,CSSPACE:11; registration let X, Y be ComplexNormSpace; cluster CLSStruct (# BoundedLinearOperators(X,Y), Zero_( BoundedLinearOperators(X,Y), C_VectorSpace_of_LinearOperators(X,Y)), Add_( BoundedLinearOperators(X,Y), C_VectorSpace_of_LinearOperators(X,Y)), Mult_( BoundedLinearOperators(X,Y),C_VectorSpace_of_LinearOperators(X,Y)) #) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital; coherence by Th21,CSSPACE:11; end; definition let X, Y be ComplexNormSpace; func C_VectorSpace_of_BoundedLinearOperators(X,Y) -> ComplexLinearSpace equals CLSStruct (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X ,Y), C_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), C_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), C_VectorSpace_of_LinearOperators(X,Y)) #); coherence; end; registration let X,Y be ComplexNormSpace; cluster C_VectorSpace_of_BoundedLinearOperators(X,Y) -> strict; coherence; end; registration let X,Y be ComplexNormSpace; cluster -> Function-like Relation-like for Element of C_VectorSpace_of_BoundedLinearOperators(X,Y); coherence; end; definition let X,Y be ComplexNormSpace; let f be Element of C_VectorSpace_of_BoundedLinearOperators(X,Y); let v be VECTOR of X; redefine func f.v -> VECTOR of Y; coherence proof reconsider f as LinearOperator of X,Y by Def7; f.v is VECTOR of Y; hence thesis; end; end; theorem Th23: for X,Y be ComplexNormSpace, f,g,h be VECTOR of C_VectorSpace_of_BoundedLinearOperators(X,Y) holds h = f+g iff for x be VECTOR of X holds h.x = f.x + g.x proof let X,Y be ComplexNormSpace; let f,g,h be VECTOR of C_VectorSpace_of_BoundedLinearOperators(X,Y); A1: C_VectorSpace_of_BoundedLinearOperators(X,Y) is Subspace of C_VectorSpace_of_LinearOperators(X,Y) by Th21,CSSPACE:11; then reconsider f1=f as VECTOR of C_VectorSpace_of_LinearOperators(X,Y) by CLVECT_1:29; reconsider h1=h as VECTOR of C_VectorSpace_of_LinearOperators(X,Y) by A1, CLVECT_1:29; reconsider g1=g as VECTOR of C_VectorSpace_of_LinearOperators(X,Y) by A1, CLVECT_1:29; hereby assume A2: h = f+g; let x be Element of X; h1=f1+g1 by A1,A2,CLVECT_1:32; hence h.x=f.x+g.x by Th15; end; assume for x be Element of X holds h.x=f.x+g.x; then h1=f1+g1 by Th15; hence thesis by A1,CLVECT_1:32; end; theorem Th24: for X,Y be ComplexNormSpace, f,h be VECTOR of C_VectorSpace_of_BoundedLinearOperators(X,Y), c be Complex holds h = c*f iff for x be VECTOR of X holds h.x = c * f.x proof let X,Y be ComplexNormSpace; let f,h be VECTOR of C_VectorSpace_of_BoundedLinearOperators(X,Y); let c be Complex; A1: C_VectorSpace_of_BoundedLinearOperators(X,Y) is Subspace of C_VectorSpace_of_LinearOperators(X,Y) by Th21,CSSPACE:11; then reconsider f1=f as VECTOR of C_VectorSpace_of_LinearOperators(X,Y) by CLVECT_1:29; reconsider h1=h as VECTOR of C_VectorSpace_of_LinearOperators(X,Y) by A1, CLVECT_1:29; hereby assume A2: h = c*f; let x be Element of X; h1=c*f1 by A1,A2,CLVECT_1:33; hence h.x=c*f.x by Th16; end; assume for x be Element of X holds h.x=c*f.x; then h1=c*f1 by Th16; hence thesis by A1,CLVECT_1:33; end; theorem Th25: for X,Y be ComplexNormSpace holds 0. C_VectorSpace_of_BoundedLinearOperators(X,Y) = (the carrier of X) --> 0.Y proof let X,Y be ComplexNormSpace; A1: 0.C_VectorSpace_of_LinearOperators(X,Y) =((the carrier of X) -->0.Y) by Th17; C_VectorSpace_of_BoundedLinearOperators(X,Y) is Subspace of C_VectorSpace_of_LinearOperators(X,Y) by Th21,CSSPACE:11; hence thesis by A1,CLVECT_1:30; end; definition let X, Y be ComplexNormSpace; let f be object such that A1: f in BoundedLinearOperators(X,Y); func modetrans(f,X,Y) -> Lipschitzian LinearOperator of X,Y equals :Def9: f; coherence by A1,Def7; end; definition let X, Y be ComplexNormSpace; let u be LinearOperator of X,Y; func PreNorms(u) -> non empty Subset of REAL equals {||.u.t.|| where t is VECTOR of X : ||.t.|| <= 1 }; coherence proof A1: now let x be object; now assume x in {||.u.t.|| where t is VECTOR of X : ||.t.|| <= 1 }; then ex t be VECTOR of X st x=||.u.t.|| & ||.t.|| <= 1; hence x in REAL; end; hence x in {||.u.t.|| where t is VECTOR of X : ||.t.|| <= 1 } implies x in REAL; end; ||.0.X.|| = 0 by CLVECT_1:102; then ||.u.(0.X).|| in {||.u.t.|| where t is VECTOR of X : ||.t.|| <= 1 }; hence thesis by A1,TARSKI:def 3; end; end; theorem Th26: for X,Y be ComplexNormSpace, g be Lipschitzian LinearOperator of X,Y holds PreNorms(g) is bounded_above proof let X,Y be ComplexNormSpace; let g be Lipschitzian LinearOperator of X,Y; PreNorms(g) is bounded_above proof consider K be Real such that A1: 0 <= K and A2: for x be VECTOR of X holds ||. g.x .|| <= K*||. x .|| by Def6; take K; let r be ExtReal; assume r in PreNorms(g); then consider t be VECTOR of X such that A3: r=||.g.t.|| and A4: ||.t.|| <= 1; A5: ||.g.t.|| <= K*||. t .|| by A2; K*||. t .|| <= K *1 by A1,A4,XREAL_1:64; hence r <=K by A3,A5,XXREAL_0:2; end; hence thesis; end; theorem for X,Y be ComplexNormSpace, g be LinearOperator of X,Y holds g is Lipschitzian iff PreNorms(g) is bounded_above proof let X,Y be ComplexNormSpace; let g be LinearOperator of X,Y; now reconsider K=upper_bound PreNorms(g) as Real; assume A1: PreNorms(g) is bounded_above; A2: now let t be VECTOR of X; now per cases; case A3: t = 0.X; then A4: ||.t.|| = 0 by NORMSP_0:def 6; g.t = g.(0c*0.X) by A3,CLVECT_1:1 .=0c*g.(0.X) by Def3 .=0.Y by CLVECT_1:1; hence ||.g.t.|| <= K*||.t.|| by A4,NORMSP_0:def 6; end; case A5: t <> 0.X; reconsider t0 = ||.t.||"+0* as Element of COMPLEX by XCMPLX_0:def 2; reconsider t1= t0 * t as VECTOR of X; A6: ||.t.|| <> 0 by A5,NORMSP_0:def 5; then A7: ||.t.|| > 0 by CLVECT_1:105; A8: |. ||.t.||"+0* .| =|. 1*||.t.||" .| .=|. 1/||.t.||.| by XCMPLX_0:def 9 .=1/|. ||.t.||.| by ABSVALUE:7 .=1/||.t.|| by A7,ABSVALUE:def 1 .=1*||.t.||" by XCMPLX_0:def 9 .=||.t.||"; then A9: ||.g.t.||/||.t.|| =||.g.t.|| * |. t0 .| by XCMPLX_0:def 9 .=||. t0*g.t .|| by CLVECT_1:def 13 .=||.g.t1.|| by Def3; ||.t1.|| = |.t0.| * ||.t.|| by CLVECT_1:def 13 .=1 by A6,A8,XCMPLX_0:def 7; then ||.g.t.||/||.t.|| in PreNorms(g) by A9; then A10: ||.g.t.||/||.t.|| <= K by A1,SEQ_4:def 1; ||.g.t.||/||.t.||*||.t.|| = ||.g.t.||*||.t.||"*||.t.|| by XCMPLX_0:def 9 .=||.g.t.||*(||.t.||"*||.t.||) .=||.g.t.||*1 by A6,XCMPLX_0:def 7 .=||.g.t.||; hence ||.g.t.|| <= K *||.t.|| by A7,A10,XREAL_1:64; end; end; hence ||.g.t.|| <= K*||.t.||; end; take K; 0 <= K proof consider r0 be object such that A11: r0 in PreNorms(g) by XBOOLE_0:def 1; reconsider r0 as Real by A11; now let r be Real; assume r in PreNorms(g); then ex t be VECTOR of X st r=||.g.t.|| & ||.t.|| <= 1; hence 0 <= r by CLVECT_1:105; end; then 0 <= r0 by A11; hence thesis by A1,A11,SEQ_4:def 1; end; hence g is Lipschitzian by A2; end; hence thesis by Th26; end; definition let X, Y be ComplexNormSpace; func BoundedLinearOperatorsNorm(X,Y) -> Function of BoundedLinearOperators(X ,Y), REAL means :Def11: for x be object st x in BoundedLinearOperators(X,Y) holds it.x = upper_bound PreNorms(modetrans(x,X,Y)); existence proof deffunc F(object) = upper_bound PreNorms(modetrans(\$1,X,Y)); A1: for z be object st z in BoundedLinearOperators(X,Y) holds F(z) in REAL by XREAL_0:def 1; ex f being Function of BoundedLinearOperators(X,Y),REAL st for x being object st x in BoundedLinearOperators(X,Y) holds f.x = F(x) from FUNCT_2:sch 2(A1); hence thesis; end; uniqueness proof let NORM1,NORM2 be Function of BoundedLinearOperators(X,Y), REAL such that A2: for x be object st x in BoundedLinearOperators(X,Y) holds NORM1.x = upper_bound PreNorms(modetrans(x,X,Y)) and A3: for x be object st x in BoundedLinearOperators(X,Y) holds NORM2.x = upper_bound PreNorms(modetrans(x,X,Y)); A4: for z be object st z in BoundedLinearOperators(X,Y) holds NORM1.z = NORM2 .z proof let z be object such that A5: z in BoundedLinearOperators(X,Y); NORM1.z = upper_bound PreNorms(modetrans(z,X,Y)) by A2,A5; hence thesis by A3,A5; end; A6: dom NORM2 = BoundedLinearOperators(X,Y) by FUNCT_2:def 1; dom NORM1 = BoundedLinearOperators(X,Y) by FUNCT_2:def 1; hence thesis by A6,A4; end; end; theorem Th28: for X,Y be ComplexNormSpace, f be Lipschitzian LinearOperator of X,Y holds modetrans(f,X,Y)=f proof let X,Y be ComplexNormSpace; let f be Lipschitzian LinearOperator of X,Y; f in BoundedLinearOperators(X,Y) by Def7; hence thesis by Def9; end; theorem Th29: for X,Y be ComplexNormSpace, f be Lipschitzian LinearOperator of X,Y holds BoundedLinearOperatorsNorm(X,Y).f = upper_bound PreNorms(f) proof let X,Y be ComplexNormSpace; let f be Lipschitzian LinearOperator of X,Y; reconsider f9=f as set; f in BoundedLinearOperators(X,Y) by Def7; hence BoundedLinearOperatorsNorm(X,Y).f = upper_bound PreNorms(modetrans(f9,X,Y)) by Def11 .= upper_bound PreNorms(f) by Th28; end; definition let X,Y be ComplexNormSpace; func C_NormSpace_of_BoundedLinearOperators(X,Y) -> non empty CNORMSTR equals CNORMSTR (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y), C_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), C_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), C_VectorSpace_of_LinearOperators(X,Y)), BoundedLinearOperatorsNorm(X,Y) #); coherence; end; theorem Th30: for X,Y be ComplexNormSpace holds (the carrier of X) --> 0.Y = 0.C_NormSpace_of_BoundedLinearOperators(X,Y) proof let X,Y be ComplexNormSpace; ((the carrier of X) --> 0.Y) =0.C_VectorSpace_of_BoundedLinearOperators( X,Y) by Th25 .=0.C_NormSpace_of_BoundedLinearOperators(X,Y); hence thesis; end; theorem Th31: for X,Y be ComplexNormSpace, f being Point of C_NormSpace_of_BoundedLinearOperators(X,Y), g be Lipschitzian LinearOperator of X,Y st g=f holds for t be VECTOR of X holds ||.g.t.|| <= ||.f.|| * ||.t.|| proof let X,Y be ComplexNormSpace; let f being Point of C_NormSpace_of_BoundedLinearOperators(X,Y); let g be Lipschitzian LinearOperator of X,Y such that A1: g=f; A2: PreNorms(g) is non empty bounded_above by Th26; now let t be VECTOR of X; now per cases; case A3: t = 0.X; then A4: ||.t.|| = 0 by NORMSP_0:def 6; g.t =g.(0c * 0.X) by A3,CLVECT_1:1 .=0c * g.(0.X) by Def3 .=0.Y by CLVECT_1:1; hence ||.g.t.|| <= ||.f.||*||.t.|| by A4,NORMSP_0:def 6; end; case A5: t <> 0.X; reconsider t0 = ||.t.||"+0* as Element of COMPLEX by XCMPLX_0:def 2; reconsider t1= t0*t as VECTOR of X; A6: ||.t.|| <> 0 by A5,NORMSP_0:def 5; then A7: ||.t.|| > 0 by CLVECT_1:105; A8: |. t0 .| =|. 1*||.t.||" .| .=|. 1/||.t.||.| by XCMPLX_0:def 9 .=1/|. ||.t.||.| by ABSVALUE:7 .=1/||.t.|| by A7,ABSVALUE:def 1 .=1*||.t.||" by XCMPLX_0:def 9 .=||.t.||"; then A9: ||.g.t.||/||.t.|| =||.g.t.|| * |. t0 .| by XCMPLX_0:def 9 .=||.t0*g.t.|| by CLVECT_1:def 13 .=||.g.t1.|| by Def3; ||.t1.|| = |.t0.| * ||.t.|| by CLVECT_1:def 13 .=1 by A6,A8,XCMPLX_0:def 7; then ||.g.t.||/||.t.|| in {||.g.s.|| where s is VECTOR of X : ||.s.|| <= 1 } by A9; then ||.g.t.||/||.t.|| <= upper_bound PreNorms(g) by A2,SEQ_4:def 1; then ||.g.t.||/||.t.|| <= BoundedLinearOperatorsNorm(X,Y).g by Th29; then A10: ||.g.t.||/||.t.|| <= ||.f.|| by A1; ||.g.t.||/||.t.||*||.t.|| = ||.g.t.||*||.t.||"*||.t.|| by XCMPLX_0:def 9 .=||.g.t.||*(||.t.||"*||.t.||) .=||.g.t.||*1 by A6,XCMPLX_0:def 7 .=||.g.t.||; hence ||.g.t.|| <= ||.f.||*||.t.|| by A7,A10,XREAL_1:64; end; end; hence ||.g.t.|| <= ||.f.||*||.t.||; end; hence thesis; end; theorem Th32: for X,Y be ComplexNormSpace, f being Point of C_NormSpace_of_BoundedLinearOperators(X,Y) holds 0 <= ||.f.|| proof let X,Y be ComplexNormSpace; let f being Point of C_NormSpace_of_BoundedLinearOperators(X,Y); reconsider g=f as Lipschitzian LinearOperator of X,Y by Def7; consider r0 be object such that A1: r0 in PreNorms(g) by XBOOLE_0:def 1; reconsider r0 as Real by A1; A2: PreNorms(g) is non empty bounded_above by Th26; A3: BoundedLinearOperatorsNorm(X,Y).f = upper_bound PreNorms(g) by Th29; now let r be Real; assume r in PreNorms(g); then ex t be VECTOR of X st r=||.g.t.|| & ||.t.|| <= 1; hence 0 <= r by CLVECT_1:105; end; then 0 <= r0 by A1; then 0 <=upper_bound PreNorms(g) by A2,A1,SEQ_4:def 1; hence thesis by A3; end; theorem Th33: for X,Y be ComplexNormSpace, f being Point of C_NormSpace_of_BoundedLinearOperators(X,Y) st f = 0. C_NormSpace_of_BoundedLinearOperators(X,Y) holds 0 = ||.f.|| proof let X,Y be ComplexNormSpace; let f being Point of C_NormSpace_of_BoundedLinearOperators(X,Y) such that A1: f = 0.C_NormSpace_of_BoundedLinearOperators(X,Y); thus ||.f.|| = 0 proof reconsider g=f as Lipschitzian LinearOperator of X,Y by Def7; set z = (the carrier of X) --> 0.Y; reconsider z as Function of the carrier of X, the carrier of Y; consider r0 be object such that A2: r0 in PreNorms(g) by XBOOLE_0:def 1; reconsider r0 as Real by A2; A3: (for s be Real st s in PreNorms(g) holds s <= 0) implies upper_bound PreNorms(g) <= 0 by SEQ_4:45; A4: PreNorms(g) is non empty bounded_above by Th26; A5: z=g by A1,Th30; A6: now let r be Real; assume r in PreNorms(g); then consider t be VECTOR of X such that A7: r=||.g.t.|| and ||.t.|| <= 1; ||.g.t.|| = ||.0.Y.|| by A5,FUNCOP_1:7 .= 0 by NORMSP_0:def 6; hence 0 <= r & r <=0 by A7; end; then 0 <= r0 by A2; then upper_bound PreNorms(g) = 0 by A6,A4,A2,A3,SEQ_4:def 1; then BoundedLinearOperatorsNorm(X,Y).f=0 by Th29; hence thesis; end; end; registration let X,Y be ComplexNormSpace; cluster -> Function-like Relation-like for Element of C_NormSpace_of_BoundedLinearOperators(X,Y); coherence; end; definition let X,Y be ComplexNormSpace; let f be Element of C_NormSpace_of_BoundedLinearOperators(X,Y); let v be VECTOR of X; redefine func f.v -> VECTOR of Y; coherence proof reconsider f as LinearOperator of X,Y by Def7; f.v is VECTOR of Y; hence thesis; end; end; theorem Th34: for X,Y be ComplexNormSpace, f,g,h be Point of C_NormSpace_of_BoundedLinearOperators(X,Y) holds h = f+g iff for x be VECTOR of X holds h.x = f.x + g.x proof let X,Y be ComplexNormSpace; let f,g,h be Point of C_NormSpace_of_BoundedLinearOperators(X,Y); reconsider f1=f, g1=g, h1=h as VECTOR of C_VectorSpace_of_BoundedLinearOperators(X,Y); h=f+g iff h1=f1+g1; hence thesis by Th23; end; theorem Th35: for X,Y be ComplexNormSpace, f,h be Point of C_NormSpace_of_BoundedLinearOperators(X,Y), c be Complex holds h = c*f iff for x be VECTOR of X holds h.x = c * f.x proof let X,Y be ComplexNormSpace; let f,h be Point of C_NormSpace_of_BoundedLinearOperators(X,Y); let c be Complex; reconsider f1=f as VECTOR of C_VectorSpace_of_BoundedLinearOperators(X,Y); reconsider h1=h as VECTOR of C_VectorSpace_of_BoundedLinearOperators(X,Y); A1: now assume h1=c*f1; hence h=Mult_(BoundedLinearOperators(X,Y), C_VectorSpace_of_LinearOperators (X,Y)).[c,f1] by CLVECT_1:def 1 .=c*f by CLVECT_1:def 1; end; now assume h=c*f; hence h1=Mult_(BoundedLinearOperators(X,Y), C_VectorSpace_of_LinearOperators(X,Y)).[c,f] by CLVECT_1:def 1 .=c*f1 by CLVECT_1:def 1; end; hence thesis by A1,Th24; end; theorem Th36: for X,Y be ComplexNormSpace, f, g being Point of C_NormSpace_of_BoundedLinearOperators(X,Y), c be Complex holds ( ||.f.|| = 0 iff f = 0.C_NormSpace_of_BoundedLinearOperators(X,Y) ) & ||.c*f.|| = |.c.| * ||.f.|| & ||.f+g.|| <= ||.f.|| + ||.g.|| proof let X,Y be ComplexNormSpace; let f,g being Point of C_NormSpace_of_BoundedLinearOperators(X,Y); let c be Complex; A1: now assume A2: f = 0.C_NormSpace_of_BoundedLinearOperators(X,Y); thus ||.f.|| = 0 proof reconsider g=f as Lipschitzian LinearOperator of X,Y by Def7; set z = (the carrier of X) --> 0.Y; reconsider z as Function of the carrier of X, the carrier of Y; consider r0 be object such that A3: r0 in PreNorms(g) by XBOOLE_0:def 1; reconsider r0 as Real by A3; A4: (for s be Real st s in PreNorms(g) holds s <= 0) implies upper_bound PreNorms(g) <= 0 by SEQ_4:45; A5: PreNorms(g) is non empty bounded_above by Th26; A6: z=g by A2,Th30; A7: now let r be Real; assume r in PreNorms(g); then consider t be VECTOR of X such that A8: r=||.g.t.|| and ||.t.|| <= 1; ||.g.t.|| = ||.0.Y.|| by A6,FUNCOP_1:7 .= 0 by NORMSP_0:def 6; hence 0 <= r & r <=0 by A8; end; then 0<=r0 by A3; then upper_bound PreNorms(g) = 0 by A7,A5,A3,A4,SEQ_4:def 1; then BoundedLinearOperatorsNorm(X,Y).f =0 by Th29; hence thesis; end; end; A9: ||.f+g.|| <= ||.f.|| + ||.g.|| proof reconsider f1=f, g1=g, h1=f+g as Lipschitzian LinearOperator of X,Y by Def7; A10: (for s be Real st s in PreNorms(h1) holds s <= ||.f.|| + ||.g .||) implies upper_bound PreNorms(h1) <= ||.f.|| + ||.g.|| by SEQ_4:45; A11: now let t be VECTOR of X such that A12: ||.t.|| <= 1; 0 <= ||.g.|| by Th32; then A13: ||.g.||*||.t.|| <= ||.g.||*1 by A12,XREAL_1:64; 0 <= ||.f.|| by Th32; then ||.f.||*||.t.|| <= ||.f.||*1 by A12,XREAL_1:64; then A14: ||.f.||*||.t.|| + ||.g.||*||.t.|| <= ||.f.||*1 + ||.g.||*1 by A13, XREAL_1:7; A15: ||.f1.t+g1.t.|| <=||.f1.t.||+||.g1.t.|| by CLVECT_1:def 13; A16: ||.g1.t.||<= ||.g.||*||.t.|| by Th31; ||.f1.t.||<= ||.f.||*||.t.|| by Th31; then ||.f1.t.||+||.g1.t.|| <= ||.f.||*||.t.|| + ||.g.||*||.t.|| by A16, XREAL_1:7; then A17: ||.f1.t.||+||.g1.t.|| <= ||.f.|| + ||.g.|| by A14,XXREAL_0:2; ||.h1.t.||= ||.f1.t+g1.t.|| by Th34; hence ||.h1.t.|| <= ||.f.|| + ||.g.|| by A15,A17,XXREAL_0:2; end; A18: now let r be Real; assume r in PreNorms(h1); then ex t be VECTOR of X st r=||.h1.t.|| & ||.t.|| <= 1; hence r <= ||.f.|| + ||.g.|| by A11; end; BoundedLinearOperatorsNorm(X,Y).(f+g) = upper_bound PreNorms(h1) by Th29; hence thesis by A18,A10; end; A19: ||.c*f.|| = |.c.| * ||.f.|| proof reconsider f1=f, h1=c*f as Lipschitzian LinearOperator of X,Y by Def7; A20: (for s be Real st s in PreNorms(h1) holds s <= |.c.|*||.f.|| ) implies upper_bound PreNorms(h1) <= |.c.|*||.f.|| by SEQ_4:45; A21: now A22: 0 <= ||.f.|| by Th32; let t be VECTOR of X; assume ||.t.|| <= 1; then A23: ||.f.||*||.t.|| <= ||.f.||*1 by A22,XREAL_1:64; ||.f1.t.||<= ||.f.||*||.t.|| by Th31; then A24: ||.f1.t.|| <= ||.f.|| by A23,XXREAL_0:2; A25: ||.c*f1.t.|| =|.c.|*||.f1.t.|| by CLVECT_1:def 13; A26: 0<= |.c.| by COMPLEX1:46; ||.h1.t.||= ||.c*f1.t.|| by Th35; hence ||.h1.t.|| <= |.c.|*||.f.|| by A25,A24,A26,XREAL_1:64; end; A27: now let r be Real; assume r in PreNorms(h1); then ex t be VECTOR of X st r=||.h1.t.|| & ||.t.|| <= 1; hence r <= |.c.|*||.f.|| by A21; end; A28: now per cases; case A29: c <> 0c; A30: now A31: 0 <= ||.c*f.|| by Th32; let t be VECTOR of X; assume ||.t.|| <= 1; then A32: ||.c*f.||*||.t.|| <= ||.c*f.||*1 by A31,XREAL_1:64; ||.h1.t.||<= ||.c*f.||*||.t.|| by Th31; then A33: ||.h1.t.|| <= ||.c*f.|| by A32,XXREAL_0:2; h1.t=c*f1.t by Th35; then A34: c"*h1.t =( c"* c)*f1.t by CLVECT_1:def 4 .=1r*f1.t by A29,COMPLEX1:def 4,XCMPLX_0:def 7 .=f1.t by CLVECT_1:def 5; A35: |.c".| =|.c.|" by COMPLEX1:66; A36: 0<= |.c".| by COMPLEX1:46; ||.c"*h1.t.|| =|.c".|*||.h1.t.|| by CLVECT_1:def 13; hence ||.f1.t.|| <= |.c.|"*||.c*f.|| by A34,A33,A36,A35,XREAL_1:64; end; A37: now let r be Real; assume r in PreNorms(f1); then ex t be VECTOR of X st r=||.f1.t.|| & ||.t.|| <= 1; hence r <= |.c.|"*||.c*f.|| by A30; end; A38: (for s be Real st s in PreNorms(f1) holds s <= |.c.|"*||.c *f.|| ) implies upper_bound PreNorms(f1) <= |.c.|"*||.c*f.|| by SEQ_4:45; A39: 0 <= |.c.| by COMPLEX1:46; BoundedLinearOperatorsNorm(X,Y).(f) = upper_bound PreNorms(f1) by Th29; then ||.f.|| <=|.c.|"*||.c*f.|| by A37,A38; then |.c.|*||.f.|| <=|.c.|*(|.c.|"*||.c*f.||) by A39,XREAL_1:64; then A40: |.c.|*||.f.|| <=(|.c.|*|.c.|")*||.c*f.||; |.c.| <>0 by A29,COMPLEX1:47; then |.c.|*||.f.|| <=1*||.c*f.|| by A40,XCMPLX_0:def 7; hence |.c.|* ||.f.|| <=||.c*f.||; end; case A41: c = 0c; reconsider fz=f as VECTOR of C_VectorSpace_of_BoundedLinearOperators(X ,Y); c*f =Mult_(BoundedLinearOperators(X,Y), C_VectorSpace_of_LinearOperators(X,Y)).[c,f] by CLVECT_1:def 1 .=c*fz by CLVECT_1:def 1 .=0.C_VectorSpace_of_BoundedLinearOperators(X,Y) by A41,CLVECT_1:1 .=0.C_NormSpace_of_BoundedLinearOperators(X,Y); hence thesis by A41,Th33,COMPLEX1:44; end; end; BoundedLinearOperatorsNorm(X,Y).(c*f) = upper_bound PreNorms(h1) by Th29; then ||.c*f.|| <= |.c.|*||.f.|| by A27,A20; hence thesis by A28,XXREAL_0:1; end; now reconsider g=f as Lipschitzian LinearOperator of X,Y by Def7; set z = (the carrier of X) --> 0.Y; reconsider z as Function of the carrier of X, the carrier of Y; assume A42: ||.f.|| = 0; now let t be VECTOR of X; ||.g.t.|| <= ||.f.|| *||.t.|| by Th31; then ||.g.t.|| = 0 by A42,CLVECT_1:105; hence g.t =0.Y by NORMSP_0:def 5 .=z.t by FUNCOP_1:7; end; then g=z by FUNCT_2:63; hence f=0.C_NormSpace_of_BoundedLinearOperators(X,Y) by Th30; end; hence thesis by A1,A19,A9; end; theorem Th37: for X,Y be ComplexNormSpace holds C_NormSpace_of_BoundedLinearOperators(X,Y) is reflexive discerning ComplexNormSpace-like proof let X,Y be ComplexNormSpace; thus C_NormSpace_of_BoundedLinearOperators(X,Y) is reflexive by Th36; for x, y being Point of C_NormSpace_of_BoundedLinearOperators(X,Y) for c be Complex holds ( ||.x.|| = 0 iff x = 0.C_NormSpace_of_BoundedLinearOperators( X,Y) ) & ||.c*x.|| = |.c.| * ||.x.|| & ||.x+y.|| <= ||.x.|| + ||.y.|| by Th36; hence thesis by CLVECT_1:def 13; end; theorem Th38: for X,Y be ComplexNormSpace holds C_NormSpace_of_BoundedLinearOperators(X,Y) is ComplexNormSpace proof let X,Y be ComplexNormSpace; CLSStruct (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X ,Y), C_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), C_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), C_VectorSpace_of_LinearOperators(X,Y)) #) is ComplexLinearSpace; hence thesis by Th37,CSSPACE3:2; end; registration let X,Y be ComplexNormSpace; cluster C_NormSpace_of_BoundedLinearOperators(X,Y) -> reflexive discerning ComplexNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable; coherence by Th38; end; theorem Th39: for X,Y be ComplexNormSpace, f,g,h be Point of C_NormSpace_of_BoundedLinearOperators(X,Y) holds h = f-g iff for x be VECTOR of X holds h.x = f.x - g.x proof let X,Y be ComplexNormSpace; let f,g,h be Point of C_NormSpace_of_BoundedLinearOperators(X,Y); reconsider f9=f,g9=g,h9=h as Lipschitzian LinearOperator of X,Y by Def7; hereby assume h=f-g; then h+g=f-(g-g) by RLVECT_1:29; then h+g=f-0.C_NormSpace_of_BoundedLinearOperators(X,Y) by RLVECT_1:15; then A1: h+g=f by RLVECT_1:13; now let x be VECTOR of X; f9.x=h9.x + g9.x by A1,Th34; then f9.x-g9.x=h9.x + (g9.x-g9.x) by RLVECT_1:def 3; then f9.x-g9.x=h9.x + 0.Y by RLVECT_1:15; hence f9.x-g9.x=h9.x by RLVECT_1:4; end; hence for x be VECTOR of X holds h.x = f.x - g.x; end; assume A2: for x be VECTOR of X holds h.x = f.x - g.x; now let x be VECTOR of X; h9.x = f9.x - g9.x by A2; then h9.x + g9.x= f9.x - (g9.x- g9.x) by RLVECT_1:29; then h9.x + g9.x= f9.x - 0.Y by RLVECT_1:15; hence h9.x + g9.x= f9.x by RLVECT_1:13; end; then f=h+g by Th34; then f-g=h+(g-g) by RLVECT_1:def 3; then f-g=h+0.C_NormSpace_of_BoundedLinearOperators(X,Y) by RLVECT_1:15; hence thesis by RLVECT_1:4; end; begin :: Complex Banach Space of Bounded Linear Operators definition let X be ComplexNormSpace; attr X is complete means :Def13: for seq be sequence of X holds seq is Cauchy_sequence_by_Norm implies seq is convergent; end; registration cluster complete for ComplexNormSpace; existence by Def13,CSSPACE3:9; end; definition mode ComplexBanachSpace is complete ComplexNormSpace; end; Lm2: for e be Real, seq be Real_Sequence st ( seq is convergent & ex k be Nat st for i be Nat st k <= i holds seq.i <=e ) holds lim seq <=e proof let e be Real; let seq be Real_Sequence such that A1: seq is convergent and A2: ex k be Nat st for i be Nat st k <= i holds seq.i <=e; consider k be Nat such that A3: for i be Nat st k <= i holds seq.i <=e by A2; reconsider e as Element of REAL by XREAL_0:def 1; set cseq = seq_const e; A4: lim cseq = cseq.0 by SEQ_4:26 .= e by SEQ_1:57; A5: now let i be Nat; A6: (seq ^\k).i = seq.(k+i) by NAT_1:def 3; seq.(k+i) <=e by A3,NAT_1:11; hence (seq ^\k) .i <= cseq.i by A6,SEQ_1:57; end; lim (seq ^\k)=lim seq by A1,SEQ_4:20; hence thesis by A1,A5,A4,SEQ_2:18; end; theorem Th40: for X be ComplexNormSpace, seq be sequence of X st seq is convergent holds ||.seq.|| is convergent & lim ||.seq.|| = ||.lim seq.|| proof let X be ComplexNormSpace; let seq be sequence of X such that A1: seq is convergent; A2: now let e1 be Real such that A3: e1 >0; reconsider e =e1 as Real; consider k be Nat such that A4: for n be Nat st n >= k holds ||.seq.n - lim seq.|| < e by A1,A3,CLVECT_1:def 16; take k; now let m be Nat; assume m >= k; then A5: ||.seq.m - lim seq.|| = k holds |.||.seq.||.m - ||.lim seq .|| .| < e1; end; then ||.seq.|| is convergent by SEQ_2:def 6; hence thesis by A2,SEQ_2:def 7; end; theorem Th41: for X,Y be ComplexNormSpace st Y is complete for seq be sequence of C_NormSpace_of_BoundedLinearOperators(X,Y) st seq is Cauchy_sequence_by_Norm holds seq is convergent proof let X,Y be ComplexNormSpace such that A1: Y is complete; let vseq be sequence of C_NormSpace_of_BoundedLinearOperators(X,Y) such that A2: vseq is Cauchy_sequence_by_Norm; defpred P[set, set] means ex xseq be sequence of Y st (for n be Nat holds xseq.n=modetrans((vseq.n),X,Y).\$1) & xseq is convergent & \$2= lim xseq; A3: for x be Element of X ex y be Element of Y st P[x,y] proof let x be Element of X; deffunc F(Nat) = modetrans((vseq.\$1),X,Y).x; consider xseq be sequence of Y such that A4: for n be Element of NAT holds xseq.n = F(n) from FUNCT_2:sch 4; A5: for n be Nat holds xseq.n = F(n) proof let n be Nat; n in NAT by ORDINAL1:def 12; hence thesis by A4; end; take lim xseq; A6: for m,k be Nat holds ||.xseq.m-xseq.k.|| <= ||.vseq.m - vseq.k.|| * ||.x.|| proof let m,k be Nat; A7: k in NAT by ORDINAL1:def 12; A8: m in NAT by ORDINAL1:def 12; reconsider h1=vseq.m-vseq.k as Lipschitzian LinearOperator of X,Y by Def7; A9: xseq.k =modetrans((vseq.k),X,Y).x by A4,A7; vseq.m is Lipschitzian LinearOperator of X,Y by Def7; then A10: modetrans((vseq.m),X,Y)=vseq.m by Th28; vseq.k is Lipschitzian LinearOperator of X,Y by Def7; then A11: modetrans((vseq.k),X,Y)=vseq.k by Th28; xseq.m =modetrans((vseq.m),X,Y).x by A4,A8; then xseq.m - xseq.k = h1.x by A10,A11,A9,Th39; hence thesis by Th31; end; now let e be Real such that A12: e > 0; now per cases; case A13: x=0.X; take k=0; thus for n, m be Nat st n >= k & m >= k holds ||.xseq.n - xseq.m.|| < e proof let n, m be Nat such that n >= k and m >= k; A14: n in NAT by ORDINAL1:def 12; A15: m in NAT by ORDINAL1:def 12; A16: xseq.m=modetrans((vseq.m),X,Y).x by A4,A15 .=modetrans((vseq.m),X,Y).(0c*x) by A13,CLVECT_1:1 .=0c * modetrans((vseq.m),X,Y).x by Def3 .=0.Y by CLVECT_1:1; xseq.n=modetrans((vseq.n),X,Y).x by A4,A14 .=modetrans((vseq.n),X,Y).(0c * x) by A13,CLVECT_1:1 .=0c * modetrans((vseq.n),X,Y).x by Def3 .=0.Y by CLVECT_1:1; then ||.xseq.n -xseq.m.|| = ||.0.Y.|| by A16,RLVECT_1:13 .=0 by NORMSP_0:def 6; hence thesis by A12; end; end; case x <>0.X; then A17: ||.x.|| <> 0 by NORMSP_0:def 5; then A18: ||.x.|| > 0 by CLVECT_1:105; then consider k be Nat such that A19: for n, m be Nat st n >= k & m >= k holds ||.( vseq.n) - (vseq.m).|| < e/||.x.|| by A2,A12,CSSPACE3:8; take k; thus for n, m be Nat st n >= k & m >= k holds ||.xseq.n- xseq.m.|| < e proof let n,m be Nat such that A20: n >=k and A21: m >= k; ||.(vseq.n) - (vseq.m).|| < e/||.x.|| by A19,A20,A21; then A22: ||.(vseq.n) - (vseq.m).|| * ||.x.|| < e/||.x.|| * ||.x.|| by A18, XREAL_1:68; A23: e/||.x.|| * ||.x.|| = e*||.x.||"* ||.x.|| by XCMPLX_0:def 9 .= e*(||.x.||"* ||.x.||) .= e*1 by A17,XCMPLX_0:def 7 .=e; ||.xseq.n-xseq.m.|| <= ||.(vseq.n) - (vseq.m).|| * ||.x.|| by A6; hence thesis by A22,A23,XXREAL_0:2; end; end; end; hence ex k be Nat st for n, m be Nat st n >= k & m >= k holds ||.xseq.n -xseq.m.|| < e; end; then xseq is Cauchy_sequence_by_Norm by CSSPACE3:8; then xseq is convergent by A1; hence thesis by A5; end; consider f be Function of the carrier of X,the carrier of Y such that A24: for x be Element of X holds P[x,f.x] from FUNCT_2:sch 3(A3); reconsider tseq=f as Function of X,Y; A25: now let x,y be VECTOR of X; consider xseq be sequence of Y such that A26: for n be Nat holds xseq.n=modetrans((vseq.n),X,Y).x and A27: xseq is convergent and A28: tseq.x = lim xseq by A24; consider zseq be sequence of Y such that A29: for n be Nat holds zseq.n=modetrans((vseq.n),X,Y).(x+y ) and zseq is convergent and A30: tseq.(x+y) = lim zseq by A24; consider yseq be sequence of Y such that A31: for n be Nat holds yseq.n=modetrans((vseq.n),X,Y).y and A32: yseq is convergent and A33: tseq.y = lim yseq by A24; now let n be Nat; thus zseq.n=modetrans((vseq.n),X,Y).(x+y) by A29 .= modetrans((vseq.n),X,Y).x+modetrans((vseq.n),X,Y).y by VECTSP_1:def 20 .= xseq.n + modetrans((vseq.n),X,Y).y by A26 .= xseq.n +yseq.n by A31; end; then zseq=xseq+yseq by NORMSP_1:def 2; hence tseq.(x+y)=tseq.x+tseq.y by A27,A28,A32,A33,A30,CLVECT_1:119; end; now let x be VECTOR of X; let c be Complex; consider xseq be sequence of Y such that A34: for n be Nat holds xseq.n=modetrans((vseq.n),X,Y).x and A35: xseq is convergent and A36: tseq.x = lim xseq by A24; consider zseq be sequence of Y such that A37: for n be Nat holds zseq.n=modetrans((vseq.n),X,Y).(c*x ) and zseq is convergent and A38: tseq.(c*x) = lim zseq by A24; now let n be Nat; thus zseq.n=modetrans((vseq.n),X,Y).(c*x) by A37 .= c*modetrans((vseq.n),X,Y).x by Def3 .= c*xseq.n by A34; end; then zseq=c*xseq by CLVECT_1:def 14; hence tseq.(c*x)=c*tseq.x by A35,A36,A38,CLVECT_1:122; end; then reconsider tseq as LinearOperator of X,Y by A25,Def3,VECTSP_1:def 20; now let e1 be Real such that A39: e1 >0; reconsider e =e1 as Real; consider k be Nat such that A40: for n, m be Nat st n >= k & m >= k holds ||.(vseq.n) - (vseq.m).|| < e by A2,A39,CSSPACE3:8; take k; now let m be Nat; assume m >= k; then A41: ||.(vseq.m) - (vseq.k).|| = k holds |.||.vseq.||.m - ||.vseq.|| .k .| < e1; end; then A44: ||.vseq.|| is convergent by SEQ_4:41; A45: tseq is Lipschitzian proof take lim (||.vseq.|| ); A46: now let x be VECTOR of X; consider xseq be sequence of Y such that A47: for n be Nat holds xseq.n=modetrans((vseq.n),X,Y).x and A48: xseq is convergent and A49: tseq.x = lim xseq by A24; A50: ||.tseq.x.|| = lim ||.xseq.|| by A48,A49,Th19; A51: for m be Nat holds ||.xseq.m.|| <= ||.vseq.m.|| * ||.x .|| proof let m be Nat; A52: xseq.m =modetrans((vseq.m),X,Y).x by A47; vseq.m is Lipschitzian LinearOperator of X,Y by Def7; hence thesis by A52,Th28,Th31; end; A53: for n be Nat holds ||.xseq.||.n <=( ||.x.||(#)||.vseq.|| ).n proof let n be Nat; A54: ||.xseq.||.n = ||.(xseq.n).|| by NORMSP_0:def 4; A55: ||.vseq.n.|| = ||.vseq.||.n by NORMSP_0:def 4; ||.(xseq.n).|| <= ||.vseq.n.|| * ||.x.|| by A51; hence thesis by A54,A55,SEQ_1:9; end; A56: ||.x.||(#)||.vseq.|| is convergent by A44; A57: lim ( ||.x.||(#)||.vseq.|| ) = lim (||.vseq.|| )* ||.x.|| by A44,SEQ_2:8; ||.xseq.|| is convergent by A48,A49,Th19; hence ||.tseq.x.|| <= lim (||.vseq.|| )* ||.x.|| by A50,A53,A56,A57, SEQ_2:18; end; now let n be Nat; ||.vseq.n.|| >=0 by CLVECT_1:105; hence ||.vseq.||.n >=0 by NORMSP_0:def 4; end; hence thesis by A44,A46,SEQ_2:17; end; A58: for e be Real st e > 0 ex k be Nat st for n be Nat st n >= k for x be VECTOR of X holds ||.modetrans((vseq.n),X,Y).x - tseq.x.|| <= e* ||.x.|| proof let e be Real; assume e > 0; then consider k be Nat such that A59: for n, m be Nat st n >= k & m >= k holds ||.(vseq.n) - (vseq.m).|| < e by A2,CSSPACE3:8; take k; now let n be Nat such that A60: n >= k; now let x be VECTOR of X; consider xseq be sequence of Y such that A61: for n be Nat holds xseq.n=modetrans((vseq.n),X,Y). x and A62: xseq is convergent and A63: tseq.x = lim xseq by A24; A64: for m,k be Nat holds ||.xseq.m-xseq.k.|| <= ||.vseq.m - vseq.k.|| * ||.x.|| proof let m,k be Nat; reconsider h1=vseq.m-vseq.k as Lipschitzian LinearOperator of X,Y by Def7; A65: xseq.k =modetrans((vseq.k),X,Y).x by A61; vseq.m is Lipschitzian LinearOperator of X,Y by Def7; then A66: modetrans((vseq.m),X,Y)=vseq.m by Th28; vseq.k is Lipschitzian LinearOperator of X,Y by Def7; then A67: modetrans((vseq.k),X,Y)=vseq.k by Th28; xseq.m =modetrans((vseq.m),X,Y).x by A61; then xseq.m - xseq.k =h1.x by A66,A67,A65,Th39; hence thesis by Th31; end; A68: for m be Nat st m >=k holds ||.xseq.n-xseq.m.|| <= e * ||.x.|| proof let m be Nat; assume m >=k; then A69: ||.vseq.n - vseq.m.|| = k holds rseq.m <= e * ||.x.|| proof let m be Nat such that A75: m >=k; rseq.m = ||.xseq.m-xseq.n.|| by A71 .= ||.xseq.n-xseq.m.|| by CLVECT_1:108; hence thesis by A68,A75; end; then lim rseq <= e * ||.x.|| by A73,A72,Lm2,Th40; hence thesis by A74,CLVECT_1:108; end; hence ||.modetrans((vseq.n),X,Y).x - tseq.x.|| <= e* ||.x.|| by A61; end; hence for x be VECTOR of X holds ||.modetrans((vseq.n),X,Y).x - tseq.x.|| <= e* ||.x.||; end; hence thesis; end; reconsider tseq as Lipschitzian LinearOperator of X,Y by A45; reconsider tv=tseq as Point of C_NormSpace_of_BoundedLinearOperators(X,Y) by Def7; A76: for e be Real st e > 0 ex k be Nat st for n be Nat st n >= k holds ||.vseq.n - tv.|| <= e proof let e be Real such that A77: e > 0; consider k be Nat such that A78: for n be Nat st n >= k holds for x be VECTOR of X holds ||.modetrans((vseq.n),X,Y).x - tseq.x.|| <= e* ||.x.|| by A58,A77; now set g1=tseq; let n be Nat such that A79: n >= k; reconsider h1=vseq.n-tv as Lipschitzian LinearOperator of X,Y by Def7; set f1=modetrans((vseq.n),X,Y); A80: now let t be VECTOR of X; assume ||.t.|| <= 1; then A81: e*||.t.|| <= e*1 by A77,XREAL_1:64; A82: ||.f1.t-g1.t.|| <=e* ||.t.|| by A78,A79; vseq.n is Lipschitzian LinearOperator of X,Y by Def7; then modetrans((vseq.n),X,Y)=vseq.n by Th28; then ||.h1.t.||= ||.f1.t-g1.t.|| by Th39; hence ||.h1.t.|| <=e by A82,A81,XXREAL_0:2; end; A83: now let r be Real; assume r in PreNorms(h1); then ex t be VECTOR of X st r=||.h1.t.|| & ||.t.|| <= 1; hence r <=e by A80; end; A84: (for s be Real st s in PreNorms(h1) holds s <= e) implies upper_bound PreNorms(h1) <=e by SEQ_4:45; BoundedLinearOperatorsNorm(X,Y).(vseq.n-tv) = upper_bound PreNorms(h1) by Th29; hence ||.vseq.n-tv.|| <=e by A83,A84; end; hence thesis; end; for e be Real st e > 0 ex m be Nat st for n be Nat st n >= m holds ||.(vseq.n) - tv.|| < e proof let e be Real such that A85: e > 0; reconsider ee=e as Real; consider m be Nat such that A86: for n be Nat st n >= m holds ||.(vseq.n) - tv.|| <= ee /2 by A76,A85; A87: e/2= m; then ||.(vseq.n) - tv.|| <= e/2 by A86; hence ||.(vseq.n) - tv.|| < e by A87,XXREAL_0:2; end; hence thesis; end; hence thesis by CLVECT_1:def 15; end; theorem Th42: for X be ComplexNormSpace, Y be ComplexBanachSpace holds C_NormSpace_of_BoundedLinearOperators(X,Y) is ComplexBanachSpace proof let X be ComplexNormSpace; let Y be ComplexBanachSpace; for seq be sequence of C_NormSpace_of_BoundedLinearOperators(X,Y) st seq is Cauchy_sequence_by_Norm holds seq is convergent by Th41; hence thesis by Def13; end; registration let X be ComplexNormSpace; let Y be ComplexBanachSpace; cluster C_NormSpace_of_BoundedLinearOperators (X,Y) -> complete; coherence by Th42; end;