let vseq be sequence of Complex_l2_Space; CLVECT_2:def 11 ( 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 seqi being Complex_Sequence st
( ( for n being Nat holds seqi . n = (seq_id (vseq . n)) . i ) & seqi is convergent & c2 = lim seqi ) );
A2:
for x being object st x in NAT holds
ex y being object st
( y in COMPLEX & S1[x,y] )
proof
let x be
object ;
( x in NAT implies ex y being object st
( y in COMPLEX & S1[x,y] ) )
assume
x in NAT
;
ex y being object st
( y in COMPLEX & S1[x,y] )
then reconsider i =
x as
Nat ;
deffunc H1(
set )
-> set =
(seq_id (vseq . c1)) . i;
consider seqi being
Complex_Sequence such that A3:
for
n being
Nat holds
seqi . n = H1(
n)
from COMSEQ_1:sch 1();
take
lim seqi
;
( lim seqi in COMPLEX & S1[x, lim seqi] )
thus
lim seqi in COMPLEX
by XCMPLX_0:def 2;
S1[x, lim seqi]
now for e being Real st e > 0 holds
ex k being Nat st
for m being Nat st k <= m holds
|.((seqi . m) - (seqi . k)).| < elet e be
Real;
( e > 0 implies ex k being Nat st
for m being Nat st k <= m holds
|.((seqi . m) - (seqi . k)).| < e )assume A4:
e > 0
;
ex k being Nat st
for m being Nat st k <= m holds
|.((seqi . m) - (seqi . k)).| < ethus
ex
k being
Nat st
for
m being
Nat st
k <= m holds
|.((seqi . m) - (seqi . k)).| < e
verumproof
set e1 =
e;
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, CLVECT_2:58;
A6:
i in NAT
by ORDINAL1:def 12;
now for m being Nat st k <= m holds
|.((seqi . m) - (seqi . k)).| < eset vk =
vseq . k;
let m be
Nat;
( k <= m implies |.((seqi . m) - (seqi . k)).| < e )assume A7:
k <= m
;
|.((seqi . m) - (seqi . k)).| < eset vm =
vseq . m;
||.((vseq . m) - (vseq . k)).|| < e
by A5, A7;
then A8:
sqrt |.(((vseq . m) - (vseq . k)) .|. ((vseq . m) - (vseq . k))).| < e
;
set seqmk =
seq_id ((vseq . m) - (vseq . k));
A9:
sqrt (|.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).|) =
sqrt (|.((seqi . m) - (seqi . k)).| ^2)
.=
|.((seqi . m) - (seqi . k)).|
by COMPLEX1:46, SQUARE_1:22
;
seq_id ((vseq . m) - (vseq . k)) =
seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k)))
by Lm15
.=
(seq_id (vseq . m)) + (- (seq_id (vseq . k)))
;
then (seq_id ((vseq . m) - (vseq . k))) . i =
((seq_id (vseq . m)) . i) + ((- (seq_id (vseq . k))) . i)
by VALUED_1:1, A6
.=
((seq_id (vseq . m)) . i) + (- ((seq_id (vseq . k)) . i))
by VALUED_1:8
.=
((seq_id (vseq . m)) . i) - ((seq_id (vseq . k)) . i)
.=
(seqi . m) - ((seq_id (vseq . k)) . i)
by A3
.=
(seqi . m) - (seqi . k)
by A3
;
then |.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).| =
(|.(seq_id ((vseq . m) - (vseq . k))).| . i) * |.((seq_id ((vseq . m) - (vseq . k))) . i).|
by VALUED_1:18
.=
(|.(seq_id ((vseq . m) - (vseq . k))).| . i) * (|.(seq_id ((vseq . m) - (vseq . k))).| . i)
by VALUED_1:18
;
then
(|.(seq_id ((vseq . m) - (vseq . k))).| . i) * (|.((seq_id ((vseq . m) - (vseq . k))) *').| . i) = |.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).|
by Lm18;
then A10:
|.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).| = (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|) . i
by SEQ_1:8;
0 <= |.((seqi . m) - (seqi . k)).|
by COMPLEX1:46;
then A11:
0 <= |.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).|
;
(
(seq_id ((vseq . m) - (vseq . k))) (#) ((seq_id ((vseq . m) - (vseq . k))) *') is
absolutely_summable & ( for
j being
Nat holds
(
(Re ((seq_id ((vseq . m) - (vseq . k))) (#) ((seq_id ((vseq . m) - (vseq . k))) *'))) . j >= 0 &
(Im ((seq_id ((vseq . m) - (vseq . k))) (#) ((seq_id ((vseq . m) - (vseq . k))) *'))) . j = 0 ) ) )
by Lm8, Lm19;
then |.(Sum ((seq_id ((vseq . m) - (vseq . k))) (#) ((seq_id ((vseq . m) - (vseq . k))) *'))).| =
Sum |.((seq_id ((vseq . m) - (vseq . k))) (#) ((seq_id ((vseq . m) - (vseq . k))) *')).|
by Lm7
.=
Sum (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|)
by COMSEQ_1:46
;
then A12:
sqrt (Sum (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|)) < e
by A8, CSSPACE:def 17;
A13:
for
i being
Nat holds
0 <= (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|) . i
|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.(seq_id ((vseq . m) - (vseq . k))).| is
summable
by CSSPACE:def 11;
then A14:
|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').| is
summable
by Lm18;
then A15:
0 <= Sum (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|)
by A13, 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 < e ^2
by A12, SQUARE_1:16;
then A16:
Sum (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|) < e * e
by A15, 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 A14, A13, RSSPACE2:3;
then A17:
|.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).| < e * e
by A16, A10, XXREAL_0:2;
sqrt (e * e) =
sqrt (e ^2)
.=
e
by A4, SQUARE_1:22
;
hence
|.((seqi . m) - (seqi . k)).| < e
by A11, A17, A9, SQUARE_1:27;
verum end;
hence
ex
k being
Nat st
for
m being
Nat st
k <= m holds
|.((seqi . m) - (seqi . k)).| < e
;
verum
end; end;
then
seqi is
convergent
by COMSEQ_3:46;
hence
S1[
x,
lim seqi]
by A3;
verum
end;
consider f being sequence of COMPLEX such that
A18:
for x being object st x in NAT holds
S1[x,f . x]
from FUNCT_2:sch 1(A2);
reconsider tseq = f as Complex_Sequence ;
set seqt = seq_id tseq;
A20:
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 )
proof
let e1 be
Real;
( e1 > 0 implies 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))) *'))).| < e1 * e1 ) )
assume A21:
e1 > 0
;
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))) *'))).| < e1 * e1 )
set e =
e1 / 2;
A22:
e1 / 2
> 0
by A21;
then consider k being
Nat such that A23:
for
n,
m being
Nat st
n >= k &
m >= k holds
||.((vseq . n) - (vseq . m)).|| < e1 / 2
by A1, CLVECT_2:58;
e1 / 2
< e1
by A21, XREAL_1:216;
then A24:
(e1 / 2) * (e1 / 2) < e1 * e1
by A22, XREAL_1:97;
A25:
for
m,
n being
Nat st
n >= k &
m >= k holds
(
|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).| is
summable &
Sum (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) < (e1 / 2) * (e1 / 2) & ( for
i being
Nat holds
0 <= (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) . i ) )
A30:
for
n,
i being
Nat for
rseq being
Real_Sequence st ( for
m being
Nat holds
rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . i ) holds
(
rseq is
convergent &
lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i )
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))) *'))).| < e1 * e1 )
proof
let n be
Nat;
( n >= k implies ( |.((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))) *'))).| < e1 * e1 ) )
assume A47:
n >= k
;
( |.((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))) *'))).| < e1 * e1 )
A48:
for
i being
Nat st
0 <= i holds
(Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i <= (e1 / 2) * (e1 / 2)
then A54:
Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) is
bounded_above
by SEQ_2:def 3;
A55:
for
i being
Nat holds
0 <= (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) . i
then A56:
|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).| is
summable
by A54, SERIES_1:17;
then
Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) is
convergent
by SERIES_1:def 2;
then
(
Sum (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) = lim (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) &
lim (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) <= (e1 / 2) * (e1 / 2) )
by A48, RSSPACE2:5, SERIES_1:def 3;
then A57:
Sum (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) < e1 * e1
by A24, XXREAL_0:2;
|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.(((seq_id tseq) - (seq_id (vseq . n))) *').| is
summable
by A56, Lm18;
then
|.(((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *')).| is
summable
by COMSEQ_1:46;
then
((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *') is
absolutely_summable
by COMSEQ_3:def 9;
then A58:
|.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *'))).| <= Sum |.(((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *')).|
by Lm6;
|.((seq_id tseq) - (seq_id (vseq . n))).| = |.(((seq_id tseq) - (seq_id (vseq . n))) *').|
by Lm18;
then
Sum |.(((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *')).| < e1 * e1
by A57, COMSEQ_1:46;
hence
(
|.((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))) *'))).| < e1 * e1 )
by A55, A54, A58, SERIES_1:17, XXREAL_0:2;
verum
end;
hence
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))) *'))).| < e1 * e1 )
;
verum
end;
A59:
|.(seq_id tseq).| (#) |.(seq_id tseq).| is summable
tseq in the_set_of_ComplexSequences
by FUNCT_2:8;
then reconsider tv = tseq as Point of Complex_l2_Space by A59, CSSPACE: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 CLVECT_2:9; verum