:: Banach Space of Bounded Linear Operators
:: by Yasunari Shidama
::
:: Received December 22, 2003
:: Copyright (c) 2003-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, FUNCOP_1, SUBSET_1,
FUNCT_2, RELAT_1, PARTFUN1, ALGSTR_0, BINOP_1, STRUCT_0, RLVECT_1,
REAL_1, SUPINF_2, ARYTM_3, ARYTM_1, FUNCSDOM, MONOID_0, TARSKI, MSSUBFAM,
UNIALG_1, RLSUB_1, RSSPACE, NORMSP_1, NAT_1, PRE_TOPC, SEQ_2, ORDINAL2,
XXREAL_0, CARD_1, COMPLEX1, XXREAL_2, SEQ_4, REWRITE1, RSSPACE3, SEQ_1,
VALUED_1, LOPBAN_1, METRIC_1, RELAT_2, FCONT_1, ASYMPT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1,
FUNCT_2, FUNCT_3, PRE_TOPC, DOMAIN_1, FUNCOP_1, BINOP_1, XXREAL_0,
XXREAL_2, XCMPLX_0, COMPLEX1, REAL_1, ORDINAL1, NAT_1, STRUCT_0,
ALGSTR_0, XREAL_0, NUMBERS, MONOID_0, RLVECT_1, RLSUB_1, NORMSP_0,
NORMSP_1, RSSPACE, RSSPACE3, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SEQ_4,
FUNCSDOM, VECTSP_1;
constructors DOMAIN_1, FUNCT_3, XXREAL_0, REAL_1, NAT_1, COMPLEX1, SEQM_3,
RLSUB_1, FUNCSDOM, MONOID_0, MEASURE6, RSSPACE3, XXREAL_2, NORMSP_1,
SEQ_4, RELSET_1, BINOP_2, RVSUM_1, SEQ_2, COMSEQ_2, SEQ_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS,
XREAL_0, MEMBERED, STRUCT_0, RLVECT_1, NORMSP_1, MONOID_0, RSSPACE3,
VALUED_1, VALUED_0, SEQ_4, FUNCT_1, NORMSP_0, NAT_1, SEQ_1, SEQ_2;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions FUNCT_1, ALGSTR_0, VECTSP_1, NORMSP_0, XXREAL_2;
equalities RLVECT_1, BINOP_1, STRUCT_0, ALGSTR_0, NORMSP_0;
expansions FUNCT_1, BINOP_1, NORMSP_0;
theorems XBOOLE_0, TARSKI, ABSVALUE, RLVECT_1, FUNCOP_1, XREAL_0, XCMPLX_0,
SEQ_1, SEQ_2, FUNCT_1, NAT_1, FUNCT_2, RLSUB_1, NORMSP_1, SEQ_4, FUNCT_3,
RSSPACE, RSSPACE3, MONOID_0, XREAL_1, COMPLEX1, XXREAL_0, VECTSP_1,
NORMSP_0, ORDINAL1;
schemes BINOP_1, SEQ_1, FUNCT_2, XBOOLE_0;
begin :: Real Vector Space of Operators
definition
let X be set;
let Y be non empty set;
let F be Function of [:REAL, Y:], Y;
let a be Real, f be Function of X, Y;
redefine func F[;](a,f) -> Element of Funcs(X, Y); :: redefines [;] (FUNCOP_1, definition)
coherence
proof
A1: dom f = X by FUNCT_2:def 1;
a in REAL by XREAL_0:def 1;
then dom f --> a is Function of X,REAL by A1,FUNCOP_1:45;
then reconsider g = <:dom f --> a, f:> as Function of X,[:REAL, Y:] by
FUNCT_3:58;
F[;](a,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 non empty addLoopStr;
func FuncAdd(X,Y) -> BinOp of Funcs(X,the carrier of Y) means
:Def1:
for f,g being Element of Funcs(X,the carrier of Y)
holds it.(f,g) = (the addF of Y).:(f,g);
existence
proof
deffunc F(Element of Funcs(X,the carrier of Y), Element of Funcs(X,the
carrier of Y)) = (the addF of Y).:($1,$2);
thus ex ADD being BinOp of Funcs(X,the carrier of Y) st
for f,g being Element of Funcs(X,the carrier of Y)
holds ADD.(f,g) = F(f,g) from BINOP_1:sch 4;
end;
uniqueness
proof
let it1,it2 be BinOp of Funcs(X,the carrier of Y) such that
A1: for f,g being Element of Funcs(X,the carrier of Y) holds it1.(f,g)
= (the addF of Y).:(f,g) and
A2: for f,g being Element of Funcs(X,the carrier of Y) holds it2.(f,g)
= (the addF of Y).:(f,g);
now
let f,g be Element of Funcs(X,the carrier of Y);
thus it1.(f,g) = (the addF of Y).:(f,g) by A1
.= it2.(f,g) by A2;
end;
hence thesis;
end;
end;
definition
let X be non empty set;
let Y be RealLinearSpace;
func FuncExtMult(X,Y) -> Function of [:REAL,Funcs(X,the carrier of Y):],
Funcs(X,the carrier of Y) means
:Def2:
for a being Real, f being Element of
Funcs(X,the carrier of Y), x being Element of X holds (it.[a,f]).x = a*(f.x);
existence
proof
deffunc F(Real,Element of Funcs(X,the carrier of Y)) = ((the Mult of Y)[;](
$1,$2));
consider F being
Function of [:REAL,Funcs(X,the carrier of Y):], Funcs(X,the carrier of Y)
such that
A1: for a be Element of REAL,
f being Element of Funcs(X,the carrier of Y) holds F.
(a,f) = F(a,f) from BINOP_1:sch 4;
take F;
let a be Real,
f be Element of Funcs(X,the carrier of Y), x be Element of X;
reconsider a as Element of REAL by XREAL_0:def 1;
A2: dom (F.[a,f]) = X by FUNCT_2:92;
F.(a,f) = ((the Mult of Y)[;](a,f)) by A1;
hence thesis by A2,FUNCOP_1:32;
end;
uniqueness
proof
let it1,it2 be Function of [:REAL,Funcs(X,the carrier of Y):], Funcs(X,the
carrier of Y) such that
A3: for a being Real, f being Element of Funcs(X,the carrier of Y), x
being Element of X holds (it1.[a,f]).x = a*(f.x) and
A4: for a being Real, f being Element of Funcs(X,the carrier of Y), x
being Element of X holds (it2.[a,f]).x = a*(f.x);
now
let a be Element of REAL, f be Element of Funcs(X,the carrier of Y);
now
let x be Element of X;
thus (it1.[a,f]).x = a*(f.x) by A3
.= (it2.[a,f]).x by A4;
end;
hence it1.(a,f) = it2.(a,f) by FUNCT_2:63;
end;
hence thesis;
end;
end;
definition
let X be set;
let Y be non empty ZeroStr;
func FuncZero(X,Y) -> Element of Funcs (X,the carrier of Y) equals
X --> 0.Y;
coherence by FUNCT_2:8;
end;
reserve X for non empty set;
reserve Y for RealLinearSpace;
reserve f,g,h for Element of Funcs(X,the carrier of Y);
Lm1: for A,B be non empty set for x being Element of A, f being Function of A,
B holds x in dom f
proof
let A,B be non empty set;
let x be Element of A, f be Function of A,B;
x in A;
hence thesis by FUNCT_2:def 1;
end;
theorem Th1:
for Y being non empty addLoopStr, f,g,h being Element of Funcs(X,
the carrier of Y) holds h = FuncAdd(X,Y).(f,g) iff for x being Element of X
holds h.x = f.x + g.x
proof
let Y be non empty addLoopStr, f,g,h be Element of Funcs(X,the carrier of Y);
hereby
assume
A1: h = (FuncAdd(X,Y)).(f,g);
let x be Element of X;
A2: x in dom ((the addF of Y).:(f,g)) by Lm1;
thus h.x = ((the addF of Y).:(f,g)).x by A1,Def1
.= f.x + g.x by A2,FUNCOP_1:22;
end;
assume
A3: for x being Element of X holds h.x=f.x + g.x;
now
let x be Element of X;
A4: x in dom ((the addF of Y).:(f,g)) by Lm1;
thus ((FuncAdd(X,Y)).(f,g)).x = ((the addF of Y).:(f,g)).x by Def1
.= f.x + g.x by A4,FUNCOP_1:22
.= h.x by A3;
end;
hence h = (FuncAdd(X,Y)).(f,g) by FUNCT_2:63;
end;
reserve a,b for Real;
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 Def2;
reconsider a as Element of REAL by XREAL_0:def 1;
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 Def2;
end;
hence h = (FuncExtMult(X,Y)).[a,f] by FUNCT_2:63;
end;
hence thesis;
end;
reserve u,v,w for VECTOR of RLSStruct(#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 Th1
.= ((FuncAdd(X,Y)).(g,f)).x by Th1;
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 Th1
.= f.x + (g.x + h.x) by Th1
.= (f.x + g.x) + h.x by RLVECT_1:def 3
.= ((FuncAdd(X,Y)).(f,g)).x + h.x by Th1
.= ((FuncAdd(X,Y)).((FuncAdd(X,Y)).(f,g),h)).x by Th1;
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 Th1
.= 0.Y + f.x by FUNCOP_1:7
.= f.x;
end;
hence thesis by FUNCT_2:63;
end;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
theorem Th6:
(FuncAdd(X,Y)).(f,(FuncExtMult(X,Y)).[-1,f]) = FuncZero(X,Y)
proof
now
let x be Element of X;
set y=f.x;
thus ((FuncAdd(X,Y)).(f,(FuncExtMult(X,Y)).[-jj,f])).x = f.x + ((
FuncExtMult(X,Y)).[-jj,f]).x by Th1
.= f.x + ((-1)*y) by Th2
.= f.x + (-y) by RLVECT_1:16
.= 0.Y by RLVECT_1:5
.= (FuncZero(X,Y)).x by FUNCOP_1:7;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th7:
(FuncExtMult(X,Y)).[1,f] = f
proof
now
let x be Element of X;
thus ((FuncExtMult(X,Y)).[jj,f]).x = 1*(f.x) by Th2
.= f.x by RLVECT_1:def 8;
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 a,b as Element of REAL by XREAL_0:def 1;
now
let x be Element of X;
thus ((FuncExtMult(X,Y)).[a,(FuncExtMult(X,Y)).[b,f]]).x = a*(((
FuncExtMult(X,Y)).[b,f]).x) by Th2
.= a*(b*(f.x)) by Th2
.= (a*b)*(f.x) by RLVECT_1:def 7
.= ((FuncExtMult(X,Y)).[a*b,f]).x by Th2;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th9:
(FuncAdd(X,Y)). ((FuncExtMult(X,Y)).[a,f],(FuncExtMult(X,Y)).[b,
f]) = (FuncExtMult(X,Y)).[a+b,f]
proof
reconsider a,b as Element of REAL by XREAL_0:def 1;
now
let x be Element of X;
thus ((FuncAdd(X,Y)). ((FuncExtMult(X,Y)).[a,f],(FuncExtMult(X,Y)).[b,f]))
.x = ((FuncExtMult(X,Y)).[a,f]).x + ((FuncExtMult(X,Y)).[b,f]).x by Th1
.= a*(f.x) + ((FuncExtMult(X,Y)).[b,f]).x by Th2
.= a*(f.x) + b*(f.x) by Th2
.= (a+b)*(f.x) by RLVECT_1:def 6
.= ((FuncExtMult(X,Y)).[a+b,f]).x by Th2;
end;
hence thesis by FUNCT_2:63;
end;
Lm2: (FuncAdd(X,Y)). ((FuncExtMult(X,Y)).[a,f],(FuncExtMult(X,Y)).[a,g]) = (
FuncExtMult(X,Y)).[a,(FuncAdd(X,Y)).(f,g)]
proof
reconsider a as Element of REAL by XREAL_0:def 1;
now
let x be Element of X;
thus ((FuncAdd(X,Y)). ((FuncExtMult(X,Y)).[a,f],(FuncExtMult(X,Y)).[a,g]))
.x = ((FuncExtMult(X,Y)).[a,f]).x + ((FuncExtMult(X,Y)).[a,g]).x by Th1
.= a*(f.x) + ((FuncExtMult(X,Y)).[a,g]).x by Th2
.= a*(f.x) + a*(g.x) by Th2
.= a*(f.x + g.x) by RLVECT_1:def 5
.= a*(((FuncAdd(X,Y)).(f,g)).x) by Th1
.= ((FuncExtMult(X,Y)).[a,(FuncAdd(X,Y)).(f,g)]).x by Th2;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th10:
RLSStruct(#Funcs(X,the carrier of Y), (FuncZero(X,Y)),FuncAdd(X,
Y),FuncExtMult(X,Y)#) is RealLinearSpace
proof
A1: for a,b being Real,v holds (a*b)*v = a*(b*v)
by Th8;
A2: for a,b being Real,v holds (a+b)*v = a*v + b*v
by Th9;
set IT = RLSStruct(#Funcs(X,the carrier of Y), (FuncZero(X,Y)),FuncAdd(X,Y),
FuncExtMult(X,Y)#);
A3: (u+v)+w = u+(v+w) by Th4;
A4: IT is right_complementable
proof
let u;
reconsider u9 = u as Element of Funcs(X,the carrier of Y);
reconsider w = (FuncExtMult(X,Y)).[-jj,u9] as VECTOR of IT;
take w;
thus thesis by Th6;
end;
A5: for a being Real,u,v holds a*(u+v) = a*u + a *v
by Lm2;
A6: 1*v = v by Th7;
A7: 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;
u+v = v+u by Th3;
hence thesis by A3,A7,A4,A5,A2,A1,A6,RLVECT_1:def 2,def 3,def 4,def 5,def 6
,def 7,def 8;
end;
definition
let X be non empty set;
let Y be RealLinearSpace;
func RealVectSpace(X,Y) -> RealLinearSpace equals
RLSStruct(#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 RealLinearSpace;
cluster RealVectSpace(X,Y) -> strict;
coherence;
end;
registration
let X be non empty set;
let Y be RealLinearSpace;
cluster RealVectSpace(X,Y) -> constituted-Functions;
coherence by MONOID_0:80;
end;
definition
let X be non empty set;
let Y be RealLinearSpace;
let f be VECTOR of RealVectSpace(X,Y);
let x be Element of X;
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 for Y be RealLinearSpace for f,g,h be VECTOR of
RealVectSpace(X,Y) holds h = f+g iff for x be Element of X holds h.x = f.x + g.
x by Th1;
theorem
for X be non empty set for Y be RealLinearSpace for f,h be VECTOR of
RealVectSpace(X,Y) for a be Real holds h = a*f iff for x be Element of X holds
h.x = a * f.x by Th2;
theorem
for X be non empty set for Y be RealLinearSpace holds 0.RealVectSpace(
X,Y) = X --> 0.Y;
begin :: Real Vector Space of Linear Operators
definition
let X, Y be non empty RLSStruct;
let IT be Function of X,Y;
attr IT is homogeneous means
:Def5:
for x being VECTOR of X, r being Real holds IT.(r*x) = r*IT.x;
end;
registration
let X be non empty RLSStruct;
let Y be RealLinearSpace;
cluster additive homogeneous for Function of X,Y;
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
.= f.x+0.Y by FUNCOP_1:7
.= f.x+f.y by FUNCOP_1:7;
end;
hereby
let x be VECTOR of X, r be Real;
thus f.(r*x) =0.Y by FUNCOP_1:7
.=r*0.Y
.= r*f.x by FUNCOP_1:7;
end;
end;
end;
definition
let X, Y be RealLinearSpace;
mode LinearOperator of X,Y is additive homogeneous Function of X,Y;
end;
definition
let X, Y be RealLinearSpace;
func LinearOperators(X,Y) -> Subset of RealVectSpace(the carrier of X, Y)
means
:Def6:
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 RealVectSpace(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 RealVectSpace(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 RealLinearSpace;
cluster LinearOperators(X,Y) -> non empty functional;
coherence
proof
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, r be Real;
thus f.(r*x) =0.Y by FUNCOP_1:7
.=r*0.Y
.= r*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
.= 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,Def6;
let x be object;
assume x in LinearOperators(X,Y);
hence thesis;
end;
end;
theorem Th14:
for X, Y be RealLinearSpace holds LinearOperators(X,Y) is linearly-closed
proof
let X, Y be RealLinearSpace;
set W = LinearOperators(X,Y);
A1: for v,u be VECTOR of RealVectSpace(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 RealVectSpace(the carrier of X,Y) such that
A2: v in W and
A3: u in W;
v+u is LinearOperator of X,Y
proof
reconsider f=v+u as Function of X,Y by FUNCT_2:66;
A4: 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 Real;
A5: u9 is LinearOperator of X,Y by A3,Def6;
A6: v9 is LinearOperator of X,Y by A2,Def6;
thus f.(s*x) =u9.(s*x)+v9.(s*x) by Th1
.=(s*(u9.x))+v9.(s*x) by A5,Def5
.=s*u9.x+s*v9.x by A6,Def5
.=s*(u9.x+v9.x) by RLVECT_1:def 5
.= s*f.x by Th1;
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;
A7: u9 is LinearOperator of X,Y by A3,Def6;
A8: v9 is LinearOperator of X,Y by A2,Def6;
thus f.(x+y) =u9.(x+y)+v9.(x+y) by Th1
.=(u9.x+u9.y)+v9.(x+y) by A7,VECTSP_1:def 20
.=u9.x+u9.y+(v9.x+v9.y) by A8,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 Th1
.= f.x+ (u9.y+v9.y) by RLVECT_1:def 3
.= f.x+f.y by Th1;
end;
hence thesis by A4;
end;
hence thesis by Def6;
end;
for a be Real
for v be VECTOR of RealVectSpace(the carrier of X,Y) st v
in W holds a * v in W
proof
let a be Real;
let v be VECTOR of RealVectSpace(the carrier of X,Y) such that
A9: v in W;
a*v is LinearOperator of X,Y
proof
reconsider f=a*v as Function of X,Y by FUNCT_2:66;
A10: 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 Real;
A11: v9 is LinearOperator of X,Y by A9,Def6;
thus f.(s*x) =a*v9.(s*x) by Th2
.=a*(s*(v9.x)) by A11,Def5
.=a*s*v9.x by RLVECT_1:def 7
.=s*(a*v9.x) by RLVECT_1:def 7
.=s*f.x by 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;
A12: v9 is LinearOperator of X,Y by A9,Def6;
thus f.(x+y) = a*(v9.(x+y)) by Th2
.=a*(v9.x+v9.y) by A12,VECTSP_1:def 20
.=a*v9.x+a*v9.y by RLVECT_1:def 5
.=f.x+a*v9.y by Th2
.=f.x+ f.y by Th2;
end;
hence thesis by A10;
end;
hence thesis by Def6;
end;
hence thesis by A1,RLSUB_1:def 1;
end;
theorem
for X, Y be RealLinearSpace holds RLSStruct (# LinearOperators(X,Y),
Zero_(LinearOperators(X,Y),RealVectSpace(the carrier of X,Y)), Add_(
LinearOperators(X,Y), RealVectSpace(the carrier of X,Y)), Mult_(LinearOperators
(X,Y), RealVectSpace(the carrier of X,Y)) #) is Subspace of RealVectSpace(the
carrier of X,Y) by Th14,RSSPACE:11;
registration
let X, Y be RealLinearSpace;
cluster RLSStruct (# LinearOperators(X,Y), Zero_(LinearOperators(X,Y),
RealVectSpace(the carrier of X,Y)), Add_(LinearOperators(X,Y), RealVectSpace(
the carrier of X,Y)), Mult_(LinearOperators(X,Y), RealVectSpace(the carrier of
X,Y)) #) -> Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital;
coherence by Th14,RSSPACE:11;
end;
definition
let X, Y be RealLinearSpace;
func R_VectorSpace_of_LinearOperators(X,Y) -> RealLinearSpace equals
RLSStruct (# LinearOperators(X,Y), Zero_(LinearOperators(X,Y),RealVectSpace(the
carrier of X,Y)), Add_(LinearOperators(X,Y), RealVectSpace(the carrier of X,Y))
, Mult_(LinearOperators(X,Y), RealVectSpace(the carrier of X,Y)) #);
coherence;
end;
registration
let X, Y be RealLinearSpace;
cluster R_VectorSpace_of_LinearOperators(X,Y) -> strict;
coherence;
end;
registration
let X,Y be RealLinearSpace;
cluster R_VectorSpace_of_LinearOperators(X,Y) -> constituted-Functions;
coherence by MONOID_0:80;
end;
definition
let X,Y be RealLinearSpace;
let f be Element of R_VectorSpace_of_LinearOperators(X,Y);
let v be VECTOR of X;
redefine func f.v -> VECTOR of Y; :: redefines . (FUNCT_1, definition)
coherence
proof
reconsider f as LinearOperator of X,Y by Def6;
f.v is VECTOR of Y;
hence thesis;
end;
end;
theorem Th16:
for X, Y be RealLinearSpace for f,g,h be VECTOR of
R_VectorSpace_of_LinearOperators(X,Y) holds h = f+g iff for x be VECTOR of X
holds h.x = f.x + g.x
proof
let X, Y be RealLinearSpace;
let f,g,h be VECTOR of R_VectorSpace_of_LinearOperators(X,Y);
reconsider f9=f,g9=g,h9=h as LinearOperator of X,Y by Def6;
A1: R_VectorSpace_of_LinearOperators(X,Y) is Subspace of RealVectSpace(the
carrier of X,Y) by Th14,RSSPACE:11;
then reconsider f1=f as VECTOR of RealVectSpace(the carrier of X,Y) by
RLSUB_1:10;
reconsider h1=h as VECTOR of RealVectSpace(the carrier of X,Y) by A1,
RLSUB_1:10;
reconsider g1=g as VECTOR of RealVectSpace(the carrier of X,Y) by A1,
RLSUB_1:10;
A2: now
assume
A3: h = f+g;
let x be Element of X;
h1=f1+g1 by A1,A3,RLSUB_1:13;
hence h9.x=f9.x+g9.x by Th1;
end;
now
assume for x be Element of X holds h9.x=f9.x+g9.x;
then h1=f1+g1 by Th1;
hence h =f+g by A1,RLSUB_1:13;
end;
hence thesis by A2;
end;
theorem Th17:
for X, Y be RealLinearSpace for f,h be VECTOR of
R_VectorSpace_of_LinearOperators(X,Y)
for a be Real holds h = a*f iff for x be
VECTOR of X holds h.x = a * f.x
proof
let X, Y be RealLinearSpace;
let f,h be VECTOR of R_VectorSpace_of_LinearOperators(X,Y);
reconsider f9=f,h9=h as LinearOperator of X,Y by Def6;
let a be Real;
A1: R_VectorSpace_of_LinearOperators(X,Y) is Subspace of RealVectSpace(the
carrier of X,Y) by Th14,RSSPACE:11;
then reconsider f1=f as VECTOR of RealVectSpace(the carrier of X,Y) by
RLSUB_1:10;
reconsider h1=h as VECTOR of RealVectSpace(the carrier of X,Y) by A1,
RLSUB_1:10;
A2: now
assume
A3: h = a*f;
let x be Element of X;
h1=a*f1 by A1,A3,RLSUB_1:14;
hence h9.x=a*f9.x by Th2;
end;
now
assume for x be Element of X holds h9.x=a*f9.x;
then h1=a*f1 by Th2;
hence h =a*f by A1,RLSUB_1:14;
end;
hence thesis by A2;
end;
theorem Th18:
for X, Y be RealLinearSpace holds 0.
R_VectorSpace_of_LinearOperators(X,Y) = (the carrier of X) -->0.Y
proof
let X, Y be RealLinearSpace;
A1: 0.RealVectSpace(the carrier of X,Y) =((the carrier of X) -->0.Y);
R_VectorSpace_of_LinearOperators(X,Y) is Subspace of RealVectSpace(the
carrier of X,Y) by Th14,RSSPACE:11;
hence thesis by A1,RLSUB_1:11;
end;
theorem Th19:
for X,Y be RealLinearSpace holds (the carrier of X) --> 0.Y is
LinearOperator of X,Y
proof
let X,Y be RealLinearSpace;
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, r be Real;
thus f.(r*x) =0.Y by FUNCOP_1:7
.=r*0.Y
.= r*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
.= f.x+0.Y by FUNCOP_1:7
.= f.x+f.y by FUNCOP_1:7;
end;
hence thesis by A1;
end;
begin :: Real Normed Linear Space of Bounded Linear Operators
theorem Th20:
for X be RealNormSpace for seq be sequence of X for g be Point
of X holds seq is convergent & lim seq = g implies ||.seq.|| is convergent &
lim ||.seq.|| = ||.g.||
proof
let X be RealNormSpace;
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,
NORMSP_1:def 7;
reconsider k = m1 as Nat;
take k;
now
let n be Nat;
assume n >= k;
then
A6: ||.(seq.n) - g.|| < r by A5;
|.||.(seq.n).|| - ||.g.||.| <= ||.(seq.n) - g.|| by NORMSP_1:9;
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,NORMSP_1:23;
hence thesis by A3,SEQ_2:def 7;
end;
definition
let X, Y be RealNormSpace;
let IT be LinearOperator of X,Y;
attr IT is Lipschitzian means
:Def8:
ex K being Real st 0 <= K &
for x being VECTOR of X holds ||. IT.x .|| <= K * ||. x .||;
end;
theorem Th21:
for X, Y be RealNormSpace holds for f be LinearOperator of X,Y
st (for x be VECTOR of X holds f.x=0.Y) holds f is Lipschitzian
proof
let X, Y be RealNormSpace;
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 .||;
end;
take 0;
thus thesis by A2;
end;
registration
let X, Y be RealNormSpace;
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 Th19;
take f;
for x be VECTOR of X holds f.x =0.Y by FUNCOP_1:7;
hence thesis by Th21;
end;
end;
definition
let X, Y be RealNormSpace;
func BoundedLinearOperators(X,Y) -> Subset of
R_VectorSpace_of_LinearOperators(X,Y) means
:Def9:
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 R_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 Def6;
hence thesis by A1,A2;
end;
uniqueness
proof
let X1,X2 be Subset of R_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 RealNormSpace;
cluster BoundedLinearOperators(X,Y) -> non empty;
coherence
proof
set f=(the carrier of X) --> 0.Y;
reconsider f as LinearOperator of X,Y by Th19;
for x be VECTOR of X holds f.x =0.Y by FUNCOP_1:7;
then f is Lipschitzian by Th21;
hence thesis by Def9;
end;
end;
theorem Th22:
for X, Y be RealNormSpace holds BoundedLinearOperators(X,Y) is
linearly-closed
proof
let X, Y be RealNormSpace;
set W = BoundedLinearOperators(X,Y);
A1: for v,u be VECTOR of R_VectorSpace_of_LinearOperators(X, Y) st v in W &
u in W holds v + u in W
proof
let v,u be VECTOR of R_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 Def6;
f is Lipschitzian
proof
reconsider v1=v as Lipschitzian LinearOperator of X,Y by A2,Def9;
consider K2 be Real such that
A4: 0 <= K2 and
A5: for x be VECTOR of X holds ||. v1.x .|| <= K2*||. x .|| by Def8;
reconsider u1=u as Lipschitzian LinearOperator of X,Y by A3,Def9;
consider K1 be Real such that
A6: 0 <= K1 and
A7: for x be VECTOR of X holds ||. u1.x .|| <= K1*||. x .|| by Def8;
take K3=K1+K2;
now
let x be VECTOR of X;
A8: ||. u1.x+v1.x .|| <= ||. u1.x .||+ ||. v1.x .|| by NORMSP_1:def 1;
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 Th16;
hence ||. f.x .|| <= K3*||. x .|| by A8,A10,XXREAL_0:2;
end;
hence thesis by A6,A4;
end;
hence thesis by Def9;
end;
for a be Real
for v be VECTOR of R_VectorSpace_of_LinearOperators(X,Y)
st v in W holds a * v in W
proof
let a be Real;
let v be VECTOR of R_VectorSpace_of_LinearOperators(X,Y) such that
A11: v in W;
reconsider f=a*v as LinearOperator of X,Y by Def6;
f is Lipschitzian
proof
reconsider v1=v as Lipschitzian LinearOperator of X,Y by A11,Def9;
consider K be Real such that
A12: 0 <= K and
A13: for x be VECTOR of X holds ||. v1.x .|| <= K*||. x .|| by Def8;
take |.a.|*K;
A14: now
let x be VECTOR of X;
0 <=|.a.| by COMPLEX1:46;
then
A15: |.a.|* ||. v1.x .|| <= |.a.|* (K*||. x .||) by A13,XREAL_1:64;
||. a*v1.x .|| = |.a.|* ||. v1.x .|| by NORMSP_1:def 1;
hence ||. f.x .|| <= |.a.|* K*||. x .|| by A15,Th17;
end;
0 <=|.a.| by COMPLEX1:46;
hence thesis by A12,A14;
end;
hence thesis by Def9;
end;
hence thesis by A1,RLSUB_1:def 1;
end;
theorem
for X, Y be RealNormSpace holds RLSStruct (# BoundedLinearOperators(X,
Y), Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)),
Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Mult_
(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)) #) is
Subspace of R_VectorSpace_of_LinearOperators(X,Y) by Th22,RSSPACE:11;
registration
let X, Y be RealNormSpace;
cluster RLSStruct (# BoundedLinearOperators(X,Y), Zero_(
BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Add_(
BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Mult_(
BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)) #) ->
Abelian add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital;
coherence by Th22,RSSPACE:11;
end;
definition
let X, Y be RealNormSpace;
func R_VectorSpace_of_BoundedLinearOperators(X,Y) -> RealLinearSpace equals
RLSStruct (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y),
R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y),
R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y),
R_VectorSpace_of_LinearOperators(X,Y)) #);
coherence;
end;
registration
let X, Y be RealNormSpace;
cluster R_VectorSpace_of_BoundedLinearOperators(X,Y) -> strict;
coherence;
end;
registration
let X,Y be RealNormSpace;
cluster -> Function-like Relation-like for Element of
R_VectorSpace_of_BoundedLinearOperators(X,Y);
coherence;
end;
definition
let X,Y be RealNormSpace;
let f be Element of R_VectorSpace_of_BoundedLinearOperators(X,Y);
let v be VECTOR of X;
redefine func f.v -> VECTOR of Y; :: redefines . (FUNCT_1, definition)
coherence
proof
reconsider f as LinearOperator of X,Y by Def9;
f.v is VECTOR of Y;
hence thesis;
end;
end;
theorem Th24:
for X, Y be RealNormSpace for f,g,h be VECTOR of
R_VectorSpace_of_BoundedLinearOperators(X,Y) holds h = f+g iff for x be VECTOR
of X holds h.x = f.x + g.x
proof
let X, Y be RealNormSpace;
let f,g,h be VECTOR of R_VectorSpace_of_BoundedLinearOperators(X,Y);
A1: R_VectorSpace_of_BoundedLinearOperators(X,Y) is Subspace of
R_VectorSpace_of_LinearOperators(X,Y) by Th22,RSSPACE:11;
then reconsider f1=f as VECTOR of R_VectorSpace_of_LinearOperators(X,Y) by
RLSUB_1:10;
reconsider h1=h as VECTOR of R_VectorSpace_of_LinearOperators(X,Y) by A1,
RLSUB_1:10;
reconsider g1=g as VECTOR of R_VectorSpace_of_LinearOperators(X,Y) by A1,
RLSUB_1:10;
hereby
assume
A2: h = f+g;
let x be Element of X;
h1=f1+g1 by A1,A2,RLSUB_1:13;
hence h.x=f.x+g.x by Th16;
end;
assume for x be Element of X holds h.x=f.x+g.x;
then h1=f1+g1 by Th16;
hence thesis by A1,RLSUB_1:13;
end;
theorem Th25:
for X, Y be RealNormSpace for f,h be VECTOR of
R_VectorSpace_of_BoundedLinearOperators(X,Y)
for a be Real holds h = a*f iff
for x be VECTOR of X holds h.x = a * f.x
proof
let X, Y be RealNormSpace;
let f,h be VECTOR of R_VectorSpace_of_BoundedLinearOperators(X,Y);
let a be Real;
A1: R_VectorSpace_of_BoundedLinearOperators(X,Y) is Subspace of
R_VectorSpace_of_LinearOperators(X,Y) by Th22,RSSPACE:11;
then reconsider f1=f as VECTOR of R_VectorSpace_of_LinearOperators(X,Y) by
RLSUB_1:10;
reconsider h1=h as VECTOR of R_VectorSpace_of_LinearOperators(X,Y) by A1,
RLSUB_1:10;
hereby
assume
A2: h = a*f;
let x be Element of X;
h1=a*f1 by A1,A2,RLSUB_1:14;
hence h.x=a*f.x by Th17;
end;
assume for x be Element of X holds h.x=a*f.x;
then h1=a*f1 by Th17;
hence thesis by A1,RLSUB_1:14;
end;
theorem Th26:
for X, Y be RealNormSpace holds 0.
R_VectorSpace_of_BoundedLinearOperators(X,Y) = (the carrier of X) --> 0.Y
proof
let X, Y be RealNormSpace;
A1: 0.R_VectorSpace_of_LinearOperators(X,Y) =((the carrier of X) -->0.Y) by
Th18;
R_VectorSpace_of_BoundedLinearOperators(X,Y) is Subspace of
R_VectorSpace_of_LinearOperators(X,Y) by Th22,RSSPACE:11;
hence thesis by A1,RLSUB_1:11;
end;
definition
let X, Y be RealNormSpace;
let f be object such that :: !!! zastapic przez In(.,.)
A1: f in BoundedLinearOperators(X,Y);
func modetrans(f,X,Y) -> Lipschitzian LinearOperator of X,Y equals
:Def11:
f;
coherence by A1,Def9;
end;
definition
let X, Y be RealNormSpace;
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;
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 Th27:
for X, Y be RealNormSpace for g be Lipschitzian LinearOperator of X,Y
holds PreNorms(g) is bounded_above
proof
let X, Y be RealNormSpace;
let g be Lipschitzian LinearOperator of X,Y;
consider K be Real such that
A1: 0 <= K and
A2: for x be VECTOR of X holds ||. g.x .|| <= K*||. x .|| by Def8;
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;
theorem
for X, Y be RealNormSpace for g be LinearOperator of X,Y holds g is
Lipschitzian iff PreNorms(g) is bounded_above
proof
let X, Y be RealNormSpace;
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;
g.t = g.(0*0.X) by A3
.=0*g.(0.X) by Def5
.=0.Y by RLVECT_1:10;
hence ||.g.t.|| <= K*||.t.|| by A4;
end;
case
A5: t <> 0.X;
reconsider t1= ( ||.t.||")*t as VECTOR of X;
A6: ||.t.|| <> 0 by A5,NORMSP_0:def 5;
A7: ||.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.||;
A8: |. ||.t.||".| = |. 1*||.t.||".| .=|. 1/||.t.||.| by XCMPLX_0:def 9
.=1/|. ||.t.||.| by ABSVALUE:7
.=1/||.t.|| by ABSVALUE:def 1
.=1*||.t.||" by XCMPLX_0:def 9
.=||.t.||";
||.t1.|| =|. ||.t.||".|*||.t.|| by NORMSP_1:def 1
.=1 by A6,A8,XCMPLX_0:def 7;
then
A9: ||.g.t1.|| in {||.g.s.|| where s is VECTOR of X : ||.s.|| <= 1 };
||.g.t.||/||.t.|| = ||.g.t.||*||.t.||" by XCMPLX_0:def 9
.=||. ||.t.||"*g.t.|| by A8,NORMSP_1:def 1
.=||.g.t1.|| by Def5;
then ||.g.t.||/||.t.|| <= K by A1,A9,SEQ_4:def 1;
hence ||.g.t.|| <= K *||.t.|| by A7,XREAL_1:64;
end;
end;
hence ||.g.t.|| <= K*||.t.||;
end;
take K;
0 <= K
proof
consider r0 be object such that
A10: r0 in PreNorms(g) by XBOOLE_0:def 1;
reconsider r0 as Real by A10;
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;
end;
then 0 <= r0 by A10;
hence thesis by A1,A10,SEQ_4:def 1;
end;
hence g is Lipschitzian by A2;
end;
hence thesis by Th27;
end;
definition
let X, Y be RealNormSpace;
func BoundedLinearOperatorsNorm(X,Y) -> Function of BoundedLinearOperators(X
,Y), REAL means
:Def13:
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;
thus 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);
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 Th29:
for X, Y be RealNormSpace for f be Lipschitzian LinearOperator of X,Y
holds modetrans(f,X,Y)=f
proof
let X, Y be RealNormSpace;
let f be Lipschitzian LinearOperator of X,Y;
f in BoundedLinearOperators(X,Y) by Def9;
hence thesis by Def11;
end;
theorem Th30:
for X, Y be RealNormSpace for f be Lipschitzian LinearOperator of X,Y
holds BoundedLinearOperatorsNorm(X,Y).f = upper_bound PreNorms(f)
proof
let X, Y be RealNormSpace;
let f be Lipschitzian LinearOperator of X,Y;
reconsider f9=f as set;
f in BoundedLinearOperators(X,Y) by Def9;
hence BoundedLinearOperatorsNorm(X,Y).f =
upper_bound PreNorms(modetrans(f9,X,Y)) by Def13
.= upper_bound PreNorms(f) by Th29;
end;
definition
let X, Y be RealNormSpace;
func R_NormSpace_of_BoundedLinearOperators(X,Y) -> non empty NORMSTR equals
NORMSTR (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y),
R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y),
R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y),
R_VectorSpace_of_LinearOperators(X,Y)), BoundedLinearOperatorsNorm(X,Y) #);
coherence;
end;
theorem Th31:
for X, Y be RealNormSpace holds (the carrier of X) --> 0.Y = 0.
R_NormSpace_of_BoundedLinearOperators(X,Y)
proof
let X, Y be RealNormSpace;
((the carrier of X) --> 0.Y) =0.R_VectorSpace_of_BoundedLinearOperators(
X,Y) by Th26
.=0.R_NormSpace_of_BoundedLinearOperators(X,Y);
hence thesis;
end;
theorem Th32:
for X, Y be RealNormSpace for f being Point of
R_NormSpace_of_BoundedLinearOperators(X,Y)
for g be Lipschitzian LinearOperator of X
,Y st g=f holds for t be VECTOR of X holds ||.g.t.|| <= ||.f.|| * ||.t.||
proof
let X, Y be RealNormSpace;
let f being Point of R_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 Th27;
now
let t be VECTOR of X;
now
per cases;
case
A3: t = 0.X;
then
A4: ||.t.|| = 0;
g.t =g.(0*0.X) by A3
.=0*g.(0.X) by Def5
.=0.Y by RLVECT_1:10;
hence ||.g.t.|| <= ||.f.||*||.t.|| by A4;
end;
case
A5: t <> 0.X;
reconsider t1= ( ||.t.||")*t as VECTOR of X;
A6: ||.t.|| <> 0 by A5,NORMSP_0:def 5;
A7: |. ||.t.||".| =|. 1*||.t.||".| .=|. 1/||.t.||.| by XCMPLX_0:def 9
.=1/|. ||.t.||.| by ABSVALUE:7
.=1/||.t.|| by ABSVALUE:def 1
.=1*||.t.||" by XCMPLX_0:def 9
.=||.t.||";
A8: ||.g.t.||/||.t.|| = ||.g.t.||*||.t.||" by XCMPLX_0:def 9
.=||. ||.t.||"*g.t.|| by A7,NORMSP_1:def 1
.=||.g.t1.|| by Def5;
||.t1.|| =|. ||.t.||".|*||.t.|| by NORMSP_1:def 1
.=1 by A6,A7,XCMPLX_0:def 7;
then ||.g.t.||/||.t.|| in {||.g.s.|| where s is VECTOR of X : ||.s.||
<= 1 } by A8;
then ||.g.t.||/||.t.|| <= upper_bound PreNorms(g) by A2,SEQ_4:def 1;
then ||.g.t.||/||.t.|| <= BoundedLinearOperatorsNorm(X,Y).g by Th30;
then
A9: ||.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 A9,XREAL_1:64;
end;
end;
hence ||.g.t.|| <= ||.f.||*||.t.||;
end;
hence thesis;
end;
theorem Th33:
for X, Y be RealNormSpace for f being Point of
R_NormSpace_of_BoundedLinearOperators(X,Y) holds 0 <= ||.f.||
proof
let X, Y be RealNormSpace;
let f being Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
reconsider g=f as Lipschitzian LinearOperator of X,Y by Def9;
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 Th27;
A3: BoundedLinearOperatorsNorm(X,Y).f = upper_bound PreNorms(g) by Th30;
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;
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 Th34:
for X, Y be RealNormSpace for f being Point of
R_NormSpace_of_BoundedLinearOperators(X,Y) st f = 0.
R_NormSpace_of_BoundedLinearOperators(X,Y) holds 0 = ||.f.||
proof
let X, Y be RealNormSpace;
let f being Point of R_NormSpace_of_BoundedLinearOperators(X,Y) such that
A1: f = 0.R_NormSpace_of_BoundedLinearOperators(X,Y);
thus ||.f.|| = 0
proof
reconsider g=f as Lipschitzian LinearOperator of X,Y by Def9;
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 Th27;
A5: z=g by A1,Th31;
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;
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 Th30;
hence thesis;
end;
end;
registration
let X,Y be RealNormSpace;
cluster -> Function-like Relation-like for Element of
R_NormSpace_of_BoundedLinearOperators(X,Y);
coherence;
end;
definition
let X,Y be RealNormSpace;
let f be Element of R_NormSpace_of_BoundedLinearOperators(X,Y);
let v be VECTOR of X;
redefine func f.v -> VECTOR of Y; :: redefines . (FUNCT_1, definition)
coherence
proof
reconsider f as LinearOperator of X,Y by Def9;
f.v is VECTOR of Y;
hence thesis;
end;
end;
theorem Th35:
for X, Y be RealNormSpace for f,g,h be Point of
R_NormSpace_of_BoundedLinearOperators(X,Y) holds h = f+g iff for x be VECTOR of
X holds h.x = f.x + g.x
proof
let X, Y be RealNormSpace;
let f,g,h be Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
reconsider f1=f, g1=g, h1=h as VECTOR of
R_VectorSpace_of_BoundedLinearOperators(X,Y);
h=f+g iff h1=f1+g1;
hence thesis by Th24;
end;
theorem Th36:
for X, Y be RealNormSpace for f,h be Point of
R_NormSpace_of_BoundedLinearOperators(X,Y)
for a be Real holds h = a*f iff for
x be VECTOR of X holds h.x = a * f.x
proof
let X, Y be RealNormSpace;
let f,h be Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
let a be Real;
reconsider f1=f as VECTOR of R_VectorSpace_of_BoundedLinearOperators(X,Y);
reconsider h1=h as VECTOR of R_VectorSpace_of_BoundedLinearOperators(X,Y);
h=a*f iff h1=a*f1;
hence thesis by Th25;
end;
theorem Th37:
for X be RealNormSpace for Y be RealNormSpace for f, g being
Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
for a be Real holds ( ||.f
.|| = 0 iff f = 0.R_NormSpace_of_BoundedLinearOperators(X,Y) ) & ||.a*f.|| =
|.a.| * ||.f.|| & ||.f+g.|| <= ||.f.|| + ||.g.||
proof
let X be RealNormSpace;
let Y be RealNormSpace;
let f, g being Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
let a be Real;
A1: now
assume
A2: f = 0.R_NormSpace_of_BoundedLinearOperators(X,Y);
thus ||.f.|| = 0
proof
reconsider g=f as Lipschitzian LinearOperator of X,Y by Def9;
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 Th27;
A6: z=g by A2,Th31;
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;
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 Th30;
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 Def9;
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 Th33;
then
A13: ||.g.||*||.t.|| <= ||.g.||*1 by A12,XREAL_1:64;
0 <= ||.f.|| by Th33;
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 NORMSP_1:def 1;
A16: ||.g1.t.||<= ||.g.||*||.t.|| by Th32;
||.f1.t.||<= ||.f.||*||.t.|| by Th32;
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 Th35;
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 Th30;
hence thesis by A18,A10;
end;
A19: ||.a*f.|| = |.a.| * ||.f.||
proof
reconsider f1=f, h1=a*f as Lipschitzian LinearOperator of X,Y by Def9;
A20: (for s be Real st s in PreNorms(h1) holds s <= |.a.|*||.f.||
) implies upper_bound PreNorms(h1) <= |.a.|*||.f.|| by SEQ_4:45;
A21: now
A22: 0 <= ||.f.|| by Th33;
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 Th32;
then
A24: ||.f1.t.|| <= ||.f.|| by A23,XXREAL_0:2;
A25: ||.a*f1.t.|| =|.a.|*||.f1.t.|| by NORMSP_1:def 1;
A26: 0<= |.a.| by COMPLEX1:46;
||.h1.t.||= ||.a*f1.t.|| by Th36;
hence ||.h1.t.|| <= |.a.|*||.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 <= |.a.|*||.f.|| by A21;
end;
A28: now
per cases;
case
A29: a <> 0;
A30: now
A31: 0 <= ||.a*f.|| by Th33;
let t be VECTOR of X;
assume ||.t.|| <= 1;
then
A32: ||.a*f.||*||.t.|| <= ||.a*f.||*1 by A31,XREAL_1:64;
||.h1.t.||<= ||.a*f.||*||.t.|| by Th32;
then
A33: ||.h1.t.|| <= ||.a*f.|| by A32,XXREAL_0:2;
h1.t=a*f1.t by Th36;
then
A34: a"*h1.t =( a"* a)*f1.t by RLVECT_1:def 7
.=1*f1.t by A29,XCMPLX_0:def 7
.=f1.t by RLVECT_1:def 8;
A35: |.a".| =|.1*a".| .=|. 1/a.| by XCMPLX_0:def 9
.=1/|.a.| by ABSVALUE:7
.=1*|.a.|" by XCMPLX_0:def 9
.=|.a.|";
A36: 0<= |.a".| by COMPLEX1:46;
||.a"*h1.t.|| =|.a".|*||.h1.t.|| by NORMSP_1:def 1;
hence ||.f1.t.|| <= |.a.|"*||.a*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 <= |.a.|"*||.a*f.|| by A30;
end;
A38: ( for s be Real st s in PreNorms(f1) holds s <= |.a.|"*
||.a*f.|| ) implies upper_bound PreNorms(f1) <= |.a.|"*||.a*f.||
by SEQ_4:45;
A39: 0 <= |.a.| by COMPLEX1:46;
BoundedLinearOperatorsNorm(X,Y).(f) = upper_bound PreNorms(f1) by Th30;
then ||.f.|| <=|.a.|"*||.a*f.|| by A37,A38;
then |.a.|*||.f.|| <=|.a.|*(|.a.|"*||.a*f.||) by A39,XREAL_1:64;
then
A40: |.a.|*||.f.|| <=(|.a.|*|.a.|")*||.a*f.||;
|.a.| <>0 by A29,COMPLEX1:47;
then |.a.|*||.f.|| <=1*||.a*f.|| by A40,XCMPLX_0:def 7;
hence |.a.|* ||.f.|| <=||.a*f.||;
end;
case
A41: a=0;
reconsider fz=f as VECTOR of R_VectorSpace_of_BoundedLinearOperators(X
,Y);
A42: a*f =a*fz
.=0.R_VectorSpace_of_BoundedLinearOperators(X,Y) by A41,RLVECT_1:10
.=0.R_NormSpace_of_BoundedLinearOperators(X,Y);
thus |.a.|* ||.f.|| =0 * ||.f.|| by A41,ABSVALUE:2
.=||.a*f.|| by A42,Th34;
end;
end;
BoundedLinearOperatorsNorm(X,Y).(a*f) = upper_bound PreNorms(h1) by Th30;
then ||.a*f.|| <= |.a.|*||.f.|| by A27,A20;
hence thesis by A28,XXREAL_0:1;
end;
now
reconsider g=f as Lipschitzian LinearOperator of X,Y by Def9;
set z = (the carrier of X) --> 0.Y;
reconsider z as Function of the carrier of X, the carrier of Y;
assume
A43: ||.f.|| = 0;
now
let t be VECTOR of X;
||.g.t.|| <= ||.f.|| *||.t.|| by Th32;
then ||.g.t.|| = 0 by A43;
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.R_NormSpace_of_BoundedLinearOperators(X,Y) by Th31;
end;
hence thesis by A1,A19,A9;
end;
theorem Th38:
for X,Y be RealNormSpace holds R_NormSpace_of_BoundedLinearOperators(X,Y) is
reflexive discerning RealNormSpace-like
proof
let X,Y be RealNormSpace;
thus ||.0.R_NormSpace_of_BoundedLinearOperators(X,Y).|| = 0 by Th37;
for x, y being Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
for a be Real
holds ( ||.x.|| = 0 iff x = 0.R_NormSpace_of_BoundedLinearOperators(X,Y
) ) & ||.a*x.|| = |.a.| * ||.x.|| & ||.x+y.|| <= ||.x.|| + ||.y.|| by Th37;
hence thesis by NORMSP_1:def 1;
end;
theorem Th39:
for X, Y be RealNormSpace holds
R_NormSpace_of_BoundedLinearOperators(X,Y) is RealNormSpace
proof
let X, Y be RealNormSpace;
RLSStruct (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X
,Y), R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y),
R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y),
R_VectorSpace_of_LinearOperators(X,Y)) #) is RealLinearSpace;
hence thesis by Th38,RSSPACE3:2;
end;
registration
let X, Y be RealNormSpace;
cluster R_NormSpace_of_BoundedLinearOperators(X,Y) ->
reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable;
coherence by Th39;
end;
theorem Th40:
for X, Y be RealNormSpace for f,g,h be Point of
R_NormSpace_of_BoundedLinearOperators(X,Y) holds h = f-g iff for x be VECTOR of
X holds h.x = f.x - g.x
proof
let X, Y be RealNormSpace;
let f,g,h be Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
reconsider f9=f,g9=g,h9=h as Lipschitzian LinearOperator of X,Y by Def9;
hereby
assume h=f-g;
then h+g=f-(g-g) by RLVECT_1:29;
then h+g=f-0.R_NormSpace_of_BoundedLinearOperators(X,Y) by RLVECT_1:15;
then
A1: h+g=f;
now
let x be VECTOR of X;
f9.x=h9.x + g9.x by A1,Th35;
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;
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;
end;
then f=h+g by Th35;
then f-g=h+(g-g) by RLVECT_1:def 3;
then f-g=h+0.R_NormSpace_of_BoundedLinearOperators(X,Y) by RLVECT_1:15;
hence thesis;
end;
begin :: Real Banach Space of Bounded Linear Operators
definition
let X be RealNormSpace;
attr X is complete means
:Def15:
for seq be sequence of X holds seq is
Cauchy_sequence_by_Norm implies seq is convergent;
end;
registration
cluster complete for RealNormSpace;
existence
by Def15,RSSPACE3:9;
end;
definition
mode RealBanachSpace is complete RealNormSpace;
end;
Lm3: 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 ee=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 Th41:
for X be RealNormSpace for seq be sequence of X st seq is
convergent holds ||.seq.|| is convergent & lim ||.seq.|| = ||.lim seq.||
proof
let X be RealNormSpace;
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,NORMSP_1:def 7;
reconsider k as Nat;
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
NORMSP_1:9;
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 Th42:
for X, Y be RealNormSpace st Y is complete for seq be sequence
of R_NormSpace_of_BoundedLinearOperators(X,Y) st seq is Cauchy_sequence_by_Norm
holds seq is convergent
proof
let X, Y be RealNormSpace such that
A1: Y is complete;
let vseq be sequence of R_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;
reconsider h1=vseq.m-vseq.k as Lipschitzian LinearOperator of X,Y
by Def9;
k in NAT by ORDINAL1:def 12;
then
A7: xseq.k =modetrans((vseq.k),X,Y).x by A4;
vseq.m is Lipschitzian LinearOperator of X,Y by Def9;
then
A8: modetrans((vseq.m),X,Y)=vseq.m by Th29;
vseq.k is Lipschitzian LinearOperator of X,Y by Def9;
then
A9: modetrans((vseq.k),X,Y)=vseq.k by Th29;
m in NAT by ORDINAL1:def 12;
then
xseq.m =modetrans((vseq.m),X,Y).x by A4;
then xseq.m - xseq.k = h1.x by A8,A9,A7,Th40;
hence thesis by Th32;
end;
now
let e be Real such that
A10: e > 0;
now
per cases;
case
A11: x=0.X;
reconsider k=0 as Nat;
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
n >= k and
m >= k;
m in NAT by ORDINAL1:def 12;
then
A12: xseq.m=modetrans((vseq.m),X,Y).x by A4
.=modetrans((vseq.m),X,Y).(0*x) by A11
.=0*modetrans((vseq.m),X,Y).x by Def5
.=0.Y by RLVECT_1:10;
n in NAT by ORDINAL1:def 12;
then
xseq.n=modetrans((vseq.n),X,Y).x by A4
.=modetrans((vseq.n),X,Y).(0*x) by A11
.=0*modetrans((vseq.n),X,Y).x by Def5
.=0.Y by RLVECT_1:10;
then ||.xseq.n -xseq.m.|| = ||.0.Y.|| by A12
.=0;
hence thesis by A10;
end;
end;
case
x <>0.X;
then
A13: ||.x.|| <> 0 by NORMSP_0:def 5;
then
A14: ||.x.|| > 0;
then e/||.x.||>0 by A10,XREAL_1:139;
then consider k be Nat such that
A15: for n, m be Nat st n >= k & m >= k holds ||.(
vseq.n) - (vseq.m).|| < e/||.x.|| by A2,RSSPACE3: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
A16: n >=k and
A17: m >= k;
||.(vseq.n) - (vseq.m).|| < e/||.x.|| by A15,A16,A17;
then
A18: ||.(vseq.n) - (vseq.m).|| * ||.x.|| < e/||.x.|| * ||.x.|| by A14,
XREAL_1:68;
A19: e/||.x.|| * ||.x.|| = e*||.x.||"* ||.x.|| by XCMPLX_0:def 9
.= e*(||.x.||"* ||.x.||)
.= e*1 by A13,XCMPLX_0:def 7
.=e;
||.xseq.n-xseq.m.|| <= ||.(vseq.n) - (vseq.m).|| * ||.x.|| by A6;
hence thesis by A18,A19,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 RSSPACE3: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
A20: 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;
A21: now
let x,y be VECTOR of X;
consider xseq be sequence of Y such that
A22: for n be Nat holds xseq.n=modetrans((vseq.n),X,Y).x and
A23: xseq is convergent and
A24: tseq.x = lim xseq by A20;
consider zseq be sequence of Y such that
A25: for n be Nat holds zseq.n=modetrans((vseq.n),X,Y).(x+y ) and
zseq is convergent and
A26: tseq.(x+y) = lim zseq by A20;
consider yseq be sequence of Y such that
A27: for n be Nat holds yseq.n=modetrans((vseq.n),X,Y).y and
A28: yseq is convergent and
A29: tseq.y = lim yseq by A20;
now
let n be Nat;
thus zseq.n=modetrans((vseq.n),X,Y).(x+y) by A25
.= 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 A22
.= xseq.n +yseq.n by A27;
end;
then zseq=xseq+yseq by NORMSP_1:def 2;
hence tseq.(x+y)=tseq.x+tseq.y by A23,A24,A28,A29,A26,NORMSP_1:25;
end;
now
let x be VECTOR of X;
let a be Real;
consider xseq be sequence of Y such that
A30: for n be Nat holds xseq.n=modetrans((vseq.n),X,Y).x and
A31: xseq is convergent and
A32: tseq.x = lim xseq by A20;
consider zseq be sequence of Y such that
A33: for n be Nat holds zseq.n=modetrans((vseq.n),X,Y).(a*x ) and
zseq is convergent and
A34: tseq.(a*x) = lim zseq by A20;
now
let n be Nat;
thus zseq.n=modetrans((vseq.n),X,Y).(a*x) by A33
.= a*modetrans((vseq.n),X,Y).x by Def5
.= a*xseq.n by A30;
end;
then zseq=a*xseq by NORMSP_1:def 5;
hence tseq.(a*x)=a*tseq.x by A31,A32,A34,NORMSP_1:28;
end;
then reconsider tseq as LinearOperator of X,Y by A21,Def5,VECTSP_1:def 20;
now
let e1 be Real such that
A35: e1 >0;
reconsider e =e1 as Real;
consider k be Nat such that
A36: for n, m be Nat st n >= k & m >= k holds ||.(vseq.n) -
(vseq.m).|| < e by A2,A35,RSSPACE3:8;
reconsider k as Nat;
take k;
now
let m be Nat;
assume m >= k;
then
A37: ||.(vseq.m) - (vseq.k).|| <e by A36;
A38: ||.vseq.m.||= ||.vseq.||.m by NORMSP_0:def 4;
A39: ||.vseq.k.||= ||.vseq.||.k by NORMSP_0:def 4;
|. ||.vseq.m.||- ||.vseq.k.|| .| <= ||.(vseq.m) - (vseq.k).|| by
NORMSP_1:9;
hence |. ||.vseq.||.m - ||.vseq.||.k .| <e1 by A39,A38,A37,XXREAL_0:2;
end;
hence
for m be Nat st m >= k holds |.||.vseq.||.m - ||.vseq.||
.k .| < e1;
end;
then
A40: ||.vseq.|| is convergent by SEQ_4:41;
A41: tseq is Lipschitzian
proof
take lim (||.vseq.|| );
A42: now
let x be VECTOR of X;
consider xseq be sequence of Y such that
A43: for n be Nat holds xseq.n=modetrans((vseq.n),X,Y).x and
A44: xseq is convergent and
A45: tseq.x = lim xseq by A20;
A46: ||.tseq.x.|| = lim ||.xseq.|| by A44,A45,Th20;
A47: for m be Nat holds ||.xseq.m.|| <= ||.vseq.m.|| * ||.x .||
proof
let m be Nat;
A48: xseq.m =modetrans((vseq.m),X,Y).x by A43;
vseq.m is Lipschitzian LinearOperator of X,Y by Def9;
hence thesis by A48,Th29,Th32;
end;
A49: for n be Nat holds ||.xseq.||.n <= ( ||.x.||(#)||.vseq .||).n
proof
let n be Nat;
A50: ||.xseq.||.n = ||.(xseq.n).|| by NORMSP_0:def 4;
A51: ||.vseq.n.|| = ||.vseq.||.n by NORMSP_0:def 4;
||.(xseq.n).|| <= ||.vseq.n.|| * ||.x.|| by A47;
hence thesis by A50,A51,SEQ_1:9;
end;
A52: ||.x.||(#)||.vseq.|| is convergent by A40;
A53: lim ( ||.x.||(#)||.vseq.|| ) = lim (||.vseq.|| )* ||.x.|| by A40,SEQ_2:8;
||.xseq.|| is convergent by A44,A45,Th20;
hence ||.tseq.x.|| <= lim (||.vseq.|| )* ||.x.|| by A46,A49,A52,A53,
SEQ_2:18;
end;
now
let n be Nat;
||.vseq.n.|| >=0;
hence ||.vseq.||.n >=0 by NORMSP_0:def 4;
end;
hence thesis by A40,A42,SEQ_2:17;
end;
A54: for e be Real
st e > 0 ex k be Nat st 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.||
proof
let e be Real;
assume e > 0;
then consider k be Nat such that
A55: for n, m be Nat st n >= k & m >= k holds ||.(vseq.n) -
(vseq.m).|| < e by A2,RSSPACE3:8;
take k;
now
let n be Nat such that
A56: n >= k;
now
let x be VECTOR of X;
consider xseq be sequence of Y such that
A57: for n be Nat holds xseq.n=modetrans((vseq.n),X,Y). x and
A58: xseq is convergent and
A59: tseq.x = lim xseq by A20;
A60: 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 Def9;
A61: xseq.k =modetrans((vseq.k),X,Y).x by A57;
vseq.m is Lipschitzian LinearOperator of X,Y by Def9;
then
A62: modetrans((vseq.m),X,Y)=vseq.m by Th29;
vseq.k is Lipschitzian LinearOperator of X,Y by Def9;
then
A63: modetrans((vseq.k),X,Y)=vseq.k by Th29;
xseq.m =modetrans((vseq.m),X,Y).x by A57;
then xseq.m - xseq.k =h1.x by A62,A63,A61,Th40;
hence thesis by Th32;
end;
A64: for m be Nat st m >=k holds ||.xseq.n-xseq.m.|| <= e *
||.x.||
proof
let m be Nat;
assume m >=k;
then
A65: ||.vseq.n - vseq.m.|| <e by A55,A56;
A66: ||.xseq.n-xseq.m.|| <= ||.vseq.n - vseq.m.|| * ||.x.|| by A60;
||.vseq.n - vseq.m.|| * ||.x.|| <= e* ||.x.|| by A65,XREAL_1:64;
hence thesis by A66,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
A67: 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 A67
.= ||.(xseq - xseq.n).k.|| by NORMSP_1:def 4
.= ||.(xseq - xseq.n).||.x by NORMSP_0:def 4;
end;
then
A68: rseq = ||.xseq - xseq.n.|| by FUNCT_2:12;
A69: xseq - xseq.n is convergent by A58,NORMSP_1:21;
lim (xseq-xseq.n)= tseq.x - xseq.n by A58,A59,NORMSP_1:27;
then
A70: lim rseq = ||.tseq.x-xseq.n.|| by A69,A68,Th41;
for m be Nat st m >= k holds rseq.m <= e * ||.x.||
proof
let m be Nat such that
A71: m >=k;
rseq.m = ||.xseq.m-xseq.n.|| by A67
.= ||.xseq.n-xseq.m.|| by NORMSP_1:7;
hence thesis by A64,A71;
end;
then lim rseq <= e * ||.x.|| by A69,A68,Lm3,Th41;
hence thesis by A70,NORMSP_1:7;
end;
hence ||.modetrans((vseq.n),X,Y).x - tseq.x.|| <= e* ||.x.|| by A57;
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 A41;
reconsider tv=tseq as Point of R_NormSpace_of_BoundedLinearOperators(X,Y) by
Def9;
A72: 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
A73: e > 0;
consider k be Nat such that
A74: 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 A54,A73;
now
set g1=tseq;
let n be Nat such that
A75: n >= k;
reconsider h1=vseq.n-tv as Lipschitzian LinearOperator of X,Y by Def9;
set f1=modetrans((vseq.n),X,Y);
A76: now
let t be VECTOR of X;
assume ||.t.|| <= 1;
then
A77: e*||.t.|| <= e*1 by A73,XREAL_1:64;
A78: ||.f1.t-g1.t.|| <=e* ||.t.|| by A74,A75;
vseq.n is Lipschitzian LinearOperator of X,Y by Def9;
then modetrans((vseq.n),X,Y)=vseq.n by Th29;
then ||.h1.t.||= ||.f1.t-g1.t.|| by Th40;
hence ||.h1.t.|| <=e by A78,A77,XXREAL_0:2;
end;
A79: 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 A76;
end;
A80: (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 Th30;
hence ||.vseq.n-tv.|| <=e by A79,A80;
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
A81: e > 0;
consider m be Nat such that
A82: for n be Nat st n >= m holds ||.(vseq.n) - tv.|| <= e
/2 by A72,A81,XREAL_1:215;
A83: e/2<e by A81,XREAL_1:216;
now
let n be Nat;
assume n >= m;
then ||.(vseq.n) - tv.|| <= e/2 by A82;
hence ||.(vseq.n) - tv.|| < e by A83,XXREAL_0:2;
end;
hence thesis;
end;
hence thesis by NORMSP_1:def 6;
end;
theorem Th43:
for X be RealNormSpace for Y be RealBanachSpace holds
R_NormSpace_of_BoundedLinearOperators(X,Y) is RealBanachSpace
proof
let X be RealNormSpace;
let Y be RealBanachSpace;
for seq be sequence of R_NormSpace_of_BoundedLinearOperators(X,Y) st seq
is Cauchy_sequence_by_Norm holds seq is convergent by Th42;
hence thesis by Def15;
end;
registration
let X be RealNormSpace;
let Y be RealBanachSpace;
cluster R_NormSpace_of_BoundedLinearOperators (X,Y) -> complete;
coherence by Th43;
end;