Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

### The abstract of the Mizar article:

### Convergence and the Limit of Complex Sequences. Series

**by****Yasunari Shidama, and****Artur Kornilowicz**- Received June 25, 1997
- MML identifier: COMSEQ_3

- [ Mizar article, MML identifier index ]

environ vocabulary SEQ_1, COMSEQ_1, COMPLEX1, FUNCT_1, SERIES_1, ABSVALUE, ARYTM, ARYTM_1, SUPINF_2, SEQ_2, ARYTM_3, PROB_1, ORDINAL2, SEQM_3, PREPOWER, SQUARE_1, RLVECT_1, RELAT_1, POWER, LATTICES; notation SUBSET_1, ORDINAL1, NUMBERS, ARYTM_0, XCMPLX_0, XREAL_0, REAL_1, RELAT_1, FUNCT_2, SEQ_1, SEQ_2, NAT_1, SEQM_3, ABSVALUE, SERIES_1, COMPLEX1, COMSEQ_1, COMSEQ_2, SQUARE_1, POWER; constructors SEQ_2, SEQM_3, SERIES_1, SQUARE_1, COMSEQ_1, COMSEQ_2, REAL_1, NAT_1, ABSVALUE, PARTFUN1, COMPLEX1, MEMBERED, ARYTM_0, ARYTM_3, FUNCT_4; clusters XREAL_0, COMSEQ_2, SEQ_1, COMSEQ_1, RELSET_1, SEQM_3, NAT_1, COMPLEX1, MEMBERED, ORDINAL2; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: Preliminaries reserve rseq,rseq1,rseq2 for Real_Sequence; reserve seq,seq1,seq2 for Complex_Sequence; reserve k, n, n1, n2, m for Nat; reserve p,r for Real; theorem :: COMSEQ_3:1 [*(n+1),0*] <> 0c & [*0,(n+1)*] <> 0c; theorem :: COMSEQ_3:2 (for n holds rseq.n = 0) implies for m holds (Partial_Sums abs(rseq)).m = 0; theorem :: COMSEQ_3:3 (for n holds rseq.n = 0) implies rseq is absolutely_summable; definition cluster absolutely_summable Real_Sequence; end; definition cluster summable -> convergent Real_Sequence; end; definition cluster absolutely_summable -> summable Real_Sequence; end; definition cluster absolutely_summable Real_Sequence; end; theorem :: COMSEQ_3:4 rseq is convergent implies (for p st 0<p ex n st for m,l be Nat st n <= m & n <= l holds abs(rseq.m-rseq.l)<p); theorem :: COMSEQ_3:5 (for n holds rseq.n <= p) implies for n, l be Nat holds Partial_Sums(rseq).(n+l)-Partial_Sums(rseq).n <= p * l; theorem :: COMSEQ_3:6 (for n holds rseq.n <= p) implies for n holds Partial_Sums(rseq).n <= p * (n+1); theorem :: COMSEQ_3:7 (for n st n <= m holds rseq1.n <= p * rseq2.n) implies Partial_Sums(rseq1).m <= p * Partial_Sums(rseq2).m; theorem :: COMSEQ_3:8 (for n st n <= m holds rseq1.n <= p * rseq2.n) implies for n st n <= m holds for l be Nat st n+l <= m holds Partial_Sums(rseq1).(n+l)-Partial_Sums(rseq1).n <= p * (Partial_Sums(rseq2).(n+l)-Partial_Sums(rseq2).n); theorem :: COMSEQ_3:9 (for n holds 0 <= rseq.n) implies (for n, m st n <= m holds abs(Partial_Sums(rseq).m-Partial_Sums(rseq).n) =Partial_Sums(rseq).m-Partial_Sums(rseq).n) & for n holds abs(Partial_Sums(rseq).n)=Partial_Sums(rseq).n; theorem :: COMSEQ_3:10 seq1 is convergent & seq2 is convergent & lim(seq1-seq2)=0c implies lim seq1 = lim seq2; begin :: The Operations on Complex Sequences reserve z for Element of COMPLEX; reserve Nseq,Nseq1 for increasing Seq_of_Nat; definition let z be Element of COMPLEX; func z GeoSeq -> Complex_Sequence means :: COMSEQ_3:def 1 it.0 = 1r & for n holds it.(n+1) = it.n * z; end; definition let z be Element of COMPLEX, n be Nat; func z #N n -> Element of COMPLEX equals :: COMSEQ_3:def 2 z GeoSeq.n; end; theorem :: COMSEQ_3:11 z #N 0 = 1r; definition let c be Complex_Sequence; func Re c -> Real_Sequence means :: COMSEQ_3:def 3 for n holds it.n = Re(c.n); end; definition let c be Complex_Sequence; func Im c -> Real_Sequence means :: COMSEQ_3:def 4 for n holds it.n = Im(c.n); end; theorem :: COMSEQ_3:12 |.z.| <= abs Re z + abs Im z; theorem :: COMSEQ_3:13 abs(Re z) <= |.z.| & abs(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); theorem :: COMSEQ_3:16 -(Re seq) = Re (-seq) & -(Im seq) = Im -seq; theorem :: COMSEQ_3:17 r*Re(z)=Re([*r,0*]*z) & r*Im(z)=Im([*r,0*]*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,0*] (#) seq) & r(#)Im seq = Im ([*r,0*] (#) 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 seq be Complex_Sequence, Nseq be increasing Seq_of_Nat; func seq (#) Nseq -> Complex_Sequence means :: COMSEQ_3:def 5 for n holds it.n = seq.(Nseq.n); end; theorem :: COMSEQ_3:22 Re (seq(#)Nseq)=(Re seq)*Nseq & Im (seq(#)Nseq)=(Im seq)*Nseq; definition let seq be Complex_Sequence, k be Nat; func seq ^\ k -> Complex_Sequence means :: COMSEQ_3:def 6 for n holds it.n=seq.(n+k); end; theorem :: COMSEQ_3:23 (Re seq)^\k =Re (seq^\k) & (Im seq)^\k =Im (seq^\k); definition let seq be Complex_Sequence; func Partial_Sums seq -> Complex_Sequence means :: COMSEQ_3:def 7 it.0 = seq.0 & for n holds it.(n+1) = it.n + seq.(n+1); end; definition let seq be Complex_Sequence; func Sum seq -> Element of COMPLEX equals :: COMSEQ_3:def 8 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 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.| <= abs( 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; definition let seq be Complex_Sequence; cluster Partial_Sums |.seq.| -> non-decreasing; 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 (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 (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)); definition let c be convergent Complex_Sequence; cluster Re c -> convergent; cluster Im c -> convergent; 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 (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<p ex n st for m st n <= m holds |.seq.m-seq.n.|<p; theorem :: COMSEQ_3:47 seq is convergent implies (for p st 0<p ex n st for m,l be Nat st n <= m & n <= l holds |.seq.m-seq.l.|<p); theorem :: COMSEQ_3:48 ((for n holds |. seq.n .| <= rseq.n) & rseq is convergent & lim(rseq)=0) implies seq is convergent & lim(seq)=0c; begin :: Summable and Absolutely Summable Complex Sequences definition let seq, seq1 be Complex_Sequence; pred seq is_subsequence_of seq1 means :: COMSEQ_3:def 9 ex Nseq st seq = seq1(#)Nseq; end; theorem :: COMSEQ_3:49 seq is_subsequence_of seq1 implies Re seq is_subsequence_of Re seq1 & Im seq is_subsequence_of Im seq1; theorem :: COMSEQ_3:50 seq is_subsequence_of seq1 & seq1 is_subsequence_of seq2 implies seq is_subsequence_of seq2; theorem :: COMSEQ_3:51 seq is bounded implies ex seq1 st seq1 is_subsequence_of seq & seq1 is convergent; definition let seq be Complex_Sequence; attr seq is summable means :: COMSEQ_3:def 10 Partial_Sums seq is convergent; end; definition cluster summable Complex_Sequence; end; definition let seq be summable Complex_Sequence; cluster Partial_Sums seq -> convergent; end; definition let seq; attr seq is absolutely_summable means :: COMSEQ_3:def 11 |.seq.| is summable; end; theorem :: COMSEQ_3:52 (for n holds seq.n = 0c) implies seq is absolutely_summable; definition cluster absolutely_summable Complex_Sequence; end; definition let seq be absolutely_summable Complex_Sequence; cluster |.seq.| -> summable; end; theorem :: COMSEQ_3:53 seq is summable implies seq is convergent & lim seq = 0c; definition cluster summable -> convergent Complex_Sequence; end; theorem :: COMSEQ_3:54 seq is summable implies Re seq is summable & Im seq is summable & Sum(seq)=[*Sum(Re seq),Sum(Im seq)*]; definition let seq be summable Complex_Sequence; cluster Re seq -> summable; cluster Im seq -> summable; end; theorem :: COMSEQ_3:55 seq1 is summable & seq2 is summable implies seq1+seq2 is summable & Sum(seq1+seq2)= Sum(seq1)+Sum(seq2); theorem :: COMSEQ_3:56 seq1 is summable & seq2 is summable implies seq1-seq2 is summable & Sum(seq1-seq2)= Sum(seq1)-Sum(seq2); definition let seq1, seq2 be summable Complex_Sequence; cluster seq1 + seq2 -> summable; cluster seq1 - seq2 -> summable; end; theorem :: COMSEQ_3:57 seq is summable implies z (#) seq is summable & Sum(z (#) seq)= z * Sum(seq); definition let z be Element of COMPLEX, seq be summable Complex_Sequence; cluster z (#) seq -> summable; end; theorem :: COMSEQ_3:58 Re seq is summable & Im seq is summable implies seq is summable & Sum(seq)=[*Sum(Re seq),Sum(Im seq)*]; theorem :: COMSEQ_3:59 seq is summable implies for n holds seq^\n is summable; definition let seq be summable Complex_Sequence, n be Nat; cluster seq^\n -> summable; end; theorem :: COMSEQ_3:60 (ex n st seq^\n is summable) implies seq is summable; theorem :: COMSEQ_3:61 seq is summable implies for n holds Sum(seq) = Partial_Sums(seq).n + Sum(seq^\(n+1)); theorem :: COMSEQ_3:62 Partial_Sums |.seq.| is bounded_above iff seq is absolutely_summable; definition let seq be absolutely_summable Complex_Sequence; cluster Partial_Sums |.seq.| -> bounded_above; end; theorem :: COMSEQ_3:63 seq is summable iff (for p st 0<p holds ex n st for m st n <= m holds |.Partial_Sums(seq).m-Partial_Sums(seq).n.|<p); theorem :: COMSEQ_3:64 seq is absolutely_summable implies seq is summable; definition cluster absolutely_summable -> summable Complex_Sequence; end; definition cluster absolutely_summable Complex_Sequence; end; theorem :: COMSEQ_3:65 |.z.| < 1 implies z GeoSeq is summable & Sum(z GeoSeq) = 1r/(1r-z); theorem :: COMSEQ_3:66 |.z.| < 1 & (for n holds seq.(n+1) = z * seq.n) implies seq is summable & Sum(seq) = seq.0/(1r-z); theorem :: COMSEQ_3:67 rseq1 is summable & (ex m st for n st m<=n holds |.seq2.n.| <= rseq1.n ) implies seq2 is absolutely_summable; theorem :: COMSEQ_3:68 (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:69 (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:70 (for n holds rseq1.n = n-root (|.seq.|.n)) & rseq1 is convergent & lim rseq1 < 1 implies seq is absolutely_summable; theorem :: COMSEQ_3:71 (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:72 (for n holds rseq1.n = n-root (|.seq.|.n)) & rseq1 is convergent & lim rseq1 > 1 implies seq is not absolutely_summable; theorem :: COMSEQ_3:73 |.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:74 p>1 & (for n st n>=1 holds |.seq.|.n = 1/n to_power p) implies seq is absolutely_summable; theorem :: COMSEQ_3:75 p<=1 & (for n st n>=1 holds |.seq.|.n=1/n to_power p) implies not seq is absolutely_summable; theorem :: COMSEQ_3:76 (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:77 (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;

Back to top