:: Hilbert Space of Complex Sequences
:: by Noboru Endou
::
:: Received February 24, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

Lm1:  for seq being Complex_Sequence holds Partial_Sums (seq *') = (Partial_Sums seq) *'
proofend;

Lm2:  for a, b being Real holds 0 <= (a ^2) + (b ^2)
proofend;

Lm3:  for z1, z2 being Complex st (Re z1) * (Im z2) = (Re z2) * (Im z1) &amp; ((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) >= 0 holds
|.(z1 + z2).| = |.z1.| + |.z2.|
proofend;

Lm4:  for seq being Complex_Sequence
for n being Element of NAT st ( for i being Element of NAT holds
( (Re seq) . i >= 0 &amp; (Im seq) . i = 0 ) ) holds
|.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n
proofend;

Lm5:  for seq being Complex_Sequence st seq is summable holds
Sum (seq *') = (Sum seq) *'
proofend;

Lm6:  for seq being Complex_Sequence st seq is absolutely_summable holds
|.(Sum seq).| <= Sum |.seq.|
proofend;

Lm7:  for seq being Complex_Sequence st seq is summable &amp; ( for n being Element of NAT holds
( (Re seq) . n >= 0 &amp; (Im seq) . n = 0 ) ) holds
|.(Sum seq).| = Sum |.seq.|
proofend;

Lm8:  for seq being Complex_Sequence
for n being Element of NAT holds
( (Re (seq (#) (seq *'))) . n >= 0 &amp; (Im (seq (#) (seq *'))) . n = 0 )
proofend;

Lm9:  for x being set holds
( x is Element of Complex_l2_Space iff ( x is Complex_Sequence &amp; |.(seq_id x).| (#) |.(seq_id x).| is summable ) )
proofend;

Lm10:  0. Complex_l2_Space = CZeroseq
proofend;

Lm11:  for u being VECTOR of Complex_l2_Space holds u = seq_id u
proofend;

Lm12:  for u, v being VECTOR of Complex_l2_Space holds u + v = (seq_id u) + (seq_id v)
proofend;

Lm13:  for r being Complex
for u being VECTOR of Complex_l2_Space holds r * u = r (#) (seq_id u)
proofend;

Lm14:  for u being VECTOR of Complex_l2_Space holds
( - u = - (seq_id u) &amp; seq_id (- u) = - (seq_id u) )
proofend;

Lm15:  for u, v being VECTOR of Complex_l2_Space holds u - v = (seq_id u) - (seq_id v)
proofend;

Lm16:  for v, w being VECTOR of Complex_l2_Space holds |.(seq_id v).| (#) |.(seq_id w).| is summable
proofend;

Lm17:  for v, w being VECTOR of Complex_l2_Space holds v .|. w = Sum ((seq_id v) (#) ((seq_id w) *'))
proofend;

Lm18:  for seq being Complex_Sequence holds |.seq.| = |.(seq *').|
proofend;

Lm19:  for x being set holds
( x is Element of Complex_l2_Space iff ( x is Complex_Sequence &amp; (seq_id x) (#) ((seq_id x) *') is absolutely_summable ) )
proofend;

theorem :: CSSPACE2:1
( the carrier of Complex_l2_Space = the_set_of_l2ComplexSequences &amp; ( for x being set holds
( x is Element of Complex_l2_Space iff ( x is Complex_Sequence &amp; |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) ) &amp; ( for x being set holds
( x is Element of Complex_l2_Space iff ( x is Complex_Sequence &amp; (seq_id x) (#) ((seq_id x) *') is absolutely_summable ) ) ) &amp; 0. Complex_l2_Space = CZeroseq &amp; ( for u being VECTOR of Complex_l2_Space holds u = seq_id u ) &amp; ( for u, v being VECTOR of Complex_l2_Space holds u + v = (seq_id u) + (seq_id v) ) &amp; ( for r being Complex
for u being VECTOR of Complex_l2_Space holds r * u = r (#) (seq_id u) ) &amp; ( for u being VECTOR of Complex_l2_Space holds
( - u = - (seq_id u) &amp; seq_id (- u) = - (seq_id u) ) ) &amp; ( for u, v being VECTOR of Complex_l2_Space holds u - v = (seq_id u) - (seq_id v) ) &amp; ( for v, w being VECTOR of Complex_l2_Space holds
( |.(seq_id v).| (#) |.(seq_id w).| is summable &amp; ( for v, w being VECTOR of Complex_l2_Space holds v .|. w = Sum ((seq_id v) (#) ((seq_id w) *')) ) ) ) ) by Lm9, Lm10, Lm11, Lm12, Lm13, Lm14, Lm15, Lm16, Lm17, Lm19, CSSPACE:def_18;

theorem Th2: :: CSSPACE2:2
for x, y, z being Point of Complex_l2_Space
for a being Complex holds
( ( x .|. x = 0 implies x = 0. Complex_l2_Space ) &amp; ( x = 0. Complex_l2_Space implies x .|. x = 0 ) &amp; Re (x .|. x) >= 0 &amp; Im (x .|. x) = 0 &amp; x .|. y = (y .|. x) *' &amp; (x + y) .|. z = (x .|. z) + (y .|. z) &amp; (a * x) .|. y = a * (x .|. y) )
proofend;

registration
cluster Complex_l2_Space  ->  ComplexUnitarySpace-like ;
coherence
 Complex_l2_Space is ComplexUnitarySpace-like by Th2, CSSPACE:def_13;
end;

Lm20:  for x, y being Complex holds 2 * |.(x * y).| <= (|.x.| ^2) + (|.y.| ^2)
proofend;

Lm21:  for x, y being Complex holds
( |.(x + y).| * |.(x + y).| <= ((2 * |.x.|) * |.x.|) + ((2 * |.y.|) * |.y.|) &amp; |.x.| * |.x.| <= ((2 * |.(x - y).|) * |.(x - y).|) + ((2 * |.y.|) * |.y.|) )
proofend;

Lm22:  for c being Complex
for seq being Complex_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = |.((seq . m) - c).| * |.((seq . m) - c).| ) holds
( rseq is convergent &amp; lim rseq = |.((lim seq) - c).| * |.((lim seq) - c).| )
proofend;

Lm23:  for c being Complex
for seq1 being Real_Sequence
for seq being Complex_Sequence st seq is convergent &amp; seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = (|.((seq . i) - c).| * |.((seq . i) - c).|) + (seq1 . i) ) holds
( rseq is convergent &amp; lim rseq = (|.((lim seq) - c).| * |.((lim seq) - c).|) + (lim seq1) )
proofend;

registration
cluster Complex_l2_Space  ->  complete ;
coherence
 Complex_l2_Space is complete
proofend;
end;

registration
clusterV80() right_complementable V131() V132() V133() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexUnitarySpace-like complete for CUNITSTR ;
existence
 ex b1 being ComplexUnitarySpace st b1 is complete
proofend;
end;

definition
mode ComplexHilbertSpace is complete ComplexUnitarySpace;
end;

begin

theorem :: CSSPACE2:3
for z1, z2 being Complex st (Re z1) * (Im z2) = (Re z2) * (Im z1) &amp; ((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) >= 0 holds
|.(z1 + z2).| = |.z1.| + |.z2.| by Lm3;

theorem :: CSSPACE2:4
for x, y being Complex holds 2 * |.(x * y).| <= (|.x.| ^2) + (|.y.| ^2) by Lm20;

theorem :: CSSPACE2:5
for x, y being Complex holds
( |.(x + y).| * |.(x + y).| <= ((2 * |.x.|) * |.x.|) + ((2 * |.y.|) * |.y.|) &amp; |.x.| * |.x.| <= ((2 * |.(x - y).|) * |.(x - y).|) + ((2 * |.y.|) * |.y.|) ) by Lm21;

theorem :: CSSPACE2:6
canceled;

theorem :: CSSPACE2:7
for seq being Complex_Sequence holds Partial_Sums (seq *') = (Partial_Sums seq) *' by Lm1;

theorem :: CSSPACE2:8
for seq being Complex_Sequence
for n being Element of NAT st ( for i being Element of NAT holds
( (Re seq) . i >= 0 &amp; (Im seq) . i = 0 ) ) holds
|.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n by Lm4;

theorem :: CSSPACE2:9
for seq being Complex_Sequence st seq is summable holds
Sum (seq *') = (Sum seq) *' by Lm5;

theorem :: CSSPACE2:10
for seq being Complex_Sequence st seq is absolutely_summable holds
|.(Sum seq).| <= Sum |.seq.| by Lm6;

theorem :: CSSPACE2:11
for seq being Complex_Sequence st seq is summable &amp; ( for n being Element of NAT holds
( (Re seq) . n >= 0 &amp; (Im seq) . n = 0 ) ) holds
|.(Sum seq).| = Sum |.seq.| by Lm7;

theorem :: CSSPACE2:12
for seq being Complex_Sequence
for n being Element of NAT holds
( (Re (seq (#) (seq *'))) . n >= 0 &amp; (Im (seq (#) (seq *'))) . n = 0 ) by Lm8;

theorem :: CSSPACE2:13
for seq being Complex_Sequence st seq is absolutely_summable &amp; Sum |.seq.| = 0 holds
for n being Element of NAT holds seq . n = 0c
proofend;

theorem :: CSSPACE2:14
for seq being Complex_Sequence holds |.seq.| = |.(seq *').| by Lm18;

theorem :: CSSPACE2:15
for c being Complex
for seq being Complex_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = |.((seq . m) - c).| * |.((seq . m) - c).| ) holds
( rseq is convergent &amp; lim rseq = |.((lim seq) - c).| * |.((lim seq) - c).| ) by Lm22;

theorem :: CSSPACE2:16
for c being Complex
for seq1 being Real_Sequence
for seq being Complex_Sequence st seq is convergent &amp; seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = (|.((seq . i) - c).| * |.((seq . i) - c).|) + (seq1 . i) ) holds
( rseq is convergent &amp; lim rseq = (|.((lim seq) - c).| * |.((lim seq) - c).|) + (lim seq1) ) by Lm23;

theorem :: CSSPACE2:17
for c being Complex
for seq being Complex_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = |.((seq . m) - c).| * |.((seq . m) - c).| ) holds
( rseq is convergent &amp; lim rseq = |.((lim seq) - c).| * |.((lim seq) - c).| ) by Lm22;

theorem :: CSSPACE2:18
for c being Complex
for seq1 being Real_Sequence
for seq being Complex_Sequence st seq is convergent &amp; seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = (|.((seq . i) - c).| * |.((seq . i) - c).|) + (seq1 . i) ) holds
( rseq is convergent &amp; lim rseq = (|.((lim seq) - c).| * |.((lim seq) - c).|) + (lim seq1) ) by Lm23;