let X, Y be ComplexNormSpace; ( Y is complete implies for seq being sequence of (C_NormSpace_of_BoundedLinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent )
assume A1:
Y is complete
; for seq being sequence of (C_NormSpace_of_BoundedLinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent
let vseq be sequence of (C_NormSpace_of_BoundedLinearOperators (X,Y)); ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent )
assume A2:
vseq is Cauchy_sequence_by_Norm
; vseq is convergent
defpred S1[ set , set ] means ex xseq being sequence of Y st
( ( for n being 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(
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();
A5:
for
n being
Nat holds
xseq . n = H1(
n)
take
lim xseq
;
S1[x, lim xseq]
A6:
for
m,
k being
Nat holds
||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||
proof
let m,
k be
Nat;
||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||
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
||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||
by Th31;
verum
end;
now for e being Real st e > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < elet e be
Real;
( e > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e )assume A12:
e > 0
;
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < enow ( ( x = 0. X & ex k being Element of NAT st
for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e ) or ( x <> 0. X & ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e ) )per cases
( x = 0. X or x <> 0. X )
;
case A13:
x = 0. X
;
ex k being Element of NAT st
for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < etake k =
0 ;
for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < ethus
for
n,
m being
Nat st
n >= k &
m >= k holds
||.((xseq . n) - (xseq . m)).|| < e
verumproof
let n,
m be
Nat;
( n >= k & m >= k implies ||.((xseq . n) - (xseq . m)).|| < e )
assume that
n >= k
and
m >= k
;
||.((xseq . n) - (xseq . m)).|| < e
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
||.((xseq . n) - (xseq . m)).|| < e
by A12;
verum
end; end; end; end; hence
ex
k being
Nat st
for
n,
m being
Nat st
n >= k &
m >= k holds
||.((xseq . n) - (xseq . m)).|| < e
;
verum end;
then
xseq is
Cauchy_sequence_by_Norm
by CSSPACE3:8;
then
xseq is
convergent
by A1;
hence
S1[
x,
lim xseq]
by A5;
verum
end;
consider f being Function of the carrier of X, the carrier of Y such that
A24:
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 ;
A25:
now for x, y being VECTOR of X holds tseq . (x + y) = (tseq . x) + (tseq . y)let x,
y be
VECTOR of
X;
tseq . (x + y) = (tseq . x) + (tseq . y)consider xseq being
sequence of
Y such that A26:
for
n being
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 being
sequence of
Y such that A29:
for
n being
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 being
sequence of
Y such that A31:
for
n being
Nat holds
yseq . n = (modetrans ((vseq . n),X,Y)) . y
and A32:
yseq is
convergent
and A33:
tseq . y = lim yseq
by A24;
now for n being Nat holds zseq . n = (xseq . n) + (yseq . n)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;
verum end;
then reconsider tseq = tseq as LinearOperator of X,Y by A25, Def3, VECTSP_1:def 20;
then A44:
||.vseq.|| is convergent
by SEQ_4:41;
A45:
tseq is Lipschitzian
proof
take
lim ||.vseq.||
;
CLOPBAN1:def 6 ( 0 <= lim ||.vseq.|| & ( for x being VECTOR of X holds ||.(tseq . x).|| <= (lim ||.vseq.||) * ||.x.|| ) )
A46:
now for x being VECTOR of X holds ||.(tseq . x).|| <= (lim ||.vseq.||) * ||.x.||let x be
VECTOR of
X;
||.(tseq . x).|| <= (lim ||.vseq.||) * ||.x.||consider xseq being
sequence of
Y such that A47:
for
n being
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 being
Nat holds
||.(xseq . m).|| <= ||.(vseq . m).|| * ||.x.||
A53:
for
n being
Nat holds
||.xseq.|| . n <= (||.x.|| (#) ||.vseq.||) . n
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;
verum end;
hence
(
0 <= lim ||.vseq.|| & ( for
x being
VECTOR of
X holds
||.(tseq . x).|| <= (lim ||.vseq.||) * ||.x.|| ) )
by A44, A46, SEQ_2:17;
verum
end;
A58:
for e being Real st e > 0 holds
ex k being Nat st
for n being 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 Nat st
for n being 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 Nat st
for n being 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
Nat such that A59:
for
n,
m being
Nat st
n >= k &
m >= k holds
||.((vseq . n) - (vseq . m)).|| < e
by A2, CSSPACE3:8;
take
k
;
for n being Nat st n >= k holds
for x being VECTOR of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.||
now for n being Nat st n >= k holds
for x being VECTOR of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.||let n be
Nat;
( n >= k implies for x being VECTOR of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.|| )assume A60:
n >= k
;
for x being VECTOR of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.||now for x being VECTOR of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.||let x be
VECTOR of
X;
||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.||consider xseq being
sequence of
Y such that A61:
for
n being
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 being
Nat holds
||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||
proof
let m,
k be
Nat;
||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||
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
||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||
by Th31;
verum
end; A68:
for
m being
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 A61;
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
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 Lipschitzian LinearOperator of X,Y by A45;
reconsider tv = tseq as Point of (C_NormSpace_of_BoundedLinearOperators (X,Y)) by Def7;
A76:
for e being Real st e > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
||.((vseq . n) - tv).|| <= e
proof
let e be
Real;
( e > 0 implies ex k being Nat st
for n being Nat st n >= k holds
||.((vseq . n) - tv).|| <= e )
assume A77:
e > 0
;
ex k being Nat st
for n being Nat st n >= k holds
||.((vseq . n) - tv).|| <= e
consider k being
Nat such that A78:
for
n being
Nat st
n >= k holds
for
x being
VECTOR of
X holds
||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.||
by A58, A77;
now for n being Nat st n >= k holds
||.((vseq . n) - tv).|| <= eset g1 =
tseq;
let n be
Nat;
( n >= k implies ||.((vseq . n) - tv).|| <= e )assume A79:
n >= k
;
||.((vseq . n) - tv).|| <= ereconsider h1 =
(vseq . n) - tv as
Lipschitzian LinearOperator of
X,
Y by Def7;
set f1 =
modetrans (
(vseq . n),
X,
Y);
A80:
now for t being VECTOR of X st ||.t.|| <= 1 holds
||.(h1 . t).|| <= elet t be
VECTOR of
X;
( ||.t.|| <= 1 implies ||.(h1 . t).|| <= e )assume
||.t.|| <= 1
;
||.(h1 . t).|| <= ethen A81:
e * ||.t.|| <= e * 1
by A77, XREAL_1:64;
A82:
||.(((modetrans ((vseq . n),X,Y)) . t) - (tseq . 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).|| = ||.(((modetrans ((vseq . n),X,Y)) . t) - (tseq . t)).||
by Th39;
hence
||.(h1 . t).|| <= e
by A82, A81, XXREAL_0:2;
verum end; A84:
( ( for
s being
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;
verum end;
hence
ex
k being
Nat st
for
n being
Nat st
n >= k holds
||.((vseq . n) - tv).|| <= e
;
verum
end;
for e being Real st e > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e
hence
vseq is convergent
by CLVECT_1:def 15; verum