:: Complex {B}anach Space of Bounded Linear Operators
:: by Noboru Endou
::
:: Received February 24, 2004
:: Copyright (c) 2004-2026 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, 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); :: redefines [;] (FUNCOP_1, definition)
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; :: redefines . (FUNCT_1, definition)
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; :: redefines . (FUNCT_1, definition)
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; :: redefines . (FUNCT_1, definition)
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*<i> 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*<i> .| =|. 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*<i> 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; :: redefines . (FUNCT_1, definition)
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.|| <e by A4;
||.seq.m.||= ||.seq.||.m by NORMSP_0:def 4;
then |. ||.seq.||.m - ||.lim seq.|| .| <= ||.seq.m - lim seq.|| by
CLVECT_1:110;
hence |. ||.seq.||.m - ||.lim seq.|| .| <e1 by A5,XXREAL_0:2;
end;
hence for m be Nat st m >= 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).|| <e by A40;
A42: ||.vseq.m.||= ||.vseq.||.m by NORMSP_0:def 4;
A43: ||.vseq.k.||= ||.vseq.||.k by NORMSP_0:def 4;
|. ||.vseq.m.||- ||.vseq.k.|| .| <= ||.(vseq.m) - (vseq.k).|| by
CLVECT_1:110;
hence |. ||.vseq.||.m - ||.vseq.||.k .| <e1 by A43,A42,A41,XXREAL_0:2;
end;
hence
for m be Nat st m >= 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.|| <e by A59,A60;
A70: ||.xseq.n-xseq.m.|| <= ||.vseq.n - vseq.m.|| * ||.x.|| by A64;
0 <= ||.x.|| by CLVECT_1:105;
then ||.vseq.n - vseq.m.|| * ||.x.|| <= e* ||.x.|| by A69,XREAL_1:64;
hence thesis by A70,XXREAL_0:2;
end;
||.xseq.n-tseq.x.|| <= e * ||.x.||
proof
deffunc F(Nat) = ||.xseq.$1 - xseq.n.||;
consider rseq be Real_Sequence such that
A71: for m be Nat holds rseq.m = F(m) from SEQ_1:sch 1;
now
let x be object;
assume x in NAT;
then reconsider k=x as Nat;
thus rseq.x = ||.xseq.k - xseq.n.|| by A71
.= ||.(xseq - xseq.n).k.|| by NORMSP_1:def 4
.= ||.(xseq - xseq.n).||.x by NORMSP_0:def 4;
end;
then
A72: rseq = ||.xseq - xseq.n.|| by FUNCT_2:12;
A73: xseq - xseq.n is convergent by A62,CLVECT_1:115;
lim (xseq-xseq.n)= tseq.x - xseq.n by A62,A63,CLVECT_1:121;
then
A74: lim rseq = ||.tseq.x-xseq.n.|| by A73,A72,Th40;
for m be Nat st 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<e by A85,XREAL_1:216;
now
let n be Nat;
assume n >= 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;