Complex_Sequence means
:: COMSEQ_3:def 1
it.0 = 1r & for n holds it.(n+1) = it.n * z;
end;
definition
let z be Complex, n be Nat;
redefine func z |^ n -> Element of COMPLEX equals
:: COMSEQ_3:def 2
z GeoSeq.n;
end;
theorem :: COMSEQ_3:11
z |^ 0 = 1r;
definition
let f be complex-valued Function;
func Re f -> Function means
:: COMSEQ_3:def 3
dom it = dom f & for x be object st x in dom it holds it.x = Re(f.x);
func Im f -> Function means
:: COMSEQ_3:def 4
dom it = dom f & for x be object st x in dom it holds it.x = Im(f.x);
end;
registration
let f be complex-valued Function;
cluster Re f -> real-valued;
cluster Im f -> real-valued;
end;
definition
let X be set, f be PartFunc of X,COMPLEX;
redefine func Re f -> PartFunc of X,REAL;
redefine func Im f -> PartFunc of X,REAL;
end;
definition
let c be Complex_Sequence;
redefine func Re c -> Real_Sequence means
:: COMSEQ_3:def 5
for n holds it.n = Re(c.n);
redefine func Im c -> Real_Sequence means
:: COMSEQ_3:def 6
for n holds it.n = Im(c.n);
end;
theorem :: COMSEQ_3:12
|.z.| <= |.Re z.| + |.Im z.|;
theorem :: COMSEQ_3:13
|.Re z.| <= |.z.| & |.Im z.| <= |.z.|;
theorem :: COMSEQ_3:14
Re seq1=Re seq2 & Im seq1=Im seq2 implies seq1=seq2;
theorem :: COMSEQ_3:15
Re seq1 + Re seq2 = Re (seq1+seq2) & Im seq1 + Im seq2 = Im (
seq1+seq2 qua Complex_Sequence);
theorem :: COMSEQ_3:16
-(Re seq) = Re (-seq) & -(Im seq) = Im -seq;
theorem :: COMSEQ_3:17
r*Re(z)=Re(r*z) & r*Im(z)=Im(r*z);
theorem :: COMSEQ_3:18
Re seq1-Re seq2=Re (seq1-seq2) & Im seq1-Im seq2=Im(seq1-seq2);
theorem :: COMSEQ_3:19
r(#)Re seq = Re (r (#) seq) & r(#)Im seq = Im (r (#) seq);
theorem :: COMSEQ_3:20
Re (z (#) seq) = Re z (#) Re seq - Im z (#) Im seq & Im (z (#) seq) =
Re z (#) Im seq + Im z (#) Re seq;
theorem :: COMSEQ_3:21
Re (seq1 (#) seq2) = Re seq1(#)Re seq2-Im seq1(#)Im seq2 & Im (seq1
(#) seq2) = Re seq1(#)Im seq2+Im seq1(#)Re seq2;
definition
let Nseq be increasing sequence of NAT, seq be Complex_Sequence;
redefine func seq * Nseq -> Complex_Sequence;
end;
theorem :: COMSEQ_3:22
Re (seq*Nseq)=(Re seq)*Nseq & Im (seq*Nseq)=(Im seq)*Nseq;
theorem :: COMSEQ_3:23
(Re seq)^\k =Re (seq^\k) & (Im seq)^\k =Im (seq^\k);
definition
let s be Complex_Sequence;
redefine func Partial_Sums s -> Complex_Sequence;
end;
definition
let seq be Complex_Sequence;
func Sum seq -> Element of COMPLEX equals
:: COMSEQ_3:def 7
lim Partial_Sums seq;
end;
theorem :: COMSEQ_3:24
(for n holds seq.n = 0c) implies for m holds (Partial_Sums seq). m = 0c;
theorem :: COMSEQ_3:25
(for n holds seq.n = 0c) implies for m holds (Partial_Sums |.seq .|).m = 0;
theorem :: COMSEQ_3:26
Partial_Sums Re seq = Re (Partial_Sums seq) & Partial_Sums Im
seq = Im (Partial_Sums seq);
theorem :: COMSEQ_3:27
Partial_Sums(seq1)+Partial_Sums(seq2) = Partial_Sums(seq1+seq2);
theorem :: COMSEQ_3:28
Partial_Sums(seq1)-Partial_Sums(seq2) = Partial_Sums(seq1-seq2);
theorem :: COMSEQ_3:29
for z being Complex holds Partial_Sums(z (#) seq) = z (#)
Partial_Sums(seq);
theorem :: COMSEQ_3:30
|.Partial_Sums(seq).k.| <= (Partial_Sums |.seq.|).k;
theorem :: COMSEQ_3:31
|.Partial_Sums(seq).m- Partial_Sums(seq).n.| <= |.
Partial_Sums(|.seq.|).m- Partial_Sums(|.seq.|).n.|;
theorem :: COMSEQ_3:32
Partial_Sums(Re seq)^\k =Re (Partial_Sums(seq)^\k) &
Partial_Sums(Im seq)^\k =Im (Partial_Sums(seq)^\k);
theorem :: COMSEQ_3:33
(for n holds seq1.n=seq.0) implies Partial_Sums(seq^\1) = (
Partial_Sums(seq)^\1) - seq1;
theorem :: COMSEQ_3:34
Partial_Sums |.seq.| is non-decreasing;
registration
let seq be Complex_Sequence;
cluster Partial_Sums |.seq.| -> non-decreasing for Real_Sequence;
end;
theorem :: COMSEQ_3:35
(for n st n <= m holds seq1.n = seq2.n) implies Partial_Sums(seq1).m =
Partial_Sums(seq2).m;
theorem :: COMSEQ_3:36
1r <> z implies for n holds Partial_Sums(z GeoSeq).n = (1r - z
|^ (n+1))/(1r-z);
theorem :: COMSEQ_3:37
z <> 1r & (for n holds seq.(n+1) = z * seq.n) implies for n
holds Partial_Sums(seq).n = seq.0 * ((1r - z |^ (n+1))/(1r-z));
begin :: Convergence of Complex Sequences
theorem :: COMSEQ_3:38
for a, b being Real_Sequence, c being Complex_Sequence st (for n
holds Re (c.n) = a.n & Im (c.n) = b.n) holds a is convergent & b is convergent
iff c is convergent;
theorem :: COMSEQ_3:39
for a, b being convergent Real_Sequence, c being
Complex_Sequence st (for n holds Re (c.n) = a.n & Im (c.n) = b.n) holds c is
convergent & lim(c)= lim(a) + lim(b)**;
theorem :: COMSEQ_3:40
for a, b being Real_Sequence, c being convergent
Complex_Sequence st (for n holds Re (c.n) = a.n & Im (c.n) = b.n) holds a is
convergent & b is convergent & lim a=Re lim c & lim b=Im lim c;
theorem :: COMSEQ_3:41
for c being convergent Complex_Sequence holds Re c is convergent
& Im c is convergent & lim Re c = Re lim c & lim Im c = Im lim c;
registration
let c be convergent Complex_Sequence;
cluster Re c -> convergent for Real_Sequence;
cluster Im c -> convergent for Real_Sequence;
end;
theorem :: COMSEQ_3:42
for c being Complex_Sequence st Re c is convergent & Im c is
convergent holds c is convergent & Re(lim(c))=lim(Re c) & Im (lim(c))=lim(Im c)
;
theorem :: COMSEQ_3:43
(0 < |.z.| & |.z.| < 1 & seq.0 = z & for n holds seq.(n+1) = seq
.n * z) implies seq is convergent & lim(seq)=0c;
theorem :: COMSEQ_3:44
|.z.| < 1 & (for n holds seq.n=z |^ (n+1)) implies seq is
convergent & lim(seq)=0c;
theorem :: COMSEQ_3:45
r>0 & (ex m st for n st n>=m holds |.seq.n.| >= r) implies not |.seq.|
is convergent or lim |.seq.| <> 0;
theorem :: COMSEQ_3:46
seq is convergent iff for p st 0*

* convergent for Complex_Sequence;
end;
definition
let seq be Complex_Sequence;
attr seq is absolutely_summable means
:: COMSEQ_3:def 9
|.seq.| is summable;
end;
theorem :: COMSEQ_3:51
(for n holds seq.n = 0c) implies seq is absolutely_summable;
registration
cluster absolutely_summable for Complex_Sequence;
end;
registration
let seq be absolutely_summable Complex_Sequence;
cluster |.seq.| -> summable for Real_Sequence;
end;
theorem :: COMSEQ_3:52
seq is summable implies seq is convergent & lim seq = 0c;
registration
cluster summable -> convergent for Complex_Sequence;
end;
theorem :: COMSEQ_3:53
seq is summable implies Re seq is summable & Im seq is summable
& Sum(seq)= Sum(Re seq)+Sum(Im seq)* ;
registration
let seq be summable Complex_Sequence;
cluster Re seq -> summable for Real_Sequence;
cluster Im seq -> summable for Real_Sequence;
end;
theorem :: COMSEQ_3:54
seq1 is summable & seq2 is summable implies seq1+seq2 is
summable & Sum(seq1+seq2)= Sum(seq1)+Sum(seq2);
theorem :: COMSEQ_3:55
seq1 is summable & seq2 is summable implies seq1-seq2 is
summable & Sum(seq1-seq2)= Sum(seq1)-Sum(seq2);
registration
let seq1, seq2 be summable Complex_Sequence;
cluster seq1 + seq2 -> summable for Complex_Sequence;
cluster seq1 - seq2 -> summable for Complex_Sequence;
end;
theorem :: COMSEQ_3:56
seq is summable implies for z being Complex holds z (#)
seq is summable & Sum(z (#) seq)= z * Sum(seq);
registration
let z be Element of COMPLEX, seq be summable Complex_Sequence;
cluster z (#) seq -> summable for Complex_Sequence;
end;
theorem :: COMSEQ_3:57
Re seq is summable & Im seq is summable implies seq is summable
& Sum(seq)=Sum(Re seq)+Sum(Im seq)*;
theorem :: COMSEQ_3:58
seq is summable implies for n holds seq^\n is summable;
registration
let seq be summable Complex_Sequence, n be Nat;
cluster seq^\n -> summable for Complex_Sequence;
end;
theorem :: COMSEQ_3:59
(ex n st seq^\n is summable) implies seq is summable;
theorem :: COMSEQ_3:60
seq is summable implies for n holds Sum(seq) = Partial_Sums(seq).n +
Sum(seq^\(n+1));
theorem :: COMSEQ_3:61
Partial_Sums |.seq.| is bounded_above iff seq is absolutely_summable;
registration
let seq be absolutely_summable Complex_Sequence;
cluster Partial_Sums |.seq.| -> bounded_above for Real_Sequence;
end;
theorem :: COMSEQ_3:62
seq is summable iff for p st 0*

* summable for Complex_Sequence;
end;
registration
cluster absolutely_summable for Complex_Sequence;
end;
theorem :: COMSEQ_3:64
|.z.| < 1 implies z GeoSeq is summable & Sum(z GeoSeq) = 1r/(1r- z);
theorem :: COMSEQ_3:65
|.z.| < 1 & (for n holds seq.(n+1) = z * seq.n) implies seq is
summable & Sum(seq) = seq.0/(1r-z);
theorem :: COMSEQ_3:66
rseq1 is summable & (ex m st for n st m<=n holds |.seq2.n.| <= rseq1.n
) implies seq2 is absolutely_summable;
theorem :: COMSEQ_3:67
(for n holds 0 <= |.seq1.|.n & |.seq1.|.n <= |.seq2.|.n) & seq2 is
absolutely_summable implies seq1 is absolutely_summable & Sum |.seq1.| <= Sum
|.seq2.|;
theorem :: COMSEQ_3:68
(for n holds |.seq.|.n>0) & (ex m st for n st n>=m holds |.seq.|.(n+1)
/|.seq.|.n >= 1) implies not seq is absolutely_summable;
theorem :: COMSEQ_3:69
(for n holds rseq1.n = n-root (|.seq.|.n)) & rseq1 is convergent & lim
rseq1 < 1 implies seq is absolutely_summable;
theorem :: COMSEQ_3:70
(for n holds rseq1.n = n-root (|.seq.|.n)) & (ex m st for n st m<=n
holds rseq1.n>= 1) implies |.seq.| is not summable;
theorem :: COMSEQ_3:71
(for n holds rseq1.n = n-root (|.seq.|.n)) & rseq1 is convergent & lim
rseq1 > 1 implies seq is not absolutely_summable;
theorem :: COMSEQ_3:72
|.seq .| is non-increasing & (for n holds rseq1.n = 2 to_power n * |.
seq.|.(2 to_power n)) implies (seq is absolutely_summable iff rseq1 is summable
);
theorem :: COMSEQ_3:73
p>1 & (for n st n>=1 holds |.seq.|.n = 1/n to_power p) implies seq is
absolutely_summable;
theorem :: COMSEQ_3:74
p<=1 & (for n st n>=1 holds |.seq.|.n=1/n to_power p) implies not seq
is absolutely_summable;
theorem :: COMSEQ_3:75
(for n holds seq.n<>0c & rseq1.n=|.seq.|.(n+1)/|.seq.|.n) & rseq1 is
convergent & lim rseq1 < 1 implies seq is absolutely_summable;
theorem :: COMSEQ_3:76
(for n holds seq.n<>0c) & (ex m st for n st n>=m holds |.seq.|.(n+1)/
|.seq.|.n >= 1) implies seq is not absolutely_summable;
*