let X, Y be RealNormSpace; ( Y is complete implies for seq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st seq is CCauchy holds
seq is convergent )
assume A1:
Y is complete
; for seq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st seq is CCauchy holds
seq is convergent
let vseq be sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ( vseq is CCauchy implies vseq is convergent )
assume A2:
vseq is CCauchy
; 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 );
A3:
for x being Element of X ex y being Element of Y st S1[x,y]
proof
let x be
Element of
X;
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 A4:
for
n being
Element of
NAT holds
xseq . n = H1(
n)
from FUNCT_2:sch 4();
take
lim xseq
;
S1[x, lim xseq]
A5:
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 ;
||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||
reconsider h1 =
(vseq . m) - (vseq . k) as
bounded LinearOperator of
X,
Y by Def10;
A6:
xseq . k = (modetrans ((vseq . k),X,Y)) . x
by A4;
vseq . m is
bounded LinearOperator of
X,
Y
by Def10;
then A7:
modetrans (
(vseq . m),
X,
Y)
= vseq . m
by Th35;
vseq . k is
bounded LinearOperator of
X,
Y
by Def10;
then A8:
modetrans (
(vseq . k),
X,
Y)
= vseq . k
by Th35;
xseq . m = (modetrans ((vseq . m),X,Y)) . x
by A4;
then
(xseq . m) - (xseq . k) = h1 . x
by A7, A8, A6, Th46;
hence
||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||
by Th38;
verum
end;
now let e be
Real;
( 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 A9:
e > 0
;
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < enow per cases
( x = 0. X or x <> 0. X )
;
case A10:
x = 0. X
;
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 ;
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
verumproof
let n,
m be
Element of
NAT ;
( n >= k & m >= k implies ||.((xseq . n) - (xseq . m)).|| < e )
assume that
n >= k
and
m >= k
;
||.((xseq . n) - (xseq . m)).|| < e
A11:
xseq . m =
(modetrans ((vseq . m),X,Y)) . x
by A4
.=
(modetrans ((vseq . m),X,Y)) . (0 * x)
by A10, RLVECT_1:10
.=
0 * ((modetrans ((vseq . m),X,Y)) . x)
by Def6
.=
0. Y
by RLVECT_1:10
;
xseq . n =
(modetrans ((vseq . n),X,Y)) . x
by A4
.=
(modetrans ((vseq . n),X,Y)) . (0 * x)
by A10, RLVECT_1:10
.=
0 * ((modetrans ((vseq . n),X,Y)) . x)
by Def6
.=
0. Y
by RLVECT_1:10
;
then ||.((xseq . n) - (xseq . m)).|| =
||.(0. Y).||
by A11, RLVECT_1:13
.=
0
;
hence
||.((xseq . n) - (xseq . m)).|| < e
by A9;
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
;
verum end;
then
xseq is
CCauchy
by RSSPACE3:8;
then
xseq is
convergent
by A1, Def16;
hence
S1[
x,
lim xseq]
by A4;
verum
end;
consider f being Function of the carrier of X, the carrier of Y such that
A19:
for x being Element of X holds S1[x,f . x]
from FUNCT_2:sch 3(A3);
reconsider tseq = f as Function of X,Y ;
A20:
now let x,
y be
VECTOR of
X;
tseq . (x + y) = (tseq . x) + (tseq . y)consider xseq being
sequence of
Y such that A21:
for
n being
Element of
NAT holds
xseq . n = (modetrans ((vseq . n),X,Y)) . x
and A22:
xseq is
convergent
and A23:
tseq . x = lim xseq
by A19;
consider zseq being
sequence of
Y such that A24:
for
n being
Element of
NAT holds
zseq . n = (modetrans ((vseq . n),X,Y)) . (x + y)
and
zseq is
convergent
and A25:
tseq . (x + y) = lim zseq
by A19;
consider yseq being
sequence of
Y such that A26:
for
n being
Element of
NAT holds
yseq . n = (modetrans ((vseq . n),X,Y)) . y
and A27:
yseq is
convergent
and A28:
tseq . y = lim yseq
by A19;
then
zseq = xseq + yseq
by NORMSP_1:def 2;
hence
tseq . (x + y) = (tseq . x) + (tseq . y)
by A22, A23, A27, A28, A25, NORMSP_1:25;
verum end;
then reconsider tseq = tseq as LinearOperator of X,Y by A20, Def6, GRCAT_1:def 8;
then A39:
||.vseq.|| is convergent
by SEQ_4:41;
A40:
tseq is bounded
proof
take
lim ||.vseq.||
;
LOPBAN_1:def 8 ( 0 <= lim ||.vseq.|| & ( for x being VECTOR of X holds ||.(tseq . x).|| <= (lim ||.vseq.||) * ||.x.|| ) )
A41:
now let x be
VECTOR of
X;
||.(tseq . x).|| <= (lim ||.vseq.||) * ||.x.||consider xseq being
sequence of
Y such that A42:
for
n being
Element of
NAT holds
xseq . n = (modetrans ((vseq . n),X,Y)) . x
and A43:
xseq is
convergent
and A44:
tseq . x = lim xseq
by A19;
A45:
||.(tseq . x).|| = lim ||.xseq.||
by A43, A44, Th24;
A46:
for
m being
Element of
NAT holds
||.(xseq . m).|| <= ||.(vseq . m).|| * ||.x.||
A48:
for
n being
Element of
NAT holds
||.xseq.|| . n <= (||.x.|| (#) ||.vseq.||) . n
A51:
||.x.|| (#) ||.vseq.|| is
convergent
by A39, SEQ_2:7;
A52:
lim (||.x.|| (#) ||.vseq.||) = (lim ||.vseq.||) * ||.x.||
by A39, SEQ_2:8;
||.xseq.|| is
convergent
by A43, A44, Th24;
hence
||.(tseq . x).|| <= (lim ||.vseq.||) * ||.x.||
by A45, A48, A51, A52, SEQ_2:18;
verum end;
hence
(
0 <= lim ||.vseq.|| & ( for
x being
VECTOR of
X holds
||.(tseq . x).|| <= (lim ||.vseq.||) * ||.x.|| ) )
by A39, A41, SEQ_2:17;
verum
end;
A53:
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;
( 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
e > 0
;
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.||
then consider k being
Element of
NAT such that A54:
for
n,
m being
Element of
NAT st
n >= k &
m >= k holds
||.((vseq . n) - (vseq . m)).|| < e
by A2, RSSPACE3:8;
take
k
;
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.||
now let n be
Element of
NAT ;
( n >= k implies for x being VECTOR of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.|| )assume A55:
n >= k
;
for x being VECTOR of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.||now let x be
VECTOR of
X;
||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.||consider xseq being
sequence of
Y such that A56:
for
n being
Element of
NAT holds
xseq . n = (modetrans ((vseq . n),X,Y)) . x
and A57:
xseq is
convergent
and A58:
tseq . x = lim xseq
by A19;
A59:
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 ;
||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||
reconsider h1 =
(vseq . m) - (vseq . k) as
bounded LinearOperator of
X,
Y by Def10;
A60:
xseq . k = (modetrans ((vseq . k),X,Y)) . x
by A56;
vseq . m is
bounded LinearOperator of
X,
Y
by Def10;
then A61:
modetrans (
(vseq . m),
X,
Y)
= vseq . m
by Th35;
vseq . k is
bounded LinearOperator of
X,
Y
by Def10;
then A62:
modetrans (
(vseq . k),
X,
Y)
= vseq . k
by Th35;
xseq . m = (modetrans ((vseq . m),X,Y)) . x
by A56;
then
(xseq . m) - (xseq . k) = h1 . x
by A61, A62, A60, Th46;
hence
||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||
by Th38;
verum
end; A63:
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 A56;
verum end; hence
for
x being
VECTOR of
X holds
||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.||
;
verum end;
hence
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.||
;
verum
end;
reconsider tseq = tseq as bounded LinearOperator of X,Y by A40;
reconsider tv = tseq as Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) by Def10;
A71:
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;
( 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 A72:
e > 0
;
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 A73:
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 A53, A72;
now set g1 =
tseq;
let n be
Element of
NAT ;
( n >= k implies ||.((vseq . n) - tv).|| <= e )assume A74:
n >= k
;
||.((vseq . n) - tv).|| <= ereconsider h1 =
(vseq . n) - tv as
bounded LinearOperator of
X,
Y by Def10;
set f1 =
modetrans (
(vseq . n),
X,
Y);
A75:
now let t be
VECTOR of
X;
( ||.t.|| <= 1 implies ||.(h1 . t).|| <= e )assume
||.t.|| <= 1
;
||.(h1 . t).|| <= ethen A76:
e * ||.t.|| <= e * 1
by A72, XREAL_1:64;
A77:
||.(((modetrans ((vseq . n),X,Y)) . t) - (tseq . t)).|| <= e * ||.t.||
by A73, A74;
vseq . n is
bounded LinearOperator of
X,
Y
by Def10;
then
modetrans (
(vseq . n),
X,
Y)
= vseq . n
by Th35;
then
||.(h1 . t).|| = ||.(((modetrans ((vseq . n),X,Y)) . t) - (tseq . t)).||
by Th46;
hence
||.(h1 . t).|| <= e
by A77, A76, XXREAL_0:2;
verum end; A79:
( ( for
s being
real number 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 Th36;
hence
||.((vseq . n) - tv).|| <= e
by A78, A79;
verum end;
hence
ex
k being
Element of
NAT st
for
n being
Element of
NAT st
n >= k holds
||.((vseq . n) - tv).|| <= e
;
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 NORMSP_1:def 6; verum