:: Cauchy Sequence of Complex Unitary Space
:: by Yasumasa Suzuki and Noboru Endou
::
:: Received March 18, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

deffunc H1( ComplexUnitarySpace) ->  Element of the U1 of $1 = 0. $1;

theorem Th1: :: CLVECT_3:1
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X holds (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2)
proofend;

theorem Th2: :: CLVECT_3:2
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X holds (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2)
proofend;

theorem Th3: :: CLVECT_3:3
for X being ComplexUnitarySpace
for seq being sequence of X
for z being Complex holds Partial_Sums (z * seq) = z * (Partial_Sums seq)
proofend;

theorem :: CLVECT_3:4
for X being ComplexUnitarySpace
for seq being sequence of X holds Partial_Sums (- seq) = - (Partial_Sums seq)
proofend;

theorem :: CLVECT_3:5
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X
for z1, z2 being Complex holds (z1 * (Partial_Sums seq1)) + (z2 * (Partial_Sums seq2)) = Partial_Sums ((z1 * seq1) + (z2 * seq2))
proofend;

definition
let X be ComplexUnitarySpace;
let seq be sequence of X;
attrseq is summable  means :Def1: :: CLVECT_3:def 1
 Partial_Sums seq is convergent ;
func Sum seq ->  Point of X equals :: CLVECT_3:def 2
 lim (Partial_Sums seq);
correctness
coherence
lim (Partial_Sums seq) is Point of X;
;
end;

:: deftheorem Def1 defines summable CLVECT_3:def_1_:_
 for X being ComplexUnitarySpace
for seq being sequence of X holds
( seq is summable iff Partial_Sums seq is convergent );

:: deftheorem  defines Sum CLVECT_3:def_2_:_
 for X being ComplexUnitarySpace
for seq being sequence of X holds Sum seq = lim (Partial_Sums seq);

theorem :: CLVECT_3:6
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is summable & seq2 is summable holds
( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) )
proofend;

theorem :: CLVECT_3:7
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is summable & seq2 is summable holds
( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) )
proofend;

theorem :: CLVECT_3:8
for X being ComplexUnitarySpace
for seq being sequence of X
for z being Complex st seq is summable holds
( z * seq is summable & Sum (z * seq) = z * (Sum seq) )
proofend;

theorem Th9: :: CLVECT_3:9
for X being ComplexUnitarySpace
for seq being sequence of X st seq is summable holds
( seq is convergent & lim seq = 0. X )
proofend;

theorem Th10: :: CLVECT_3:10
for X being ComplexHilbertSpace
for seq being sequence of X holds
( seq is summable iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r )
proofend;

theorem :: CLVECT_3:11
for X being ComplexUnitarySpace
for seq being sequence of X st seq is summable holds
Partial_Sums seq is bounded
proofend;

theorem Th12: :: CLVECT_3:12
for X being ComplexUnitarySpace
for seq1, seq being sequence of X st ( for n being Element of NAT holds seq1 . n = seq . 0 ) holds
Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1
proofend;

theorem Th13: :: CLVECT_3:13
for X being ComplexUnitarySpace
for seq being sequence of X st seq is summable holds
for k being Element of NAT holds seq ^\ k is summable
proofend;

theorem :: CLVECT_3:14
for X being ComplexUnitarySpace
for seq being sequence of X st ex k being Element of NAT st seq ^\ k is summable holds
seq is summable
proofend;

definition
let X be ComplexUnitarySpace;
let seq be sequence of X;
let n be Element of NAT ;
func Sum (seq,n) ->  Point of X equals :: CLVECT_3:def 3
(Partial_Sums seq) . n;
correctness
coherence
(Partial_Sums seq) . n is Point of X;
;
end;

:: deftheorem  defines Sum CLVECT_3:def_3_:_
 for X being ComplexUnitarySpace
for seq being sequence of X
for n being Element of NAT holds Sum (seq,n) = (Partial_Sums seq) . n;

theorem :: CLVECT_3:15
for X being ComplexUnitarySpace
for seq being sequence of X holds Sum (seq,0) = seq . 0 by BHSP_4:def_1;

