:: CSSPACE2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for seq being Complex_Sequence holds seq = (seq *' ) *'
proof end;

Lm2: for seq being Complex_Sequence holds Partial_Sums (seq *' ) = (Partial_Sums seq) *'
proof end;

Lm3: for a, b being Real holds 0 <= (a ^2 ) + (b ^2 )
proof end;

Lm4: for z1, z2 being Complex st (Re z1) * (Im z2) = (Re z2) * (Im z1) & ((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) >= 0 holds
|.(z1 + z2).| = |.z1.| + |.z2.|
proof end;

Lm5: for seq being Complex_Sequence
for n being Nat st ( for i being Nat holds
( (Re seq) . i >= 0 & (Im seq) . i = 0 ) ) holds
|.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n
proof end;

Lm6: for seq being Complex_Sequence st seq is summable holds
Sum (seq *' ) = (Sum seq) *'
proof end;

Lm7: for seq being Complex_Sequence st seq is absolutely_summable holds
|.(Sum seq).| <= Sum |.seq.|
proof end;

Lm8: for seq being Complex_Sequence st seq is summable & ( for n being Nat holds
( (Re seq) . n >= 0 & (Im seq) . n = 0 ) ) holds
|.(Sum seq).| = Sum |.seq.|
proof end;

Lm9: for seq being Complex_Sequence
for n being Nat holds
( (Re (seq (#) (seq *' ))) . n >= 0 & (Im (seq (#) (seq *' ))) . n = 0 )
proof end;

Lm10: for x being set holds
( x is Element of Complex_l2_Space iff ( x is Complex_Sequence & |.(seq_id x).| (#) |.(seq_id x).| is summable ) )
proof end;

Lm11: 0. Complex_l2_Space = CZeroseq
proof end;

Lm12: for u being VECTOR of Complex_l2_Space holds u = seq_id u
proof end;

Lm13: for u, v being VECTOR of Complex_l2_Space holds u + v = (seq_id u) + (seq_id v)
proof end;

Lm14: for r being Complex
for u being VECTOR of Complex_l2_Space holds r * u = r (#) (seq_id u)
proof end;

Lm15: for u being VECTOR of Complex_l2_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )
proof end;

Lm16: for u, v being VECTOR of Complex_l2_Space holds u - v = (seq_id u) - (seq_id v)
proof end;

Lm17: for v, w being VECTOR of Complex_l2_Space holds |.(seq_id v).| (#) |.(seq_id w).| is summable
proof end;

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

Lm19: for seq being Complex_Sequence holds |.seq.| = |.(seq *' ).|
proof end;

Lm20: for x being set holds
( x is Element of Complex_l2_Space iff ( x is Complex_Sequence & (seq_id x) (#) ((seq_id x) *' ) is absolutely_summable ) )
proof end;

theorem :: CSSPACE2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( the carrier of Complex_l2_Space = the_set_of_l2ComplexSequences & ( for x being set holds
( x is Element of Complex_l2_Space iff ( x is Complex_Sequence & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) ) & ( for x being set holds
( x is Element of Complex_l2_Space iff ( x is Complex_Sequence & (seq_id x) (#) ((seq_id x) *' ) is absolutely_summable ) ) ) & 0. Complex_l2_Space = CZeroseq & ( for u being VECTOR of Complex_l2_Space holds u = seq_id u ) & ( for u, v being VECTOR of Complex_l2_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for r being Complex
for u being VECTOR of Complex_l2_Space holds r * u = r (#) (seq_id u) ) & ( for u being VECTOR of Complex_l2_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of Complex_l2_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v, w being VECTOR of Complex_l2_Space holds
( |.(seq_id v).| (#) |.(seq_id w).| is summable & ( for v, w being VECTOR of Complex_l2_Space holds v .|. w = Sum ((seq_id v) (#) ((seq_id w) *' )) ) ) ) ) by Lm10, Lm11, Lm12, Lm13, Lm14, Lm15, Lm16, Lm17, Lm18, Lm20, CSSPACE:def 20;

theorem Th2: :: CSSPACE2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being Point of Complex_l2_Space
for a being Complex holds
( ( x .|. x = 0 implies x = 0. Complex_l2_Space ) & ( x = 0. Complex_l2_Space implies x .|. x = 0 ) & Re (x .|. x) >= 0 & Im (x .|. x) = 0 & x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
proof end;

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

Lm21: for x, y being Complex holds 2 * |.(x * y).| <= (|.x.| ^2 ) + (|.y.| ^2 )
proof end;

Lm22: for x, y being Complex holds
( |.(x + y).| * |.(x + y).| <= ((2 * |.x.|) * |.x.|) + ((2 * |.y.|) * |.y.|) & |.x.| * |.x.| <= ((2 * |.(x - y).|) * |.(x - y).|) + ((2 * |.y.|) * |.y.|) )
proof end;

Lm23: for c being Complex
for seq being Complex_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for m being Nat holds rseq . m = |.((seq . m) - c).| * |.((seq . m) - c).| ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| * |.((lim seq) - c).| )
proof end;

Lm24: for c being Complex
for seq1 being Real_Sequence
for seq being Complex_Sequence st seq is convergent & seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Nat holds rseq . i = (|.((seq . i) - c).| * |.((seq . i) - c).|) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (|.((lim seq) - c).| * |.((lim seq) - c).|) + (lim seq1) )
proof end;

theorem :: CSSPACE2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for vseq being sequence of Complex_l2_Space st vseq is Cauchy holds
vseq is convergent
proof end;

then Lm25: Complex_l2_Space is complete
by CLVECT_2:def 12;

registration
cluster Complex_l2_Space -> ComplexUnitarySpace-like Hilbert ;
coherence
Complex_l2_Space is Hilbert by Lm25, CLVECT_2:def 13;
end;

theorem :: CSSPACE2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being Complex st (Re z1) * (Im z2) = (Re z2) * (Im z1) & ((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) >= 0 holds
|.(z1 + z2).| = |.z1.| + |.z2.| by Lm4;

theorem :: CSSPACE2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Complex holds 2 * |.(x * y).| <= (|.x.| ^2 ) + (|.y.| ^2 ) by Lm21;

theorem :: CSSPACE2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Complex holds
( |.(x + y).| * |.(x + y).| <= ((2 * |.x.|) * |.x.|) + ((2 * |.y.|) * |.y.|) & |.x.| * |.x.| <= ((2 * |.(x - y).|) * |.(x - y).|) + ((2 * |.y.|) * |.y.|) ) by Lm22;

theorem :: CSSPACE2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for seq being Complex_Sequence holds seq = (seq *' ) *' by Lm1;

theorem :: CSSPACE2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for seq being Complex_Sequence holds Partial_Sums (seq *' ) = (Partial_Sums seq) *' by Lm2;

theorem :: CSSPACE2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for seq being Complex_Sequence
for n being Nat st ( for i being Nat holds
( (Re seq) . i >= 0 & (Im seq) . i = 0 ) ) holds
|.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n by Lm5;

theorem :: CSSPACE2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for seq being Complex_Sequence st seq is summable holds
Sum (seq *' ) = (Sum seq) *' by Lm6;

theorem :: CSSPACE2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for seq being Complex_Sequence st seq is absolutely_summable holds
|.(Sum seq).| <= Sum |.seq.| by Lm7;

theorem :: CSSPACE2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for seq being Complex_Sequence st seq is summable & ( for n being Nat holds
( (Re seq) . n >= 0 & (Im seq) . n = 0 ) ) holds
|.(Sum seq).| = Sum |.seq.| by Lm8;

theorem :: CSSPACE2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for seq being Complex_Sequence
for n being Nat holds
( (Re (seq (#) (seq *' ))) . n >= 0 & (Im (seq (#) (seq *' ))) . n = 0 ) by Lm9;

theorem :: CSSPACE2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for seq being Complex_Sequence st seq is absolutely_summable & Sum |.seq.| = 0 holds
for n being Nat holds seq . n = 0c
proof end;

theorem :: CSSPACE2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for seq being Complex_Sequence holds |.seq.| = |.(seq *' ).| by Lm19;

theorem :: CSSPACE2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for c being Complex
for seq being Complex_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for m being Nat holds rseq . m = |.((seq . m) - c).| * |.((seq . m) - c).| ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| * |.((lim seq) - c).| ) by Lm23;

theorem :: CSSPACE2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for c being Complex
for seq1 being Real_Sequence
for seq being Complex_Sequence st seq is convergent & seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Nat holds rseq . i = (|.((seq . i) - c).| * |.((seq . i) - c).|) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (|.((lim seq) - c).| * |.((lim seq) - c).|) + (lim seq1) ) by Lm24;

theorem :: CSSPACE2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for c being Complex
for seq being Complex_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for m being Nat holds rseq . m = |.((seq . m) - c).| * |.((seq . m) - c).| ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| * |.((lim seq) - c).| ) by Lm23;

theorem :: CSSPACE2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for c being Complex
for seq1 being Real_Sequence
for seq being Complex_Sequence st seq is convergent & seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Nat holds rseq . i = (|.((seq . i) - c).| * |.((seq . i) - c).|) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (|.((lim seq) - c).| * |.((lim seq) - c).|) + (lim seq1) ) by Lm24;