let X, Y be ComplexNormSpace; :: thesis: ( Y is complete implies for seq being sequence of (C_NormSpace_of_BoundedLinearOperators X,Y) st seq is CCauchy holds
seq is convergent )
assume A1:
Y is complete
; :: thesis: for seq being sequence of (C_NormSpace_of_BoundedLinearOperators X,Y) st seq is CCauchy holds
seq is convergent
let vseq be sequence of (C_NormSpace_of_BoundedLinearOperators X,Y); :: thesis: ( vseq is CCauchy implies vseq is convergent )
assume A2:
vseq is CCauchy
; :: thesis: vseq is convergent
A3:
||.vseq.|| is convergent
defpred S1[ set , set ] means ex xseq being sequence of Y st
( ( for n being Element of NAT holds xseq . n = (modetrans (vseq . n),X,Y) . $1 ) & xseq is convergent & $2 = lim xseq );
A11:
for x being Element of X ex y being Element of Y st S1[x,y]
proof
let x be
Element of
X;
:: thesis: ex y being Element of Y st S1[x,y]
deffunc H1(
Element of
NAT )
-> Element of the
carrier of
Y =
(modetrans (vseq . $1),X,Y) . x;
consider xseq being
sequence of
Y such that A12:
for
n being
Element of
NAT holds
xseq . n = H1(
n)
from FUNCT_2:sch 4();
A13:
for
m,
k being
Element of
NAT holds
||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||
proof
let m,
k be
Element of
NAT ;
:: thesis: ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||
vseq . m is
bounded LinearOperator of
X,
Y
by Def8;
then A14:
modetrans (vseq . m),
X,
Y = vseq . m
by Th33;
vseq . k is
bounded LinearOperator of
X,
Y
by Def8;
then A15:
modetrans (vseq . k),
X,
Y = vseq . k
by Th33;
reconsider h1 =
(vseq . m) - (vseq . k) as
bounded LinearOperator of
X,
Y by Def8;
A16:
xseq . m = (modetrans (vseq . m),X,Y) . x
by A12;
xseq . k = (modetrans (vseq . k),X,Y) . x
by A12;
then
(xseq . m) - (xseq . k) = h1 . x
by A14, A15, A16, Th44;
hence
||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||
by Th36;
:: thesis: verum
end;
A17:
xseq is
convergent
proof
now let e be
Real;
:: thesis: ( e > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e )assume A18:
e > 0
;
:: thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < ethus
ex
k being
Element of
NAT st
for
n,
m being
Element of
NAT st
n >= k &
m >= k holds
||.((xseq . n) - (xseq . m)).|| < e
:: thesis: verumproof
now per cases
( x = 0. X or x <> 0. X )
;
case A19:
x = 0. X
;
:: thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < etake k =
0 ;
:: thesis: for n, m being Element of NAT st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < ethus
for
n,
m being
Element of
NAT st
n >= k &
m >= k holds
||.((xseq . n) - (xseq . m)).|| < e
:: thesis: verumproof
let n,
m be
Element of
NAT ;
:: thesis: ( n >= k & m >= k implies ||.((xseq . n) - (xseq . m)).|| < e )
assume
(
n >= k &
m >= k )
;
:: thesis: ||.((xseq . n) - (xseq . m)).|| < e
A20:
xseq . n =
(modetrans (vseq . n),X,Y) . x
by A12
.=
(modetrans (vseq . n),X,Y) . (0c * x)
by A19, CLVECT_1:2
.=
0c * ((modetrans (vseq . n),X,Y) . x)
by Def4
.=
0. Y
by CLVECT_1:2
;
xseq . m =
(modetrans (vseq . m),X,Y) . x
by A12
.=
(modetrans (vseq . m),X,Y) . (0c * x)
by A19, CLVECT_1:2
.=
0c * ((modetrans (vseq . m),X,Y) . x)
by Def4
.=
0. Y
by CLVECT_1:2
;
then ||.((xseq . n) - (xseq . m)).|| =
||.(0. Y).||
by A20, RLVECT_1:26
.=
0
by CLVECT_1:def 11
;
hence
||.((xseq . n) - (xseq . m)).|| < e
by A18;
:: thesis: verum
end; end;
hence
ex
k being
Element of
NAT st
for
n,
m being
Element of
NAT st
n >= k &
m >= k holds
||.((xseq . n) - (xseq . m)).|| < e
;
:: thesis: verum
end; end;
then
xseq is
CCauchy
by CSSPACE3:10;
hence
xseq is
convergent
by A1, Def14;
:: thesis: verum
end;
take y =
lim xseq;
:: thesis: S1[x,y]
thus
S1[
x,
y]
by A12, A17;
:: thesis: verum
end;
consider f being Function of the carrier of X,the carrier of Y such that
A27:
for x being Element of X holds S1[x,f . x]
from FUNCT_2:sch 3(A11);
reconsider tseq = f as Function of X,Y ;
tseq is LinearOperator of X,Y
proof
A28:
now let x,
y be
VECTOR of
X;
:: thesis: tseq . (x + y) = (tseq . x) + (tseq . y)consider xseq being
sequence of
Y such that A29:
( ( for
n being
Element of
NAT holds
xseq . n = (modetrans (vseq . n),X,Y) . x ) &
xseq is
convergent &
tseq . x = lim xseq )
by A27;
consider yseq being
sequence of
Y such that A30:
( ( for
n being
Element of
NAT holds
yseq . n = (modetrans (vseq . n),X,Y) . y ) &
yseq is
convergent &
tseq . y = lim yseq )
by A27;
consider zseq being
sequence of
Y such that A31:
( ( for
n being
Element of
NAT holds
zseq . n = (modetrans (vseq . n),X,Y) . (x + y) ) &
zseq is
convergent &
tseq . (x + y) = lim zseq )
by A27;
zseq = xseq + yseq
hence
tseq . (x + y) = (tseq . x) + (tseq . y)
by A29, A30, A31, CLVECT_1:121;
:: thesis: verum end;
hence
tseq is
LinearOperator of
X,
Y
by A28, Def3, Def4;
:: thesis: verum
end;
then reconsider tseq = tseq as LinearOperator of X,Y ;
A34:
tseq is bounded
proof
A35:
now let x be
VECTOR of
X;
:: thesis: ||.(tseq . x).|| <= (lim ||.vseq.||) * ||.x.||consider xseq being
sequence of
Y such that A36:
( ( for
n being
Element of
NAT holds
xseq . n = (modetrans (vseq . n),X,Y) . x ) &
xseq is
convergent &
tseq . x = lim xseq )
by A27;
A37:
for
m being
Element of
NAT holds
||.(xseq . m).|| <= ||.(vseq . m).|| * ||.x.||
A39:
||.xseq.|| is
convergent
by A36, Th22;
A40:
||.(tseq . x).|| = lim ||.xseq.||
by A36, Th22;
A41:
for
n being
Element of
NAT holds
||.xseq.|| . n <= (||.x.|| (#) ||.vseq.||) . n
A44:
||.x.|| (#) ||.vseq.|| is
convergent
by A3, SEQ_2:21;
lim (||.x.|| (#) ||.vseq.||) = (lim ||.vseq.||) * ||.x.||
by A3, SEQ_2:22;
hence
||.(tseq . x).|| <= (lim ||.vseq.||) * ||.x.||
by A39, A40, A41, A44, SEQ_2:32;
:: thesis: verum end;
take K =
lim ||.vseq.||;
:: according to CLOPBAN1:def 7 :: thesis: ( 0 <= K & ( for x being VECTOR of X holds ||.(tseq . x).|| <= K * ||.x.|| ) )
K >= 0
hence
(
0 <= K & ( for
x being
VECTOR of
X holds
||.(tseq . x).|| <= K * ||.x.|| ) )
by A35;
:: thesis: verum
end;
A45:
for e being Real st e > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
for x being VECTOR of X holds ||.(((modetrans (vseq . n),X,Y) . x) - (tseq . x)).|| <= e * ||.x.||
proof
let e be
Real;
:: thesis: ( e > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
for x being VECTOR of X holds ||.(((modetrans (vseq . n),X,Y) . x) - (tseq . x)).|| <= e * ||.x.|| )
assume A46:
e > 0
;
:: thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
for x being VECTOR of X holds ||.(((modetrans (vseq . n),X,Y) . x) - (tseq . x)).|| <= e * ||.x.||
consider k being
Element of
NAT such that A47:
for
n,
m being
Element of
NAT st
n >= k &
m >= k holds
||.((vseq . n) - (vseq . m)).|| < e
by A2, A46, CSSPACE3:10;
A48:
now let n be
Element of
NAT ;
:: thesis: ( n >= k implies for x being VECTOR of X holds ||.(((modetrans (vseq . n),X,Y) . x) - (tseq . x)).|| <= e * ||.x.|| )assume A49:
n >= k
;
:: thesis: for x being VECTOR of X holds ||.(((modetrans (vseq . n),X,Y) . x) - (tseq . x)).|| <= e * ||.x.||now let x be
VECTOR of
X;
:: thesis: ||.(((modetrans (vseq . n),X,Y) . x) - (tseq . x)).|| <= e * ||.x.||consider xseq being
sequence of
Y such that A50:
( ( for
n being
Element of
NAT holds
xseq . n = (modetrans (vseq . n),X,Y) . x ) &
xseq is
convergent &
tseq . x = lim xseq )
by A27;
A51:
for
m,
k being
Element of
NAT holds
||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||
proof
let m,
k be
Element of
NAT ;
:: thesis: ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||
vseq . m is
bounded LinearOperator of
X,
Y
by Def8;
then A52:
modetrans (vseq . m),
X,
Y = vseq . m
by Th33;
vseq . k is
bounded LinearOperator of
X,
Y
by Def8;
then A53:
modetrans (vseq . k),
X,
Y = vseq . k
by Th33;
reconsider h1 =
(vseq . m) - (vseq . k) as
bounded LinearOperator of
X,
Y by Def8;
A54:
xseq . m = (modetrans (vseq . m),X,Y) . x
by A50;
xseq . k = (modetrans (vseq . k),X,Y) . x
by A50;
then
(xseq . m) - (xseq . k) = h1 . x
by A52, A53, A54, Th44;
hence
||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||
by Th36;
:: thesis: verum
end; A55:
for
m being
Element of
NAT st
m >= k holds
||.((xseq . n) - (xseq . m)).|| <= e * ||.x.||
||.((xseq . n) - (tseq . x)).|| <= e * ||.x.||
hence
||.(((modetrans (vseq . n),X,Y) . x) - (tseq . x)).|| <= e * ||.x.||
by A50;
:: thesis: verum end; hence
for
x being
VECTOR of
X holds
||.(((modetrans (vseq . n),X,Y) . x) - (tseq . x)).|| <= e * ||.x.||
;
:: thesis: verum end;
take
k
;
:: thesis: for n being Element of NAT st n >= k holds
for x being VECTOR of X holds ||.(((modetrans (vseq . n),X,Y) . x) - (tseq . x)).|| <= e * ||.x.||
thus
for
n being
Element of
NAT st
n >= k holds
for
x being
VECTOR of
X holds
||.(((modetrans (vseq . n),X,Y) . x) - (tseq . x)).|| <= e * ||.x.||
by A48;
:: thesis: verum
end;
reconsider tseq = tseq as bounded LinearOperator of X,Y by A34;
reconsider tv = tseq as Point of (C_NormSpace_of_BoundedLinearOperators X,Y) by Def8;
A65:
for e being Real st e > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e
proof
let e be
Real;
:: thesis: ( e > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e )
assume A66:
e > 0
;
:: thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e
consider k being
Element of
NAT such that A67:
for
n being
Element of
NAT st
n >= k holds
for
x being
VECTOR of
X holds
||.(((modetrans (vseq . n),X,Y) . x) - (tseq . x)).|| <= e * ||.x.||
by A45, A66;
now let n be
Element of
NAT ;
:: thesis: ( n >= k implies ||.((vseq . n) - tv).|| <= e )assume A68:
n >= k
;
:: thesis: ||.((vseq . n) - tv).|| <= eset f1 =
modetrans (vseq . n),
X,
Y;
set g1 =
tseq;
reconsider h1 =
(vseq . n) - tv as
bounded LinearOperator of
X,
Y by Def8;
A69:
now let t be
VECTOR of
X;
:: thesis: ( ||.t.|| <= 1 implies ||.(h1 . t).|| <= e )assume A70:
||.t.|| <= 1
;
:: thesis: ||.(h1 . t).|| <= e
vseq . n is
bounded LinearOperator of
X,
Y
by Def8;
then
modetrans (vseq . n),
X,
Y = vseq . n
by Th33;
then A71:
||.(h1 . t).|| = ||.(((modetrans (vseq . n),X,Y) . t) - (tseq . t)).||
by Th44;
A72:
||.(((modetrans (vseq . n),X,Y) . t) - (tseq . t)).|| <= e * ||.t.||
by A67, A68;
e * ||.t.|| <= e * 1
by A66, A70, XREAL_1:66;
hence
||.(h1 . t).|| <= e
by A71, A72, XXREAL_0:2;
:: thesis: verum end; A76:
( ( for
s being
real number st
s in PreNorms h1 holds
s <= e ) implies
sup (PreNorms h1) <= e )
by SEQ_4:62;
(BoundedLinearOperatorsNorm X,Y) . ((vseq . n) - tv) = sup (PreNorms h1)
by Th34;
hence
||.((vseq . n) - tv).|| <= e
by A73, A76, CLVECT_1:def 10;
:: thesis: verum end;
hence
ex
k being
Element of
NAT st
for
n being
Element of
NAT st
n >= k holds
||.((vseq . n) - tv).|| <= e
;
:: thesis: verum
end;
for e being Real st e > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
hence
vseq is convergent
by CLVECT_1:def 16; :: thesis: verum