:: CSSPACE2 semantic presentation

Lemma1: for b₁ being Complex_Sequence holds b₁ = (b₁ *' ) *'

proof end;

Lemma2: for b₁ being Complex_Sequence holds Partial_Sums (b₁ *' ) = (Partial_Sums b₁) *'

proof end;

Lemma3: for b₁, b₂ being Real holds 0 <= (b₁ ^2 ) + (b₂ ^2 )

proof end;

Lemma4: for b₁, b₂ being Complex st (Re b₁) * (Im b₂) = (Re b₂) * (Im b₁) & ((Re b₁) * (Re b₂)) + ((Im b₁) * (Im b₂)) >= 0 holds
|.(b₁ + b₂).| = |.b₁.| + |.b₂.|

proof end;

Lemma5: for b₁ being Complex_Sequence
for b₂ being Nat st ( for b₃ being Nat holds
( (Re b₁) . b₃ >= 0 & (Im b₁) . b₃ = 0 ) ) holds
|.(Partial_Sums b₁).| . b₂ = (Partial_Sums |.b₁.|) . b₂

proof end;

Lemma6: for b₁ being Complex_Sequence st b₁ is summable holds
Sum (b₁ *' ) = (Sum b₁) *'

proof end;

Lemma7: for b₁ being Complex_Sequence st b₁ is absolutely_summable holds
|.(Sum b₁).| <= Sum |.b₁.|

proof end;

Lemma8: for b₁ being Complex_Sequence st b₁ is summable & ( for b₂ being Nat holds
( (Re b₁) . b₂ >= 0 & (Im b₁) . b₂ = 0 ) ) holds
|.(Sum b₁).| = Sum |.b₁.|

proof end;

Lemma9: for b₁ being Complex_Sequence
for b₂ being Nat holds
( (Re (b₁ (#) (b₁ *' ))) . b₂ >= 0 & (Im (b₁ (#) (b₁ *' ))) . b₂ = 0 )

proof end;

Lemma10: for b₁ being set holds
( b₁ is Element of Complex_l2_Space iff ( b₁ is Complex_Sequence & |.(seq_id b₁).| (#) |.(seq_id b₁).| is summable ) )

proof end;

Lemma11: 0. Complex_l2_Space = CZeroseq

proof end;

Lemma12: for b₁ being VECTOR of Complex_l2_Space holds b₁ = seq_id b₁

proof end;

Lemma13: for b₁, b₂ being VECTOR of Complex_l2_Space holds b₁ + b₂ = (seq_id b₁) + (seq_id b₂)

proof end;

Lemma14: for b₁ being Complex
for b₂ being VECTOR of Complex_l2_Space holds b₁ * b₂ = b₁ (#) (seq_id b₂)

proof end;

Lemma15: for b₁ being VECTOR of Complex_l2_Space holds
( - b₁ = - (seq_id b₁) & seq_id (- b₁) = - (seq_id b₁) )

proof end;

Lemma16: for b₁, b₂ being VECTOR of Complex_l2_Space holds b₁ - b₂ = (seq_id b₁) - (seq_id b₂)

proof end;

Lemma17: for b₁, b₂ being VECTOR of Complex_l2_Space holds |.(seq_id b₁).| (#) |.(seq_id b₂).| is summable

proof end;

Lemma18: for b₁, b₂ being VECTOR of Complex_l2_Space holds b₁ .|. b₂ = Sum ((seq_id b₁) (#) ((seq_id b₂) *' ))

proof end;

Lemma19: for b₁ being Complex_Sequence holds |.b₁.| = |.(b₁ *' ).|

proof end;

Lemma20: for b₁ being set holds
( b₁ is Element of Complex_l2_Space iff ( b₁ is Complex_Sequence & (seq_id b₁) (#) ((seq_id b₁) *' ) is absolutely_summable ) )

proof end;

theorem Th1: :: CSSPACE2:1

( the carrier of Complex_l2_Space = the_set_of_l2ComplexSequences & ( for b₁ being set holds
( b₁ is Element of Complex_l2_Space iff ( b₁ is Complex_Sequence & |.(seq_id b₁).| (#) |.(seq_id b₁).| is summable ) ) ) & ( for b₁ being set holds
( b₁ is Element of Complex_l2_Space iff ( b₁ is Complex_Sequence & (seq_id b₁) (#) ((seq_id b₁) *' ) is absolutely_summable ) ) ) & 0. Complex_l2_Space = CZeroseq & ( for b₁ being VECTOR of Complex_l2_Space holds b₁ = seq_id b₁ ) & ( for b₁, b₂ being VECTOR of Complex_l2_Space holds b₁ + b₂ = (seq_id b₁) + (seq_id b₂) ) & ( for b₁ being Complex
for b₂ being VECTOR of Complex_l2_Space holds b₁ * b₂ = b₁ (#) (seq_id b₂) ) & ( for b₁ being VECTOR of Complex_l2_Space holds
( - b₁ = - (seq_id b₁) & seq_id (- b₁) = - (seq_id b₁) ) ) & ( for b₁, b₂ being VECTOR of Complex_l2_Space holds b₁ - b₂ = (seq_id b₁) - (seq_id b₂) ) & ( for b₁, b₂ being VECTOR of Complex_l2_Space holds
( |.(seq_id b₁).| (#) |.(seq_id b₂).| is summable & ( for b₃, b₄ being VECTOR of Complex_l2_Space holds b₃ .|. b₄ = Sum ((seq_id b₃) (#) ((seq_id b₄) *' )) ) ) ) ) by Lemma10, Lemma11, Lemma12, Lemma13, Lemma14, Lemma15, Lemma16, Lemma17, Lemma18, Lemma20, CSSPACE:def 20;

theorem Th2: :: CSSPACE2:2

for b₁, b₂, b₃ being Point of Complex_l2_Space
for b₄ being Complex holds
( ( b₁ .|. b₁ = 0 implies b₁ = 0. Complex_l2_Space ) & ( b₁ = 0. Complex_l2_Space implies b₁ .|. b₁ = 0 ) & Re (b₁ .|. b₁) >= 0 & Im (b₁ .|. b₁) = 0 & b₁ .|. b₂ = (b₂ .|. b₁) *' & (b₁ + b₂) .|. b₃ = (b₁ .|. b₃) + (b₂ .|. b₃) & (b₄ * b₁) .|. b₂ = b₄ * (b₁ .|. b₂) )

proof end;

registration

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

end;

Lemma22: for b₁, b₂ being Complex holds 2 * |.(b₁ * b₂).| <= (|.b₁.| ^2 ) + (|.b₂.| ^2 )

proof end;

Lemma23: for b₁, b₂ being Complex holds
( |.(b₁ + b₂).| * |.(b₁ + b₂).| <= ((2 * |.b₁.|) * |.b₁.|) + ((2 * |.b₂.|) * |.b₂.|) & |.b₁.| * |.b₁.| <= ((2 * |.(b₁ - b₂).|) * |.(b₁ - b₂).|) + ((2 * |.b₂.|) * |.b₂.|) )

proof end;

Lemma24: for b₁ being Complex
for b₂ being Complex_Sequence st b₂ is convergent holds
for b₃ being Real_Sequence st ( for b₄ being Nat holds b₃ . b₄ = |.((b₂ . b₄) - b₁).| * |.((b₂ . b₄) - b₁).| ) holds
( b₃ is convergent & lim b₃ = |.((lim b₂) - b₁).| * |.((lim b₂) - b₁).| )

proof end;

Lemma25: for b₁ being Complex
for b₂ being Real_Sequence
for b₃ being Complex_Sequence st b₃ is convergent & b₂ is convergent holds
for b₄ being Real_Sequence st ( for b₅ being Nat holds b₄ . b₅ = (|.((b₃ . b₅) - b₁).| * |.((b₃ . b₅) - b₁).|) + (b₂ . b₅) ) holds
( b₄ is convergent & lim b₄ = (|.((lim b₃) - b₁).| * |.((lim b₃) - b₁).|) + (lim b₂) )

proof end;

theorem Th3: :: CSSPACE2:3

for b₁ being sequence of Complex_l2_Space st b₁ is Cauchy holds
b₁ is convergent

proof end;

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

registration

cluster Complex_l2_Space -> ComplexUnitarySpace-like Hilbert ;
coherence by Lemma26, CLVECT_2:def 13;

end;

theorem Th4: :: CSSPACE2:4

for b₁, b₂ being Complex st (Re b₁) * (Im b₂) = (Re b₂) * (Im b₁) & ((Re b₁) * (Re b₂)) + ((Im b₁) * (Im b₂)) >= 0 holds
|.(b₁ + b₂).| = |.b₁.| + |.b₂.| by Lemma4;

theorem Th5: :: CSSPACE2:5

for b₁, b₂ being Complex holds 2 * |.(b₁ * b₂).| <= (|.b₁.| ^2 ) + (|.b₂.| ^2 ) by Lemma22;

theorem Th6: :: CSSPACE2:6

for b₁, b₂ being Complex holds
( |.(b₁ + b₂).| * |.(b₁ + b₂).| <= ((2 * |.b₁.|) * |.b₁.|) + ((2 * |.b₂.|) * |.b₂.|) & |.b₁.| * |.b₁.| <= ((2 * |.(b₁ - b₂).|) * |.(b₁ - b₂).|) + ((2 * |.b₂.|) * |.b₂.|) ) by Lemma23;

theorem Th7: :: CSSPACE2:7

for b₁ being Complex_Sequence holds b₁ = (b₁ *' ) *' by Lemma1;

theorem Th8: :: CSSPACE2:8

for b₁ being Complex_Sequence holds Partial_Sums (b₁ *' ) = (Partial_Sums b₁) *' by Lemma2;

theorem Th9: :: CSSPACE2:9

for b₁ being Complex_Sequence
for b₂ being Nat st ( for b₃ being Nat holds
( (Re b₁) . b₃ >= 0 & (Im b₁) . b₃ = 0 ) ) holds
|.(Partial_Sums b₁).| . b₂ = (Partial_Sums |.b₁.|) . b₂ by Lemma5;

theorem Th10: :: CSSPACE2:10

for b₁ being Complex_Sequence st b₁ is summable holds
Sum (b₁ *' ) = (Sum b₁) *' by Lemma6;

theorem Th11: :: CSSPACE2:11

for b₁ being Complex_Sequence st b₁ is absolutely_summable holds
|.(Sum b₁).| <= Sum |.b₁.| by Lemma7;

theorem Th12: :: CSSPACE2:12

for b₁ being Complex_Sequence st b₁ is summable & ( for b₂ being Nat holds
( (Re b₁) . b₂ >= 0 & (Im b₁) . b₂ = 0 ) ) holds
|.(Sum b₁).| = Sum |.b₁.| by Lemma8;

theorem Th13: :: CSSPACE2:13

for b₁ being Complex_Sequence
for b₂ being Nat holds
( (Re (b₁ (#) (b₁ *' ))) . b₂ >= 0 & (Im (b₁ (#) (b₁ *' ))) . b₂ = 0 ) by Lemma9;

theorem Th14: :: CSSPACE2:14

for b₁ being Complex_Sequence st b₁ is absolutely_summable & Sum |.b₁.| = 0 holds
for b₂ being Nat holds b₁ . b₂ = 0c

proof end;

theorem Th15: :: CSSPACE2:15

for b₁ being Complex_Sequence holds |.b₁.| = |.(b₁ *' ).| by Lemma19;

theorem Th16: :: CSSPACE2:16

for b₁ being Complex
for b₂ being Complex_Sequence st b₂ is convergent holds
for b₃ being Real_Sequence st ( for b₄ being Nat holds b₃ . b₄ = |.((b₂ . b₄) - b₁).| * |.((b₂ . b₄) - b₁).| ) holds
( b₃ is convergent & lim b₃ = |.((lim b₂) - b₁).| * |.((lim b₂) - b₁).| ) by Lemma24;

theorem Th17: :: CSSPACE2:17

for b₁ being Complex
for b₂ being Real_Sequence
for b₃ being Complex_Sequence st b₃ is convergent & b₂ is convergent holds
for b₄ being Real_Sequence st ( for b₅ being Nat holds b₄ . b₅ = (|.((b₃ . b₅) - b₁).| * |.((b₃ . b₅) - b₁).|) + (b₂ . b₅) ) holds
( b₄ is convergent & lim b₄ = (|.((lim b₃) - b₁).| * |.((lim b₃) - b₁).|) + (lim b₂) ) by Lemma25;

theorem Th18: :: CSSPACE2:18

theorem Th19: :: CSSPACE2:19