let X, Y, Z be RealNormSpace; ( Z is complete implies for seq being sequence of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent )
assume A1:
Z is complete
; for seq being sequence of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent
let vseq be sequence of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)); ( 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 Z st
( ( for n being Nat holds xseq . n = (vseq . n) . $1 ) & xseq is convergent & $2 = lim xseq );
A3:
for xy being Element of [:X,Y:] ex z being Element of Z st S1[xy,z]
proof
let xy be
Element of
[:X,Y:];
ex z being Element of Z st S1[xy,z]
deffunc H1(
Nat)
-> Element of the
carrier of
Z =
(modetrans ((vseq . $1),X,Y,Z)) . xy;
consider xseq being
sequence of
Z 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 = (vseq . n) . xy
take
lim xseq
;
S1[xy, lim xseq]
consider x being
Point of
X,
y being
Point of
Y such that A7:
xy = [x,y]
by PRVECT_3:18;
A8:
for
m,
k being
Nat holds
||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * (||.x.|| * ||.y.||)
proof
let m,
k be
Nat;
||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * (||.x.|| * ||.y.||)
reconsider h1 =
(vseq . m) - (vseq . k) as
Lipschitzian BilinearOperator of
X,
Y,
Z by Def9;
A9:
xseq . m = (vseq . m) . (
x,
y)
by A5, A7;
A10:
xseq . k = (vseq . k) . (
x,
y)
by A5, A7;
(xseq . m) - (xseq . k) = h1 . (
x,
y)
by A9, A10, Th40;
then
||.((xseq . m) - (xseq . k)).|| <= (||.((vseq . m) - (vseq . k)).|| * ||.x.||) * ||.y.||
by Th32;
hence
||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * (||.x.|| * ||.y.||)
;
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 A11:
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 or y = 0. Y ) & ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e ) or ( x <> 0. X & y <> 0. Y & 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 y = 0. Y or ( x <> 0. X & y <> 0. Y ) )
;
case A12:
(
x = 0. X or
y = 0. Y )
;
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < ereconsider k =
0 as
Nat ;
take k =
k;
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
A13:
xseq . m = (vseq . m) . (
x,
y)
by A5, A7;
A14:
(
vseq . m is
Lipschitzian BilinearOperator of
X,
Y,
Z &
vseq . n is
Lipschitzian BilinearOperator of
X,
Y,
Z )
by Def9;
A15:
(
x = 0 * x or
y = 0 * y )
by A12;
then A16:
(vseq . m) . (
x,
y) =
0 * ((vseq . m) . (x,y))
by A14, LOPBAN_8:12
.=
0. Z
by RLVECT_1:10
;
A17:
xseq . n = (vseq . n) . (
x,
y)
by A5, A7;
(vseq . n) . (
x,
y) =
0 * ((vseq . n) . (x,y))
by A14, A15, LOPBAN_8:12
.=
0. Z
by RLVECT_1:10
;
hence
||.((xseq . n) - (xseq . m)).|| < e
by A11, A13, A16, A17;
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
convergent
by A1, RSSPACE3:8;
hence
S1[
xy,
lim xseq]
by A5;
verum
end;
consider f being Function of the carrier of [:X,Y:], the carrier of Z such that
A24:
for z being Element of [:X,Y:] holds S1[z,f . z]
from FUNCT_2:sch 3(A3);
reconsider tseq = f as Function of [:X,Y:],Z ;
A25:
for x1, x2 being Point of X
for y being Point of Y holds tseq . ((x1 + x2),y) = (tseq . (x1,y)) + (tseq . (x2,y))
proof
let x1,
x2 be
Point of
X;
for y being Point of Y holds tseq . ((x1 + x2),y) = (tseq . (x1,y)) + (tseq . (x2,y))let y be
Point of
Y;
tseq . ((x1 + x2),y) = (tseq . (x1,y)) + (tseq . (x2,y))
reconsider x1y =
[x1,y] as
Point of
[:X,Y:] ;
reconsider x2y =
[x2,y] as
Point of
[:X,Y:] ;
reconsider x1x2y =
[(x1 + x2),y] as
Point of
[:X,Y:] ;
consider sqx1y being
sequence of
Z such that A26:
for
n being
Nat holds
(
sqx1y . n = (vseq . n) . x1y &
sqx1y is
convergent &
tseq . x1y = lim sqx1y )
by A24;
consider sqx2y being
sequence of
Z such that A27:
for
n being
Nat holds
(
sqx2y . n = (vseq . n) . x2y &
sqx2y is
convergent &
tseq . x2y = lim sqx2y )
by A24;
consider sqx1x2y being
sequence of
Z such that A28:
for
n being
Nat holds
(
sqx1x2y . n = (vseq . n) . x1x2y &
sqx1x2y is
convergent &
tseq . x1x2y = lim sqx1x2y )
by A24;
for
n being
Nat holds
sqx1x2y . n = (sqx1y . n) + (sqx2y . n)
then A32:
sqx1x2y = sqx1y + sqx2y
by NORMSP_1:def 2;
thus
tseq . (
(x1 + x2),
y)
= (tseq . (x1,y)) + (tseq . (x2,y))
by A26, A27, A28, A32, NORMSP_1:25;
verum
end;
A33:
for x being Point of X
for y being Point of Y
for a being Real holds tseq . ((a * x),y) = a * (tseq . (x,y))
proof
let x be
Point of
X;
for y being Point of Y
for a being Real holds tseq . ((a * x),y) = a * (tseq . (x,y))let y be
Point of
Y;
for a being Real holds tseq . ((a * x),y) = a * (tseq . (x,y))let a be
Real;
tseq . ((a * x),y) = a * (tseq . (x,y))
reconsider xy =
[x,y] as
Point of
[:X,Y:] ;
reconsider axy =
[(a * x),y] as
Point of
[:X,Y:] ;
consider sqxy being
sequence of
Z such that A34:
for
n being
Nat holds
(
sqxy . n = (vseq . n) . xy &
sqxy is
convergent &
tseq . xy = lim sqxy )
by A24;
consider sqaxy being
sequence of
Z such that A35:
for
n being
Nat holds
(
sqaxy . n = (vseq . n) . axy &
sqaxy is
convergent &
tseq . axy = lim sqaxy )
by A24;
for
n being
Nat holds
sqaxy . n = a * (sqxy . n)
then
sqaxy = a * sqxy
by NORMSP_1:def 5;
hence
tseq . (
(a * x),
y)
= a * (tseq . (x,y))
by A34, A35, NORMSP_1:28;
verum
end;
A40:
for x being Point of X
for y1, y2 being Point of Y holds tseq . (x,(y1 + y2)) = (tseq . (x,y1)) + (tseq . (x,y2))
proof
let x be
Point of
X;
for y1, y2 being Point of Y holds tseq . (x,(y1 + y2)) = (tseq . (x,y1)) + (tseq . (x,y2))let y1,
y2 be
Point of
Y;
tseq . (x,(y1 + y2)) = (tseq . (x,y1)) + (tseq . (x,y2))
reconsider x1y =
[x,y1] as
Point of
[:X,Y:] ;
reconsider x2y =
[x,y2] as
Point of
[:X,Y:] ;
reconsider x1x2y =
[x,(y1 + y2)] as
Point of
[:X,Y:] ;
consider sqx1y being
sequence of
Z such that A41:
for
n being
Nat holds
(
sqx1y . n = (vseq . n) . x1y &
sqx1y is
convergent &
tseq . x1y = lim sqx1y )
by A24;
consider sqx2y being
sequence of
Z such that A42:
for
n being
Nat holds
(
sqx2y . n = (vseq . n) . x2y &
sqx2y is
convergent &
tseq . x2y = lim sqx2y )
by A24;
consider sqx1x2y being
sequence of
Z such that A43:
for
n being
Nat holds
(
sqx1x2y . n = (vseq . n) . x1x2y &
sqx1x2y is
convergent &
tseq . x1x2y = lim sqx1x2y )
by A24;
for
n being
Nat holds
sqx1x2y . n = (sqx1y . n) + (sqx2y . n)
then
sqx1x2y = sqx1y + sqx2y
by NORMSP_1:def 2;
hence
tseq . (
x,
(y1 + y2))
= (tseq . (x,y1)) + (tseq . (x,y2))
by A41, A42, A43, NORMSP_1:25;
verum
end;
for x being Point of X
for y being Point of Y
for a being Real holds tseq . (x,(a * y)) = a * (tseq . (x,y))
proof
let x be
Point of
X;
for y being Point of Y
for a being Real holds tseq . (x,(a * y)) = a * (tseq . (x,y))let y be
Point of
Y;
for a being Real holds tseq . (x,(a * y)) = a * (tseq . (x,y))let a be
Real;
tseq . (x,(a * y)) = a * (tseq . (x,y))
reconsider xy =
[x,y] as
Point of
[:X,Y:] ;
reconsider axy =
[x,(a * y)] as
Point of
[:X,Y:] ;
consider sqxy being
sequence of
Z such that A48:
for
n being
Nat holds
(
sqxy . n = (vseq . n) . xy &
sqxy is
convergent &
tseq . xy = lim sqxy )
by A24;
consider sqaxy being
sequence of
Z such that A49:
for
n being
Nat holds
(
sqaxy . n = (vseq . n) . axy &
sqaxy is
convergent &
tseq . axy = lim sqaxy )
by A24;
for
n being
Nat holds
sqaxy . n = a * (sqxy . n)
then
sqaxy = a * sqxy
by NORMSP_1:def 5;
hence
tseq . (
x,
(a * y))
= a * (tseq . (x,y))
by A48, A49, NORMSP_1:28;
verum
end;
then reconsider tseq = tseq as BilinearOperator of X,Y,Z by A25, A33, A40, LOPBAN_8:12;
then A59:
||.vseq.|| is convergent
by SEQ_4:41;
A60:
tseq is Lipschitzian
proof
take
lim ||.vseq.||
;
LOPBAN_9:def 3 ( 0 <= lim ||.vseq.|| & ( for x being VECTOR of X
for y being VECTOR of Y holds ||.(tseq . (x,y)).|| <= ((lim ||.vseq.||) * ||.x.||) * ||.y.|| ) )
A61:
now for x being Point of X
for y being Point of Y holds ||.(tseq . (x,y)).|| <= ((lim ||.vseq.||) * ||.x.||) * ||.y.||let x be
Point of
X;
for y being Point of Y holds ||.(tseq . (x,y)).|| <= ((lim ||.vseq.||) * ||.x.||) * ||.y.||let y be
Point of
Y;
||.(tseq . (x,y)).|| <= ((lim ||.vseq.||) * ||.x.||) * ||.y.||reconsider xy =
[x,y] as
Point of
[:X,Y:] ;
consider xyseq being
sequence of
Z such that A62:
for
n being
Nat holds
xyseq . n = (vseq . n) . xy
and A63:
xyseq is
convergent
and A64:
tseq . xy = lim xyseq
by A24;
A65:
||.(tseq . xy).|| = lim ||.xyseq.||
by A63, A64, LOPBAN_1:20;
A66:
for
m being
Nat holds
||.(xyseq . m).|| <= ||.(vseq . m).|| * (||.x.|| * ||.y.||)
A68:
for
n being
Nat holds
||.xyseq.|| . n <= ((||.x.|| * ||.y.||) (#) ||.vseq.||) . n
A72:
lim ((||.x.|| * ||.y.||) (#) ||.vseq.||) = (lim ||.vseq.||) * (||.x.|| * ||.y.||)
by B53, SEQ_2:8, SEQ_4:41;
||.xyseq.|| is
convergent
by A63, A64, LOPBAN_1:20;
hence
||.(tseq . (x,y)).|| <= ((lim ||.vseq.||) * ||.x.||) * ||.y.||
by A59, A65, A68, A72, SEQ_2:18;
verum end;
hence
(
0 <= lim ||.vseq.|| & ( for
x being
VECTOR of
X for
y being
VECTOR of
Y holds
||.(tseq . (x,y)).|| <= ((lim ||.vseq.||) * ||.x.||) * ||.y.|| ) )
by B53, A61, SEQ_2:17, SEQ_4:41;
verum
end;
A73:
for e being Real st e > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
for x being Point of X
for y being Point of Y holds ||.(((vseq . n) . (x,y)) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.||
proof
let e be
Real;
( e > 0 implies ex k being Nat st
for n being Nat st n >= k holds
for x being Point of X
for y being Point of Y holds ||.(((vseq . n) . (x,y)) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.|| )
assume
e > 0
;
ex k being Nat st
for n being Nat st n >= k holds
for x being Point of X
for y being Point of Y holds ||.(((vseq . n) . (x,y)) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.||
then consider k being
Nat such that A74:
for
n,
m being
Nat st
n >= k &
m >= k holds
||.((vseq . n) - (vseq . m)).|| < e
by A2, RSSPACE3:8;
take
k
;
for n being Nat st n >= k holds
for x being Point of X
for y being Point of Y holds ||.(((vseq . n) . (x,y)) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.||
now for n being Nat st n >= k holds
for x being Point of X
for y being Point of Y holds ||.(((vseq . n) . (x,y)) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.||let n be
Nat;
( n >= k implies for x being Point of X
for y being Point of Y holds ||.(((vseq . n) . (x,y)) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.|| )assume A75:
n >= k
;
for x being Point of X
for y being Point of Y holds ||.(((vseq . n) . (x,y)) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.||now for x being Point of X
for y being Point of Y holds ||.(((vseq . n) . (x,y)) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.||let x be
Point of
X;
for y being Point of Y holds ||.(((vseq . n) . (x,y)) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.||let y be
Point of
Y;
||.(((vseq . n) . (x,y)) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.||reconsider xy =
[x,y] as
Point of
[:X,Y:] ;
consider xyseq being
sequence of
Z such that A76:
for
n being
Nat holds
xyseq . n = (vseq . n) . xy
and A77:
xyseq is
convergent
and A78:
tseq . xy = lim xyseq
by A24;
A79:
for
m,
k being
Nat holds
||.((xyseq . m) - (xyseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * (||.x.|| * ||.y.||)
A81:
for
m being
Nat st
m >= k holds
||.((xyseq . n) - (xyseq . m)).|| <= (e * ||.x.||) * ||.y.||
||.((xyseq . n) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.||
proof
deffunc H1(
Nat)
-> object =
||.((xyseq . $1) - (xyseq . n)).||;
consider rseq being
Real_Sequence such that A84:
for
m being
Nat holds
rseq . m = H1(
m)
from SEQ_1:sch 1();
then A85:
rseq = ||.(xyseq - (xyseq . n)).||
by FUNCT_2:12;
A86:
xyseq - (xyseq . n) is
convergent
by A77, NORMSP_1:21;
lim (xyseq - (xyseq . n)) = (tseq . (x,y)) - (xyseq . n)
by A77, A78, NORMSP_1:27;
then A87:
lim rseq = ||.((tseq . (x,y)) - (xyseq . n)).||
by A85, A86, LOPBAN_1:41;
for
m being
Nat st
m >= k holds
rseq . m <= (e * ||.x.||) * ||.y.||
then
lim rseq <= (e * ||.x.||) * ||.y.||
by A85, A86, LOPBAN_1:41, Lm3;
hence
||.((xyseq . n) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.||
by A87, NORMSP_1:7;
verum
end; hence
||.(((vseq . n) . (x,y)) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.||
by A76;
verum end; hence
for
x being
Point of
X for
y being
Point of
Y holds
||.(((vseq . n) . (x,y)) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.||
;
verum end;
hence
for
n being
Nat st
n >= k holds
for
x being
Point of
X for
y being
Point of
Y holds
||.(((vseq . n) . (x,y)) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.||
;
verum
end;
reconsider tseq = tseq as Lipschitzian BilinearOperator of X,Y,Z by A60;
reconsider tv = tseq as Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) by Def9;
A89:
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 A90:
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 A91:
for
n being
Nat st
n >= k holds
for
x being
Point of
X for
y being
Point of
Y holds
||.(((vseq . n) . (x,y)) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.||
by A73, A90;
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 A92:
n >= k
;
||.((vseq . n) - tv).|| <= ereconsider h1 =
(vseq . n) - tv as
Lipschitzian BilinearOperator of
X,
Y,
Z by Def9;
set f1 =
vseq . n;
A93:
now for t being Point of X
for s being Point of Y st ||.t.|| <= 1 & ||.s.|| <= 1 holds
||.(h1 . (t,s)).|| <= elet t be
Point of
X;
for s being Point of Y st ||.t.|| <= 1 & ||.s.|| <= 1 holds
||.(h1 . (t,s)).|| <= elet s be
Point of
Y;
( ||.t.|| <= 1 & ||.s.|| <= 1 implies ||.(h1 . (t,s)).|| <= e )assume
(
||.t.|| <= 1 &
||.s.|| <= 1 )
;
||.(h1 . (t,s)).|| <= ethen
||.t.|| * ||.s.|| <= 1
* 1
by XREAL_1:66;
then A94:
e * (||.t.|| * ||.s.||) <= e * 1
by A90, XREAL_1:64;
A95:
||.(((vseq . n) . (t,s)) - (tseq . (t,s))).|| <= (e * ||.t.||) * ||.s.||
by A91, A92;
||.(h1 . (t,s)).|| = ||.(((vseq . n) . (t,s)) - (tseq . (t,s))).||
by Th40;
hence
||.(h1 . (t,s)).|| <= e
by A94, A95, XXREAL_0:2;
verum end;
( ( for
s being
Real st
s in PreNorms h1 holds
s <= e ) implies
upper_bound (PreNorms h1) <= e )
by SEQ_4:45;
hence
||.((vseq . n) - tv).|| <= e
by A96, Th30;
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 NORMSP_1:def 6; verum