let vseq be sequence of l2_Space; BHSP_3:def 4 ( not vseq is Cauchy or vseq is convergent )
assume A1:
vseq is Cauchy
; vseq is convergent
defpred S1[ object , object ] means ex i being Nat st
( c1 = i & ex rseqi being Real_Sequence st
( ( for n being Nat holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & c2 = lim rseqi ) );
A2:
for x being object st x in NAT holds
ex y being object st
( y in REAL & S1[x,y] )
proof
let x be
object ;
( x in NAT implies ex y being object st
( y in REAL & S1[x,y] ) )
assume
x in NAT
;
ex y being object st
( y in REAL & S1[x,y] )
then reconsider i =
x as
Element of
NAT ;
deffunc H1(
set )
-> Element of
REAL =
(seq_id (vseq . c1)) . i;
consider rseqi being
Real_Sequence such that A3:
for
n being
Nat holds
rseqi . n = H1(
n)
from SEQ_1:sch 1();
reconsider lr =
lim rseqi as
Element of
REAL by XREAL_0:def 1;
take
lr
;
( lr in REAL & S1[x,lr] )
now for e being Real st e > 0 holds
ex k being Nat st
for m being Nat st k <= m holds
|.((rseqi . m) - (rseqi . k)).| < elet e be
Real;
( e > 0 implies ex k being Nat st
for m being Nat st k <= m holds
|.((rseqi . m) - (rseqi . k)).| < e )assume A4:
e > 0
;
ex k being Nat st
for m being Nat st k <= m holds
|.((rseqi . m) - (rseqi . k)).| < ethus
ex
k being
Nat st
for
m being
Nat st
k <= m holds
|.((rseqi . m) - (rseqi . k)).| < e
verumproof
consider k being
Nat such that A5:
for
n,
m being
Nat st
n >= k &
m >= k holds
||.((vseq . n) - (vseq . m)).|| < e
by A1, A4, BHSP_3:2;
now for m being Nat st k <= m holds
|.((rseqi . m) - (rseqi . k)).| < elet m be
Nat;
( k <= m implies |.((rseqi . m) - (rseqi . k)).| < e )assume
k <= m
;
|.((rseqi . m) - (rseqi . k)).| < ethen
||.((vseq . m) - (vseq . k)).|| < e
by A5;
then
sqrt (((vseq . m) - (vseq . k)) .|. ((vseq . m) - (vseq . k))) < e
by BHSP_1:def 4;
then A6:
sqrt (Sum ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k))))) < e
by Th1;
reconsider e1 =
e as
Real ;
A7:
sqrt (|.((rseqi . m) - (rseqi . k)).| * |.((rseqi . m) - (rseqi . k)).|) =
sqrt (|.((rseqi . m) - (rseqi . k)).| ^2)
.=
|.((rseqi . m) - (rseqi . k)).|
by COMPLEX1:46, SQUARE_1:22
;
seq_id ((vseq . m) - (vseq . k)) =
(seq_id (vseq . m)) - (seq_id (vseq . k))
by Th1
.=
(seq_id (vseq . m)) + (- (seq_id (vseq . k)))
by SEQ_1:11
;
then (seq_id ((vseq . m) - (vseq . k))) . i =
((seq_id (vseq . m)) . i) + ((- (seq_id (vseq . k))) . i)
by SEQ_1:7
.=
((seq_id (vseq . m)) . i) + (- ((seq_id (vseq . k)) . i))
by SEQ_1:10
.=
((seq_id (vseq . m)) . i) - ((seq_id (vseq . k)) . i)
.=
(rseqi . m) - ((seq_id (vseq . k)) . i)
by A3
.=
(rseqi . m) - (rseqi . k)
by A3
;
then ((seq_id ((vseq . m) - (vseq . k))) . i) * ((seq_id ((vseq . m) - (vseq . k))) . i) =
((rseqi . m) - (rseqi . k)) ^2
.=
|.((rseqi . m) - (rseqi . k)).| ^2
by COMPLEX1:75
.=
|.((rseqi . m) - (rseqi . k)).| * |.((rseqi . m) - (rseqi . k)).|
;
then A8:
|.((rseqi . m) - (rseqi . k)).| * |.((rseqi . m) - (rseqi . k)).| = ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))) . i
by SEQ_1:8;
A9:
for
i being
Nat holds
0 <= ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))) . i
A10:
(seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k))) is
summable
by RSSPACE:def 11;
then A11:
0 <= Sum ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k))))
by A9, SERIES_1:18;
then
0 <= sqrt (Sum ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))))
by SQUARE_1:def 2;
then
(sqrt (Sum ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))))) ^2 < e1 ^2
by A6, SQUARE_1:16;
then A12:
Sum ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))) < e * e
by A11, SQUARE_1:def 2;
((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))) . i <= Sum ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k))))
by A10, A9, Lm1;
then A13:
(
0 <= |.((rseqi . m) - (rseqi . k)).| &
|.((rseqi . m) - (rseqi . k)).| * |.((rseqi . m) - (rseqi . k)).| < e * e )
by A12, A8, COMPLEX1:46, XXREAL_0:2;
sqrt (e * e) =
sqrt (e1 ^2)
.=
e
by A4, SQUARE_1:22
;
hence
|.((rseqi . m) - (rseqi . k)).| < e
by A13, A7, SQUARE_1:27;
verum end;
hence
ex
k being
Nat st
for
m being
Nat st
k <= m holds
|.((rseqi . m) - (rseqi . k)).| < e
;
verum
end; end;
then
rseqi is
convergent
by SEQ_4:41;
hence
(
lr in REAL &
S1[
x,
lr] )
by A3;
verum
end;
consider f being sequence of REAL such that
A14:
for x being object st x in NAT holds
S1[x,f . x]
from FUNCT_2:sch 1(A2);
reconsider tseq = f as Real_Sequence ;
A16:
for e being Real st e > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
( ((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))) is summable & Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) < e * e )
A51:
(seq_id tseq) (#) (seq_id tseq) is summable
tseq in the_set_of_RealSequences
by FUNCT_2:8;
then reconsider tv = tseq as Point of l2_Space by A51, RSSPACE:def 11;
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 BHSP_2:9; verum