theorem Th16: :: CLVECT_3:16
for X being ComplexUnitarySpace
for seq being sequence of X holds Sum (seq,1) = (Sum (seq,0)) + (seq . 1)
proofend;

theorem Th17: :: CLVECT_3:17
for X being ComplexUnitarySpace
for seq being sequence of X holds Sum (seq,1) = (seq . 0) + (seq . 1)
proofend;

theorem :: CLVECT_3:18
for X being ComplexUnitarySpace
for seq being sequence of X
for n being Element of NAT holds Sum (seq,(n + 1)) = (Sum (seq,n)) + (seq . (n + 1)) by BHSP_4:def_1;

theorem Th19: :: CLVECT_3:19
for X being ComplexUnitarySpace
for seq being sequence of X
for n being Element of NAT holds seq . (n + 1) = (Sum (seq,(n + 1))) - (Sum (seq,n))
proofend;

theorem :: CLVECT_3:20
for X being ComplexUnitarySpace
for seq being sequence of X holds seq . 1 = (Sum (seq,1)) - (Sum (seq,0))
proofend;

definition
let X be ComplexUnitarySpace;
let seq be sequence of X;
let n, m be Element of NAT ;
func Sum (seq,n,m) ->  Point of X equals :: CLVECT_3:def 4
(Sum (seq,n)) - (Sum (seq,m));
correctness
coherence
(Sum (seq,n)) - (Sum (seq,m)) is Point of X;
;
end;

:: deftheorem  defines Sum CLVECT_3:def_4_:_
 for X being ComplexUnitarySpace
for seq being sequence of X
for n, m being Element of NAT holds Sum (seq,n,m) = (Sum (seq,n)) - (Sum (seq,m));

theorem :: CLVECT_3:21
for X being ComplexUnitarySpace
for seq being sequence of X holds Sum (seq,1,0) = seq . 1
proofend;

theorem :: CLVECT_3:22
for X being ComplexUnitarySpace
for seq being sequence of X
for n being Element of NAT holds Sum (seq,(n + 1),n) = seq . (n + 1) by Th19;

theorem Th23: :: CLVECT_3:23
for X being ComplexHilbertSpace
for seq being sequence of X holds
( seq is summable iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k &amp; m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r )
proofend;

theorem :: CLVECT_3:24
for X being ComplexHilbertSpace
for seq being sequence of X holds
( seq is summable iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k &amp; m >= k holds
||.(Sum (seq,n,m)).|| < r )
proofend;

definition
let Cseq be Complex_Sequence;
let n be Element of NAT ;
func Sum (Cseq,n) ->  Complex equals :: CLVECT_3:def 5
(Partial_Sums Cseq) . n;
correctness
coherence
(Partial_Sums Cseq) . n is Complex;
;
end;

:: deftheorem  defines Sum CLVECT_3:def_5_:_
 for Cseq being Complex_Sequence
for n being Element of NAT holds Sum (Cseq,n) = (Partial_Sums Cseq) . n;

definition
let Cseq be Complex_Sequence;
let n, m be Element of NAT ;
func Sum (Cseq,n,m) ->  Complex equals :: CLVECT_3:def 6
(Sum (Cseq,n)) - (Sum (Cseq,m));
correctness
coherence
(Sum (Cseq,n)) - (Sum (Cseq,m)) is Complex;
;
end;

:: deftheorem  defines Sum CLVECT_3:def_6_:_
 for Cseq being Complex_Sequence
for n, m being Element of NAT holds Sum (Cseq,n,m) = (Sum (Cseq,n)) - (Sum (Cseq,m));

definition
let X be ComplexUnitarySpace;
let seq be sequence of X;
attrseq is absolutely_summable  means :Def7: :: CLVECT_3:def 7
||.seq.|| is summable ;
end;

:: deftheorem Def7 defines absolutely_summable CLVECT_3:def_7_:_
 for X being ComplexUnitarySpace
