environ
vocabularies HIDDEN, NUMBERS, COMSEQ_1, ARYTM_3, FUNCT_1, SUBSET_1, COMPLEX1, ARYTM_1, RELAT_1, XCMPLX_0, SERIES_1, CARD_1, REAL_1, XXREAL_0, SQUARE_1, CARD_3, ORDINAL2, SEQ_2, VALUED_1, CSSPACE, RSSPACE, SUPINF_2, RLVECT_1, ALGSTR_0, ZFMISC_1, STRUCT_0, REALSET1, PROB_2, BHSP_1, SEQ_1, PRE_TOPC, FUNCOP_1, NAT_1, BHSP_3, NORMSP_1, XXREAL_2, REWRITE1, CSSPACE2;
notations HIDDEN, SUBSET_1, ZFMISC_1, ORDINAL1, XCMPLX_0, XXREAL_0, NUMBERS, COMPLEX1, XREAL_0, NAT_1, STRUCT_0, ALGSTR_0, RELAT_1, DOMAIN_1, PARTFUN1, FUNCT_1, FUNCT_2, BINOP_1, FUNCOP_1, REALSET1, PRE_TOPC, SQUARE_1, VALUED_1, SEQ_1, SEQ_2, SERIES_1, COMSEQ_1, COMSEQ_2, COMSEQ_3, NORMSP_0, CLVECT_1, CLVECT_2, CSSPACE;
definitions CLVECT_2;
theorems RELAT_1, SQUARE_1, ABSVALUE, ZFMISC_1, SEQ_1, SEQ_2, SEQM_3, SERIES_1, INT_1, FUNCT_1, FUNCT_2, RLVECT_1, SEQ_4, RSSPACE, XCMPLX_1, CSSPACE, CLVECT_1, COMSEQ_1, COMSEQ_2, COMSEQ_3, COMPLEX1, CLVECT_2, RSSPACE2, FUNCOP_1, XREAL_1, XXREAL_0, VALUED_1, XCMPLX_0, ORDINAL1;
schemes NAT_1, SEQ_1, FUNCT_2, COMSEQ_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, MEMBERED, COMSEQ_2, COMSEQ_3, REALSET1, STRUCT_0, CSSPACE, VALUED_1, VALUED_0, SEQ_2, XREAL_0, SQUARE_1, NAT_1, INT_1;
constructors HIDDEN, BINOP_1, FUNCOP_1, REAL_1, SQUARE_1, COMSEQ_2, COMSEQ_3, REALSET1, CLVECT_2, SEQ_2, RELSET_1, CFUNCDOM;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities SQUARE_1, REALSET1, BINOP_1, STRUCT_0, ALGSTR_0, VALUED_1, CSSPACE, CFUNCDOM;
expansions ;
Lm1:
for seq being Complex_Sequence holds Partial_Sums (seq *') = (Partial_Sums seq) *'
Lm2:
for a, b being Real holds 0 <= (a ^2) + (b ^2)
Lm3:
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.|
Lm4:
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
Lm5:
for seq being Complex_Sequence st seq is summable holds
Sum (seq *') = (Sum seq) *'
Lm6:
for seq being Complex_Sequence st seq is absolutely_summable holds
|.(Sum seq).| <= Sum |.seq.|
Lm7:
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.|
Lm8:
for seq being Complex_Sequence
for n being Nat holds
( (Re (seq (#) (seq *'))) . n >= 0 & (Im (seq (#) (seq *'))) . n = 0 )
Lm9:
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 ) )
Lm10:
0. Complex_l2_Space = CZeroseq
Lm12:
for u, v being VECTOR of Complex_l2_Space holds u + v = (seq_id u) + (seq_id v)
Lm13:
for r being Complex
for u being VECTOR of Complex_l2_Space holds r * u = r (#) (seq_id u)
Lm14:
for u being VECTOR of Complex_l2_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )
Lm15:
for u, v being VECTOR of Complex_l2_Space holds u - v = (seq_id u) - (seq_id v)
Lm16:
for v, w being VECTOR of Complex_l2_Space holds |.(seq_id v).| (#) |.(seq_id w).| is summable
Lm18:
for seq being Complex_Sequence holds |.seq.| = |.(seq *').|
Lm19:
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 ) )
theorem
( 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 Lm9, Lm10, Lm12, Lm13, Lm14, Lm15, Lm16, Lm19, CSSPACE:def 17;
Lm20:
for x, y being Complex holds 2 * |.(x * y).| <= (|.x.| ^2) + (|.y.| ^2)
Lm21:
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.|) )
Lm22:
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).| )
Lm23:
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) )