for seq being sequence of X holds
( seq is absolutely_summable iff ||.seq.|| is summable );

theorem :: CLVECT_3:25
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is absolutely_summable &amp; seq2 is absolutely_summable holds
seq1 + seq2 is absolutely_summable
proofend;

theorem :: CLVECT_3:26
for X being ComplexUnitarySpace
for seq being sequence of X
for z being Complex st seq is absolutely_summable holds
z * seq is absolutely_summable
proofend;

theorem :: CLVECT_3:27
for X being ComplexUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence st ( for n being Element of NAT holds ||.seq.|| . n <= Rseq . n ) &amp; Rseq is summable holds
seq is absolutely_summable
proofend;

theorem :: CLVECT_3:28
for X being ComplexUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence st ( for n being Element of NAT holds
( seq . n <> 0. X &amp; Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) ) &amp; Rseq is convergent &amp; lim Rseq < 1 holds
seq is absolutely_summable
proofend;

theorem Th29: :: CLVECT_3:29
for X being ComplexUnitarySpace
for seq being sequence of X
for r being Real st r > 0 &amp; ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.(seq . n).|| >= r &amp; seq is convergent holds
lim seq <> 0. X
proofend;

theorem Th30: :: CLVECT_3:30
for X being ComplexUnitarySpace
for seq being sequence of X st ( for n being Element of NAT holds seq . n <> 0. X ) &amp; ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 holds
not seq is summable
proofend;

theorem :: CLVECT_3:31
for X being ComplexUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence st ( for n being Element of NAT holds seq . n <> 0. X ) &amp; ( for n being Element of NAT holds Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) &amp; Rseq is convergent &amp; lim Rseq > 1 holds
not seq is summable
proofend;

theorem :: CLVECT_3:32
for X being ComplexUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence st ( for n being Element of NAT holds Rseq . n = n -root ||.(seq . n).|| ) &amp; Rseq is convergent &amp; lim Rseq < 1 holds
seq is absolutely_summable
proofend;

theorem :: CLVECT_3:33
for X being ComplexUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence st ( for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ) &amp; ex m being Element of NAT st
for n being Element of NAT st n >= m holds
Rseq . n >= 1 holds
not seq is summable
proofend;

theorem :: CLVECT_3:34
for X being ComplexUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence st ( for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ) &amp; Rseq is convergent &amp; lim Rseq > 1 holds
not seq is summable
proofend;

theorem Th35: :: CLVECT_3:35
for X being ComplexUnitarySpace
for seq being sequence of X holds Partial_Sums ||.seq.|| is non-decreasing
proofend;

theorem :: CLVECT_3:36
for X being ComplexUnitarySpace
for seq being sequence of X
for n being Element of NAT holds (Partial_Sums ||.seq.||) . n >= 0
proofend;

theorem Th37: :: CLVECT_3:37
for X being ComplexUnitarySpace
for seq being sequence of X
for n being Element of NAT holds ||.((Partial_Sums seq) . n).|| <= (Partial_Sums ||.seq.||) . n
proofend;

theorem :: CLVECT_3:38
for X being ComplexUnitarySpace
for seq being sequence of X
for n being Element of NAT holds ||.(Sum (seq,n)).|| <= Sum (||.seq.||,n)
proofend;

theorem Th39: :: CLVECT_3:39
for X being ComplexUnitarySpace
for seq being sequence of X
for n, m being Element of NAT holds ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n))
proofend;

theorem Th40: :: CLVECT_3:40
for X being ComplexUnitarySpace
for seq being sequence of X
for n, m being Element of NAT holds ||.((Sum (seq,m)) - (Sum (seq,n))).|| <= abs ((Sum (||.seq.||,m)) - (Sum (||.seq.||,n)))
proofend;

theorem :: CLVECT_3:41
for X being ComplexUnitarySpace
for seq being sequence of X
for n, m being Element of NAT holds ||.(Sum (seq,m,n)).|| <= abs (Sum (||.seq.||,m,n))
proofend;

theorem :: CLVECT_3:42
for X being ComplexHilbertSpace
for seq being sequence of X st seq is absolutely_summable holds
seq is summable
proofend;

definition
let X be ComplexUnitarySpace;
let seq be sequence of X;
let Cseq be Complex_Sequence;
funcCseq * seq ->  sequence of X means :Def8: :: CLVECT_3:def 8
 for n being Element of NAT holds it . n = (Cseq . n) * (seq . n);
existence
 ex b1 being sequence of X st
for n being Element of NAT holds b1 . n = (Cseq . n) * (seq . n)
proofend;
uniqueness
 for b1, b2 being sequence of X st ( for n being Element of NAT holds b1 . n = (Cseq . n) * (seq . n) ) &amp; ( for n being Element of NAT holds b2 . n = (Cseq . n) * (seq . n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines * CLVECT_3:def_8_:_
 for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq being Complex_Sequence
for b4 being sequence of X holds
( b4 = Cseq * seq iff for n being Element of NAT holds b4 . n = (Cseq . n) * (seq . n) );

theorem :: CLVECT_3:43
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X
for Cseq being Complex_Sequence holds Cseq * (seq1 + seq2) = (Cseq * seq1) + (Cseq * seq2)
proofend;

theorem :: CLVECT_3:44
for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq1, Cseq2 being Complex_Sequence holds (Cseq1 + Cseq2) * seq = (Cseq1 * seq) + (Cseq2 * seq)
proofend;

theorem :: CLVECT_3:45
for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq1, Cseq2 being Complex_Sequence holds (Cseq1 (#) Cseq2) * seq = Cseq1 * (Cseq2 * seq)
proofend;

theorem Th46: :: CLVECT_3:46
for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq being Complex_Sequence
for z being Complex holds (z (#) Cseq) * seq = z * (Cseq * seq)
proofend;

theorem :: CLVECT_3:47
for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq being Complex_Sequence holds Cseq * (- seq) = (- Cseq) * seq
proofend;

theorem Th48: :: CLVECT_3:48
for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq being Complex_Sequence st Cseq is convergent &amp; seq is convergent holds
Cseq * seq is convergent
proofend;

theorem :: CLVECT_3:49
for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq being Complex_Sequence st Cseq is bounded &amp; seq is bounded holds
Cseq * seq is bounded
proofend;

theorem :: CLVECT_3:50
for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq being Complex_Sequence st Cseq is convergent &amp; seq is convergent holds
( Cseq * seq is convergent &amp; lim (Cseq * seq) = (lim Cseq) * (lim seq) )
proofend;

definition
let Cseq be Complex_Sequence;
attrCseq is Cauchy  means :Def9: :: CLVECT_3:def 9
 for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k &amp; m >= k holds
|.((Cseq . n) - (Cseq . m)).| < r;
end;

:: deftheorem Def9 defines Cauchy CLVECT_3:def_9_:_
 for Cseq being Complex_Sequence holds
( Cseq is Cauchy iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k &amp; m >= k holds
|.((Cseq . n) - (Cseq . m)).| < r );

theorem :: CLVECT_3:51
for Cseq being Complex_Sequence
for X being ComplexHilbertSpace
for seq being sequence of X st seq is Cauchy &amp; Cseq is Cauchy holds
Cseq * seq is Cauchy
proofend;

theorem Th52: :: CLVECT_3:52
for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq being Complex_Sequence
for n being Element of NAT holds (Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n = ((Partial_Sums (Cseq * seq)) . (n + 1)) - ((Cseq * (Partial_Sums seq)) . (n + 1))
proofend;

theorem Th53: :: CLVECT_3:53
for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq being Complex_Sequence
for n being Element of NAT holds (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq))) . n)
proofend;

theorem :: CLVECT_3:54
for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq being Complex_Sequence
for n being Element of NAT holds Sum ((Cseq * seq),(n + 1)) = ((Cseq * (Partial_Sums seq)) . (n + 1)) - (Sum ((((Cseq ^\ 1) - Cseq) * (Partial_Sums seq)),n)) by Th53;