:: Convergence and the Limit of Complex Sequences. Series :: by Yasunari Shidama and Artur Korni{\l}owicz :: :: Received June 25, 1997 :: Copyright (c) 1997-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SEQ_1, COMSEQ_1, SUBSET_1, REAL_1, COMPLEX1, CARD_1, ARYTM_3, RELAT_1, XCMPLX_0, FUNCT_1, SERIES_1, XXREAL_0, ARYTM_1, FUNCOP_1, SEQ_2, VALUED_0, ORDINAL2, NAT_1, PREPOWER, NEWTON, SQUARE_1, VALUED_1, CARD_3, POWER, XXREAL_2, PARTFUN1, TARSKI, FUNCT_7, ASYMPT_1, XREAL_0; notations TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, COMPLEX1, REAL_1, NEWTON, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, VALUED_1, SEQ_1, SEQ_2, NAT_1, VALUED_0, SERIES_1, SQUARE_1, POWER, COMSEQ_1, COMSEQ_2; constructors XREAL_0, PARTFUN1, FUNCT_3, FUNCOP_1, ARYTM_0, REAL_1, SQUARE_1, NAT_1, SEQM_3, COMSEQ_2, NEWTON, SERIES_1, RECDEF_1, SEQ_2, VALUED_1, SEQ_4, RELSET_1, BINOP_2, RVSUM_1, SEQ_1; registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, MEMBERED, COMSEQ_2, NEWTON, VALUED_0, VALUED_1, SEQ_4, SERIES_1, SQUARE_1, SEQ_1, SEQ_2; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions COMSEQ_2, SERIES_1, VALUED_0; equalities SERIES_1, SQUARE_1, VALUED_1; expansions COMSEQ_2, SERIES_1, FUNCT_2; theorems NAT_1, ABSVALUE, SEQ_1, SEQ_2, SERIES_1, SEQM_3, SEQ_4, POWER, COMPLEX1, COMSEQ_2, SQUARE_1, FUNCT_2, XCMPLX_0, XCMPLX_1, FUNCOP_1, XREAL_1, NEWTON, XXREAL_0, ORDINAL1, VALUED_0, VALUED_1, FUNCT_1, RELAT_1, RELSET_1, PARTFUN1; schemes NAT_1, SEQ_1, COMSEQ_1, FUNCT_1; 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; Lm1: 0c = 0+0*; theorem n+1 <> 0c & (n+1)* <> 0c; theorem Th2: (for n holds rseq.n = 0) implies for m holds (Partial_Sums abs( rseq)).m = 0 proof defpred P[Nat] means abs(rseq).$1 = (Partial_Sums abs(rseq)).$1; assume A1: for n holds rseq.n = 0; A2: for k st P[k] holds P[k+1] proof let k be Nat such that A3: P[k]; thus abs(rseq).(k+1) = 0 + abs(rseq).(k+1) .= |.0.| + abs(rseq).(k+1) by ABSVALUE:def 1 .= |.rseq.k.| + abs(rseq).(k+1) by A1 .= (Partial_Sums abs(rseq)).k + abs(rseq).(k+1) by A3,SEQ_1:12 .= (Partial_Sums abs(rseq)).(k+1) by SERIES_1:def 1; end; let m; A4: P[0] by SERIES_1:def 1; for n holds P[n] from NAT_1:sch 2(A4,A2); hence (Partial_Sums abs(rseq)).m = abs(rseq).m .= |.rseq.m.| by SEQ_1:12 .= |.0.| by A1 .= 0 by ABSVALUE:def 1; end; theorem Th3: (for n holds rseq.n = 0) implies rseq is absolutely_summable proof assume A1: for n holds rseq.n = 0; take 0; let p be Real such that A2: 0
convergent for Real_Sequence; coherence by SERIES_1:4; end; registration cluster absolutely_summable -> summable for Real_Sequence; coherence; end; registration cluster absolutely_summable for Real_Sequence; existence by Lm2,Th3; end; theorem rseq is convergent implies for p st 0
Complex_Sequence means :Def1: it.0 = 1r & for n holds it.(n+1) = it.n * z; existence proof reconsider z9 = z as Element of COMPLEX by XCMPLX_0:def 2; deffunc f(set,Element of COMPLEX) = In($2*z9,COMPLEX); consider f being sequence of COMPLEX such that A1: f.0 = 1r & for n being Nat holds f.(n+1) = f(n,f.n) from NAT_1:sch 12; take f; thus f.0 = 1r by A1; let n; f.(n+1) = f(n,f.n) by A1; hence thesis; end; uniqueness proof let seq1,seq2; assume that A2: seq1.0=1r and A3: for n holds seq1.(n+1)=seq1.n * z and A4: seq2.0=1r and A5: for n holds seq2.(n+1)=seq2.n * z; defpred P[Nat] means seq1.$1 = seq2.$1; A6: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume P[k]; hence seq1.(k+1) = seq2.k * z by A3 .= seq2.(k+1) by A5; end; A7: P[0] by A2,A4; for n being Nat holds P[n] from NAT_1:sch 2(A7,A6); hence seq1 = seq2; end; end; definition let z be Complex, n be Nat; redefine func z |^ n -> Element of COMPLEX equals z GeoSeq.n; coherence by XCMPLX_0:def 2; compatibility proof reconsider n as Element of NAT by ORDINAL1:def 12; defpred P[Nat] means z|^$1 = z GeoSeq.$1; let w be Element of COMPLEX; A1: for n being Nat st P[n] holds P[n+1] proof let n be Nat; assume P[n]; hence z|^(n+1) = z GeoSeq.n*z by NEWTON:6 .= z GeoSeq.(n+1) by Def1; end; z|^0 = 1r by COMPLEX1:def 4,NEWTON:4 .= z GeoSeq.0 by Def1; then A2: P[0]; for n being Nat holds P[n] from NAT_1:sch 2(A2,A1); then z|^n = z GeoSeq.n; hence thesis; end; end; theorem z |^ 0 = 1r by COMPLEX1:def 4,NEWTON:4; definition let f be complex-valued Function; set A = dom f; deffunc F(object) = Re(f.$1); func Re f -> Function means :Def3: dom it = dom f & for x be object st x in dom it holds it.x = Re(f.x); existence proof ex f being Function st dom f = A & for x be object st x in A holds f.x = F(x) from FUNCT_1:sch 3; hence thesis; end; uniqueness proof let g,h be Function such that A1: dom g = dom f and A2: for x be object st x in dom g holds g.x = F(x) and A3: dom h = dom f and A4: for x be object st x in dom h holds h.x = F(x); now let x be object; assume A5: x in dom g; hence g.x = F(x) by A2 .= h.x by A1,A3,A4,A5; end; hence thesis by A1,A3,FUNCT_1:2; end; deffunc F(object) = Im(f.$1); func Im f -> Function means :Def4: dom it = dom f & for x be object st x in dom it holds it.x = Im(f.x); existence proof ex f being Function st dom f = A & for x be object st x in A holds f.x = F(x) from FUNCT_1:sch 3; hence thesis; end; uniqueness proof let g,h be Function such that A6: dom g = dom f and A7: for x be object st x in dom g holds g.x = F(x) and A8: dom h = dom f and A9: for x be object st x in dom h holds h.x = F(x); now let x be object; assume A10: x in dom g; hence g.x = F(x) by A7 .= h.x by A6,A8,A9,A10; end; hence thesis by A6,A8,FUNCT_1:2; end; end; registration let f be complex-valued Function; cluster Re f -> real-valued; coherence proof let x be object; assume x in dom Re f; then (Re f).x = Re(f.x) by Def3; hence thesis; end; cluster Im f -> real-valued; coherence proof let x be object; assume x in dom Im f; then (Im f).x = Im(f.x) by Def4; hence thesis; end; end; definition let X be set, f be PartFunc of X,COMPLEX; redefine func Re f -> PartFunc of X,REAL; coherence proof A1: dom f c= X by RELAT_1:def 18; A2: rng Re f c= REAL by VALUED_0:def 3; dom Re f = dom f by Def3; hence thesis by A1,A2,RELSET_1:4; end; redefine func Im f -> PartFunc of X,REAL; coherence proof A3: dom f c= X by RELAT_1:def 18; A4: rng Im f c= REAL by VALUED_0:def 3; dom Im f = dom f by Def4; hence thesis by A3,A4,RELSET_1:4; end; end; definition let c be Complex_Sequence; redefine func Re c -> Real_Sequence means :Def5: for n holds it.n = Re(c.n); coherence proof dom Re c = dom c by Def3 .= NAT by FUNCT_2:def 1; then Re c is total by PARTFUN1:def 2; hence thesis; end; compatibility proof let f be Real_Sequence; A1: dom Re c = dom c by Def3; A2: dom c = NAT by FUNCT_2:def 1; A3: dom f = NAT by FUNCT_2:def 1; thus f = Re c implies for n holds f.n = Re(c.n) by A1,A2,Def3,ORDINAL1:def 12; assume A4: for n holds f.n = Re(c.n); now let x be object; assume A5: x in dom f; hence f.x = Re(c.x) by A4 .= (Re c).x by A1,A2,A3,A5,Def3; end; hence thesis by A1,A2,A3,FUNCT_1:2; end; redefine func Im c -> Real_Sequence means :Def6: for n holds it.n = Im(c.n); coherence proof dom Im c = dom c by Def4 .= NAT by FUNCT_2:def 1; then Im c is total by PARTFUN1:def 2; hence thesis; end; compatibility proof let f be Real_Sequence; A6: dom Im c = dom c by Def4; A7: dom c = NAT by FUNCT_2:def 1; A8: dom f = NAT by FUNCT_2:def 1; thus f = Im c implies for n holds f.n = Im(c.n) by A6,A7,ORDINAL1:def 12,Def4; assume A9: for n holds f.n = Im(c.n); now let x be object; assume A10: x in dom f; hence f.x = Im(c.x) by A9 .= (Im c).x by A6,A7,A8,A10,Def4; end; hence thesis by A6,A7,A8,FUNCT_1:2; end; end; theorem Th12: |.z.| <= |.Re z.| + |.Im z.| proof z = Re z + (Im z)* by COMPLEX1:13; then A1: |.z.| <= |.Re z +0*.| +|.0+(Im z)*.| by COMPLEX1:56; Re(0+(Im z)*)=0 & Im(0+(Im z)*)=Im z by COMPLEX1:12; hence thesis by A1,COMPLEX1:51; end; theorem Th13: |.Re z.| <= |.z.| & |.Im z.| <= |.z.| proof 0 <= (Re z)^2 by XREAL_1:63; then A1: 0+(Im z)^2 <= (Re z)^2 + (Im z)^2 by XREAL_1:6; 0 <= (Im z)^2 by XREAL_1:63; then A2: sqrt((Im z)^2) <= sqrt((Re z)^2 + (Im z)^2) by A1,SQUARE_1:26; 0 <= (Im z)^2 by XREAL_1:63; then A3: 0+(Re z)^2 <= (Im z)^2 + (Re z)^2 by XREAL_1:6; 0 <= (Re z)^2 by XREAL_1:63; then |.z.| = sqrt ((Re z)^2 + (Im z)^2) & sqrt((Re z)^2) <= sqrt((Re z)^2 + (Im z )^2) by A3,COMPLEX1:def 12,SQUARE_1:26; hence thesis by A2,COMPLEX1:72; end; theorem Th14: Re seq1=Re seq2 & Im seq1=Im seq2 implies seq1=seq2 proof assume that A1: Re seq1=Re seq2 and A2: Im seq1=Im seq2; now let n be Element of NAT; A3: Im(seq1.n)=Im seq2.n by A2,Def6 .=Im(seq2.n) by Def6; Re(seq1.n)=Re seq2.n by A1,Def5 .=Re(seq2.n) by Def5; hence seq1.n=seq2.n by A3,COMPLEX1:3; end; hence thesis; end; theorem Th15: Re seq1 + Re seq2 = Re (seq1+seq2) & Im seq1 + Im seq2 = Im ( seq1+seq2 qua Complex_Sequence) proof now let n be Element of NAT; thus (Re seq1+Re seq2).n=Re seq1.n+Re seq2.n by SEQ_1:7 .=Re(seq1.n)+Re seq2.n by Def5 .=Re(seq1.n)+Re(seq2.n) by Def5 .=Re(seq1.n+seq2.n) by COMPLEX1:8 .=Re((seq1+seq2).n) by VALUED_1:1 .=Re (seq1+seq2).n by Def5; end; hence Re seq1+Re seq2=Re (seq1+seq2); now let n be Element of NAT; thus (Im seq1+Im seq2).n=Im seq1.n+Im seq2.n by SEQ_1:7 .=Im(seq1.n)+Im seq2.n by Def6 .=Im(seq1.n)+Im(seq2.n) by Def6 .=Im(seq1.n+seq2.n) by COMPLEX1:8 .=Im((seq1+seq2).n) by VALUED_1:1 .=Im (seq1+seq2).n by Def6; end; hence thesis; end; theorem Th16: -(Re seq) = Re (-seq) & -(Im seq) = Im -seq proof now let n be Element of NAT; thus (-Re seq).n= -(Re seq.n) by SEQ_1:10 .=-Re(seq.n) by Def5 .= Re(-(seq.n)) by COMPLEX1:17 .= Re((-seq).n) by VALUED_1:8 .=Re (-seq).n by Def5; end; hence -Re seq=Re (-seq); now let n be Element of NAT; thus (-Im seq).n=-Im seq.n by SEQ_1:10 .=-Im(seq.n) by Def6 .= Im(-(seq.n)) by COMPLEX1:17 .= Im((-seq).n) by VALUED_1:8 .=(Im -seq).n by Def6; end; hence thesis; end; theorem Th17: r*Re(z)=Re(r*z) & r*Im(z)=Im(r*z) proof reconsider r9 = r as Element of COMPLEX by XCMPLX_0:def 2; r = r +0*; then A1: Re r = r & Im r = 0 by COMPLEX1:12; r*z = Re r9 * Re z - Im r9 * Im z + (Re r9 * Im z + Re z * Im r9)* by COMPLEX1:82 .= r * Re z+(r * Im z)* by A1; hence thesis by COMPLEX1:12; end; theorem Th18: Re seq1-Re seq2=Re (seq1-seq2) & Im seq1-Im seq2=Im(seq1-seq2) proof now let n be Element of NAT; thus (Re seq1-Re seq2).n = Re seq1.n+(-Re seq2).n by SEQ_1:7 .=Re seq1.n+(Re -seq2).n by Th16 .=(Re seq1+Re -seq2).n by SEQ_1:7 .=Re (seq1-seq2).n by Th15; end; hence Re seq1-Re seq2=Re (seq1-seq2); now let n be Element of NAT; thus (Im seq1-Im seq2).n = Im seq1.n+(-Im seq2).n by SEQ_1:7 .=Im seq1.n+Im (-seq2).n by Th16 .=(Im seq1+Im -seq2).n by SEQ_1:7 .=Im(seq1-seq2).n by Th15; end; hence thesis; end; theorem r(#)Re seq = Re (r (#) seq) & r(#)Im seq = Im (r (#) seq) proof now let n be Element of NAT; thus (r(#)Re seq).n= r*(Re seq.n) by SEQ_1:9 .=r*Re(seq.n) by Def5 .=Re(r*(seq.n)) by Th17 .=Re((r (#) seq).n) by VALUED_1:6 .=Re (r (#) seq).n by Def5; end; hence r(#)Re seq=Re (r (#) seq); now let n be Element of NAT; thus (r(#)Im seq).n= r*(Im seq.n) by SEQ_1:9 .=r*Im(seq.n) by Def6 .=Im(r*(seq.n)) by Th17 .=Im((r(#) seq).n) by VALUED_1:6 .=Im(r(#)seq).n by Def6; end; hence thesis; end; theorem Re (z (#) seq) = Re z (#) Re seq - Im z (#) Im seq & Im (z (#) seq) = Re z (#) Im seq + Im z (#) Re seq proof now let n be Element of NAT; thus Re (z (#) seq).n=Re((z (#) seq).n) by Def5 .= Re((z * seq.n )) by VALUED_1:6 .= Re(Re(z) * Re(seq.n) - Im(z) * Im(seq.n)+ (Re(z) * Im(seq.n) + Re( seq.n) * Im(z))*) by COMPLEX1:82 .= Re(z) * Re(seq.n) - Im(z) * Im(seq.n) by COMPLEX1:12 .= Re(z) *( Re seq.n) - Im(z) * Im(seq.n) by Def5 .= Re(z) *( Re seq.n) - Im(z) *( Im seq.n) by Def6 .= (Re(z) (#) Re seq).n - Im(z) *( Im seq.n) by SEQ_1:9 .= (Re(z) (#) Re seq).n - (Im(z) (#) Im seq).n by SEQ_1:9 .= (Re(z) (#) Re seq).n + (- (Im(z) (#) Im seq).n) .= (Re(z) (#) Re seq).n + (- Im(z) (#) Im seq).n by SEQ_1:10 .= (Re(z) (#) Re seq - Im(z) (#) Im seq).n by SEQ_1:7; end; hence Re (z (#) seq)=Re(z)(#)Re seq-Im(z)(#)Im seq; now let n be Element of NAT; thus Im(z(#)seq).n =Im((z (#) seq).n) by Def6 .=Im((z * seq.n )) by VALUED_1:6 .=Im(Re(z) * Re(seq.n) - Im(z) * Im(seq.n)+ (Re(z) * Im(seq.n) + Re( seq.n) * Im(z))*) by COMPLEX1:82 .= Re(z) * Im(seq.n) + Re(seq.n) * Im(z) by COMPLEX1:12 .= Re(z) * Im(seq.n) + Im(z) * Re seq.n by Def5 .= Re(z) * Im seq.n + Im(z) *(Re seq.n) by Def6 .= (Re(z) (#) Im seq).n + Im(z) *(Re seq.n) by SEQ_1:9 .= (Re(z) (#) Im seq).n + (Im(z) (#) Re seq).n by SEQ_1:9 .= (Re(z) (#) Im seq + Im(z) (#) Re seq).n by SEQ_1:7; end; hence thesis; end; theorem Re (seq1 (#) seq2) = Re seq1(#)Re seq2-Im seq1(#)Im seq2 & Im (seq1 (#) seq2) = Re seq1(#)Im seq2+Im seq1(#)Re seq2 proof now let n be Element of NAT; thus Re (seq1 (#) seq2).n=Re((seq1 (#) seq2).n) by Def5 .=Re((seq1.n * seq2.n )) by VALUED_1:5 .=Re(Re(seq1.n) * Re(seq2.n) - Im(seq1.n) * Im(seq2.n)+ (Re(seq1.n) * Im(seq2.n) + Re(seq2.n) * Im(seq1.n))*) by COMPLEX1:82 .= Re(seq1.n) * Re(seq2.n) - Im(seq1.n) * Im(seq2.n) by COMPLEX1:12 .= (Re seq1.n) * Re(seq2.n) - Im(seq1.n) * Im(seq2.n) by Def5 .= (Re seq1.n) *( Re seq2.n) - Im(seq1.n) * Im(seq2.n) by Def5 .= (Re seq1.n) *( Re seq2.n) - Im(seq1.n) *( Im seq2.n) by Def6 .= (Re seq1.n) *( Re seq2.n) - (Im seq1.n)*( Im seq2.n) by Def6 .= (Re seq1 (#) Re seq2).n - (Im seq1.n) *( Im seq2.n) by SEQ_1:8 .= (Re seq1 (#) Re seq2).n - (Im seq1 (#) Im seq2).n by SEQ_1:8 .= (Re seq1 (#)Re seq2).n + (- (Im seq1 (#) Im seq2).n) .= (Re seq1 (#) Re seq2).n + (- Im seq1 (#) Im seq2).n by SEQ_1:10 .= (Re seq1 (#) Re seq2 - Im seq1 (#) Im seq2).n by SEQ_1:7; end; hence Re (seq1 (#) seq2)=Re seq1(#)Re seq2-Im seq1(#)Im seq2; now let n be Element of NAT; thus Im (seq1 (#) seq2).n =Im((seq1 (#) seq2).n) by Def6 .=Im((seq1.n * seq2.n )) by VALUED_1:5 .=Im(Re(seq1.n) * Re(seq2.n) - Im(seq1.n) * Im(seq2.n)+ (Re(seq1.n) * Im(seq2.n) + Re(seq2.n) * Im(seq1.n))*) by COMPLEX1:82 .= Re(seq1.n) * Im(seq2.n) + Re(seq2.n) * Im(seq1.n) by COMPLEX1:12 .= Re(seq1.n) * Im(seq2.n) + Im(seq1.n) * Re seq2.n by Def5 .= Re seq1.n * Im(seq2.n) + Im(seq1.n) * Re seq2.n by Def5 .= Re seq1.n * Im seq2.n + Im(seq1.n) * Re seq2.n by Def6 .= (Re seq1.n * Im seq2.n) + (Im seq1.n * Re seq2.n) by Def6 .= (Re seq1 (#) Im seq2).n + Im seq1.n *( Re seq2.n) by SEQ_1:8 .= (Re seq1 (#) Im seq2).n + (Im seq1 (#) Re seq2).n by SEQ_1:8 .= (Re seq1 (#) Im seq2 + Im seq1 (#) Re seq2).n by SEQ_1:7; end; hence thesis; end; definition let Nseq be increasing sequence of NAT, seq be Complex_Sequence; redefine func seq * Nseq -> Complex_Sequence; coherence proof dom (seq*Nseq)=NAT by FUNCT_2:def 1; hence thesis; end; end; theorem Th22: Re (seq*Nseq)=(Re seq)*Nseq & Im (seq*Nseq)=(Im seq)*Nseq proof now let n be Element of NAT; thus (Re (seq*Nseq)).n =Re((seq*Nseq).n) by Def5 .=Re(seq.(Nseq.n)) by FUNCT_2:15 .=Re seq.(Nseq.n) by Def5 .=(Re seq*Nseq).n by FUNCT_2:15; end; hence Re (seq*Nseq)=Re seq*Nseq; now let n be Element of NAT; thus Im (seq*Nseq).n =Im((seq*Nseq).n) by Def6 .=Im(seq.(Nseq.n)) by FUNCT_2:15 .=Im seq.(Nseq.n) by Def6 .=(Im seq*Nseq).n by FUNCT_2:15; end; hence thesis; end; theorem Th23: (Re seq)^\k =Re (seq^\k) & (Im seq)^\k =Im (seq^\k) proof now let n be Element of NAT; thus (Re seq^\k).n =Re seq.(n+k) by NAT_1:def 3 .=Re(seq.(n+k)) by Def5 .=Re((seq^\k).n) by NAT_1:def 3 .=Re ((seq)^\k).n by Def5; thus (Im seq^\k).n =Im seq.(n+k) by NAT_1:def 3 .=Im(seq.(n+k)) by Def6 .=Im((seq^\k).n) by NAT_1:def 3 .=Im ((seq)^\k).n by Def6; end; hence thesis; end; definition let s be Complex_Sequence; redefine func Partial_Sums s -> Complex_Sequence; coherence proof A1: dom Partial_Sums s = NAT by PARTFUN1:def 2; rng Partial_Sums s c= COMPLEX by VALUED_0:def 1; then Partial_Sums s is PartFunc of NAT, COMPLEX by A1,RELSET_1:4; hence Partial_Sums s is Complex_Sequence; end; end; definition let seq be Complex_Sequence; func Sum seq -> Element of COMPLEX equals lim Partial_Sums seq; coherence by XCMPLX_0:def 2; end; theorem Th24: (for n holds seq.n = 0c) implies for m holds (Partial_Sums seq). m = 0c proof defpred P[Nat] means seq.$1 = (Partial_Sums seq).$1; assume A1: for n holds seq.n = 0c; A2: for k being Nat st P[k] holds P[k+1] proof let k be Nat such that A3: P[k]; thus seq.(k+1) = 0c + seq.(k+1) .= (Partial_Sums seq).k + seq.(k+1) by A1,A3 .= (Partial_Sums seq).(k+1) by SERIES_1:def 1; end; let m; A4: P[0] by SERIES_1:def 1; for n being Nat holds P[n] from NAT_1:sch 2(A4,A2); then seq = Partial_Sums seq; hence thesis by A1; end; theorem Th25: (for n holds seq.n = 0c) implies for m holds (Partial_Sums |.seq .|).m = 0 proof defpred P[Nat] means |.seq.|.$1 = (Partial_Sums |.seq.|).$1; assume A1: for n holds seq.n = 0c; A2: for k being Nat st P[k] holds P[k+1] proof let k be Nat such that A3: P[k]; thus |.seq.|.(k+1) = |.0c.| + |.seq.|.(k+1) by COMPLEX1:44 .= |.seq.k.| + |.seq.|.(k+1) by A1 .= (Partial_Sums |.seq.|).k + |.seq.|.(k+1) by A3,VALUED_1:18 .= (Partial_Sums |.seq.|).(k+1) by SERIES_1:def 1; end; let m; A4: P[0] by SERIES_1:def 1; for n being Nat holds P[n] from NAT_1:sch 2(A4,A2); hence (Partial_Sums |.seq.|).m = |.seq.|.m .= |.seq.m.| by VALUED_1:18 .= 0 by A1,COMPLEX1:44; end; theorem Th26: Partial_Sums Re seq = Re (Partial_Sums seq) & Partial_Sums Im seq = Im (Partial_Sums seq) proof defpred P[Nat] means Partial_Sums(Re seq).$1 = Re Partial_Sums( seq).$1; defpred R[Nat] means Partial_Sums(Im seq).$1 = Im Partial_Sums(seq).$1; A1: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume P[k]; then Partial_Sums(Re seq).(k+1) =Re Partial_Sums(seq).k + Re seq.(k+1) by SERIES_1:def 1 .=Re Partial_Sums(seq).k +Re(seq.(k+1)) by Def5 .=Re(Partial_Sums(seq).k) +Re(seq.(k+1)) by Def5 .=Re(Partial_Sums(seq).k + seq.(k+1)) by COMPLEX1:8 .=Re(Partial_Sums(seq).(k+1)) by SERIES_1:def 1 .=Re Partial_Sums(seq).(k+1) by Def5; hence thesis; end; A2: for k be Nat st R[k] holds R[k+1] proof let k be Nat; assume R[k]; then Partial_Sums(Im seq).(k+1) = Im Partial_Sums(seq).k + Im seq.(k+1) by SERIES_1:def 1 .=Im Partial_Sums(seq).k +Im(seq.(k+1)) by Def6 .=Im(Partial_Sums(seq).k) +Im(seq.(k+1)) by Def6 .=Im(Partial_Sums(seq).k + seq.(k+1)) by COMPLEX1:8 .=Im(Partial_Sums(seq).(k+1)) by SERIES_1:def 1 .=Im Partial_Sums(seq).(k+1) by Def6; hence thesis; end; Partial_Sums(Im seq).0 = Im seq.0 by SERIES_1:def 1 .= Im(seq.0) by Def6 .= Im(Partial_Sums(seq).0) by SERIES_1:def 1 .= Im Partial_Sums(seq).0 by Def6; then A3: R[0]; A4: for n being Nat holds R[n] from NAT_1:sch 2(A3,A2); Partial_Sums(Re seq).0 = Re seq.0 by SERIES_1:def 1 .= Re(seq.0) by Def5 .= Re(Partial_Sums(seq).0) by SERIES_1:def 1 .= Re Partial_Sums(seq).0 by Def5; then A5: P[0]; for n being Nat holds P[n] from NAT_1:sch 2(A5,A1); hence thesis by A4; end; theorem Th27: Partial_Sums(seq1)+Partial_Sums(seq2) = Partial_Sums(seq1+seq2) by SERIES_1:5; theorem Th28: Partial_Sums(seq1)-Partial_Sums(seq2) = Partial_Sums(seq1-seq2) proof A1: Im(Partial_Sums(seq1)-Partial_Sums(seq2)) =Im Partial_Sums(seq1)-Im Partial_Sums(seq2) by Th18 .=Partial_Sums Im seq1-Im Partial_Sums(seq2) by Th26 .=Partial_Sums Im seq1-Partial_Sums Im seq2 by Th26 .=Partial_Sums(Im seq1-Im seq2) by SERIES_1:6 .=Partial_Sums(Im (seq1-seq2)) by Th18 .=Im Partial_Sums(seq1-seq2) by Th26; Re (Partial_Sums(seq1)-Partial_Sums(seq2)) =Re Partial_Sums(seq1)-Re Partial_Sums(seq2) by Th18 .=Partial_Sums Re seq1-Re Partial_Sums(seq2) by Th26 .=Partial_Sums Re seq1-Partial_Sums Re seq2 by Th26 .=Partial_Sums(Re seq1-Re seq2) by SERIES_1:6 .=Partial_Sums(Re (seq1-seq2)) by Th18 .=Re Partial_Sums(seq1-seq2) by Th26; hence thesis by A1,Th14; end; theorem Th29: for z being Complex holds Partial_Sums(z (#) seq) = z (#) Partial_Sums(seq) proof let z be Complex; defpred P[Nat] means Partial_Sums(z (#) seq).$1= (z (#) Partial_Sums(seq)).$1; A1: now let n be Nat; assume A2: P[n]; Partial_Sums(z (#) seq).(n+1) =Partial_Sums(z (#) seq).n + (z (#) seq) .(n+1) by SERIES_1:def 1 .=(z * Partial_Sums(seq).n )+ (z (#) seq).(n+1) by A2,VALUED_1:6 .=(z * Partial_Sums(seq).n )+ (z * seq.(n+1)) by VALUED_1:6 .= z * ( Partial_Sums(seq).n + seq.(n+1)) .= z * ( Partial_Sums(seq).(n+1)) by SERIES_1:def 1 .= (z (#) Partial_Sums(seq)).(n+1) by VALUED_1:6; hence P[n+1]; end; Partial_Sums(z(#)seq).0=(z (#) seq).0 by SERIES_1:def 1 .=z * seq.0 by VALUED_1:6 .=z * Partial_Sums(seq).0 by SERIES_1:def 1 .=(z (#) Partial_Sums(seq)).0 by VALUED_1:6; then A3: P[0]; for n being Nat holds P[n] from NAT_1:sch 2(A3,A1); hence thesis; end; theorem |.Partial_Sums(seq).k.| <= (Partial_Sums |.seq.|).k proof defpred P[Nat] means |. Partial_Sums(seq).$1 .| <= Partial_Sums(|.seq.|).$1; A1: now let k; assume P[k]; then A2: |. Partial_Sums(seq).k.| + |.(seq).(k+1).| <= Partial_Sums(|.seq.| ).k + |.(seq).(k+1).| by XREAL_1:6; |. Partial_Sums(seq).(k+1) .| =|. Partial_Sums(seq).k + (seq).(k+1) .| & |. Partial_Sums(seq).k + (seq).(k+1) .| <= |. Partial_Sums(seq).k.| + |. (seq ).(k+ 1) .| by COMPLEX1:56,SERIES_1:def 1; then |. Partial_Sums(seq).(k+1) .| <= Partial_Sums(|.seq.|).k + |.seq.(k+1) .| by A2,XXREAL_0:2; then |. Partial_Sums(seq).(k+1) .| <= Partial_Sums(|.seq.|).k+|.seq.|.(k+1) by VALUED_1:18; hence P[k+1] by SERIES_1:def 1; end; Partial_Sums(|.seq.|).0 = (|.seq.|).0 by SERIES_1:def 1 .= |. seq.0 .| by VALUED_1:18; then A3: P[0] by SERIES_1:def 1; for k being Nat holds P[k] from NAT_1:sch 2(A3,A1); hence thesis; end; theorem Th31: |.Partial_Sums(seq).m- Partial_Sums(seq).n.| <= |. Partial_Sums(|.seq.|).m- Partial_Sums(|.seq.|).n.| proof A1: for n,k be Nat holds 0 <= Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n proof let n; defpred P[Nat] means 0 <= Partial_Sums(|.seq.|).(n+$1)- Partial_Sums(|.seq.|).n; A2: now let k; A3: Partial_Sums(|.seq.|).(n+(k+1))- Partial_Sums(|.seq.|).n = Partial_Sums(|.seq.|).(n+k)+|.seq.|.(n+k+1) - Partial_Sums(|.seq.|).n by SERIES_1:def 1 .=Partial_Sums(|.seq.|).(n+k)+|.seq.(n+k+1).| - Partial_Sums(|.seq.| ).n by VALUED_1:18 .=Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n +|.seq.(n+k+1 ).|; A4: 0 <= |.seq.(n+k+1).| by COMPLEX1:46; assume P[k]; hence P[k+1] by A3,A4; end; A5: P[0]; thus for k be Nat holds P[k] from NAT_1:sch 2(A5,A2); end; A6: for n,k be Nat holds |. Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n.| = Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n by A1,ABSVALUE:def 1; A7: for n,m st n <= m holds |.Partial_Sums(seq).m- Partial_Sums(seq).n .| <= |. Partial_Sums(|.seq.|).m- Partial_Sums(|.seq.|).n.| proof let n,m be Nat; assume n <= m; then consider k be Nat such that A8: m=n+k by NAT_1:10; A9: for k be Nat holds |.Partial_Sums(seq).(n+k)- Partial_Sums (seq).n.| <= |. Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n.| proof defpred P[Nat] means |.Partial_Sums(seq).(n+$1)- Partial_Sums (seq).n.| <= |. Partial_Sums(|.seq.|).(n+$1)- Partial_Sums(|.seq.|).n.|; A10: now let k be Nat; assume P[k]; then A11: |.Partial_Sums(seq).(n+k)- Partial_Sums(seq).n+seq.(n+k+1).| <= |. Partial_Sums(seq).(n+k)- Partial_Sums(seq).n.| +|.seq.(n+k+1).| & |. Partial_Sums(seq).(n+k)- Partial_Sums(seq).n.| +|.seq.(n+k+1).| <= |. Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n .| +|.seq.(n+k+1).| by COMPLEX1:56,XREAL_1:6; A12: |.Partial_Sums(seq).(n+(k+1))- Partial_Sums(seq).n .| =|.( Partial_Sums(seq).(n+k)+seq.(n+k+1))- Partial_Sums(seq).n.| by SERIES_1:def 1 .=|.Partial_Sums(seq).(n+k)- Partial_Sums(seq).n+seq.(n+k+1).|; |. Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n .| +|. seq.(n+k+1).| =Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n +|.seq.(n+k +1).| by A6 .=Partial_Sums(|.seq.|).(n+k)+|.seq.(n+k+1).| - Partial_Sums(|.seq .|).n .=Partial_Sums(|.seq.|).(n+k)+|.seq.|.(n+k+1) - Partial_Sums(|.seq .|).n by VALUED_1:18 .=Partial_Sums(|.seq.|).(n+(k+1))- Partial_Sums(|.seq.|).n by SERIES_1:def 1 .=|. Partial_Sums(|.seq.|).(n+(k+1))- Partial_Sums(|.seq.|).n .| by A6; hence P[k+1] by A12,A11,XXREAL_0:2; end; A13: P[0]; thus for k be Nat holds P[k] from NAT_1:sch 2(A13,A10 ); end; thus thesis by A9,A8; end; for n, m holds |.Partial_Sums(seq).m- Partial_Sums(seq).n.| <= |. Partial_Sums(|.seq.|).m- Partial_Sums(|.seq.|).n .| proof let n,m; m <= n implies |.Partial_Sums(seq).m- Partial_Sums(seq).n.| <= |. Partial_Sums(|.seq.|).m- Partial_Sums(|.seq.|).n .| proof assume m <= n; then A14: |.Partial_Sums(seq).n- Partial_Sums(seq).m.| <= |. Partial_Sums( |.seq.|).n- Partial_Sums(|.seq.|).m .| by A7; |. Partial_Sums(|.seq.|).n- Partial_Sums(|.seq.|).m .| =|.-( Partial_Sums(|.seq.|).n- Partial_Sums(|.seq.|).m) .| by COMPLEX1:52 .=|. Partial_Sums(|.seq.|).m- Partial_Sums(|.seq.|).n .|; hence thesis by A14,COMPLEX1:60; end; hence thesis by A7; end; hence thesis; end; theorem Th32: Partial_Sums(Re seq)^\k =Re (Partial_Sums(seq)^\k) & Partial_Sums(Im seq)^\k =Im (Partial_Sums(seq)^\k) proof now let n be Element of NAT; thus (Partial_Sums(Re seq)^\k).n =Partial_Sums(Re seq).(n+k) by NAT_1:def 3 .=Re Partial_Sums(seq).(n+k) by Th26 .=Re(Partial_Sums(seq).(n+k)) by Def5 .=Re((Partial_Sums(seq)^\k).n) by NAT_1:def 3 .=(Re (Partial_Sums(seq)^\k)).n by Def5; thus (Partial_Sums(Im seq)^\k).n =Partial_Sums(Im seq).(n+k) by NAT_1:def 3 .=Im Partial_Sums(seq).(n+k) by Th26 .=Im(Partial_Sums(seq).(n+k)) by Def6 .=Im((Partial_Sums(seq)^\k).n) by NAT_1:def 3 .=Im (Partial_Sums(seq)^\k).n by Def6; end; hence thesis; end; theorem (for n holds seq1.n=seq.0) implies Partial_Sums(seq^\1) = ( Partial_Sums(seq)^\1) - seq1 proof assume A1: for n holds seq1.n=seq.0; A2: now let n; thus Re seq1.n=Re(seq1.n) by Def5 .=Re(seq.0) by A1 .=Re seq.0 by Def5; thus Im seq1.n=Im(seq1.n) by Def6 .=Im(seq.0) by A1 .=Im seq.0 by Def6; end; A3: Im Partial_Sums(seq^\1)=Partial_Sums(Im (seq^\1)) by Th26 .=Partial_Sums(Im seq^\1) by Th23 .= (Partial_Sums(Im seq)^\1) - Im seq1 by A2,SERIES_1:11 .=Im (Partial_Sums(seq)^\1)-Im seq1 by Th32 .=Im (Partial_Sums(seq)^\1-seq1) by Th18; Re Partial_Sums(seq^\1)=Partial_Sums(Re (seq^\1)) by Th26 .=Partial_Sums(Re seq^\1) by Th23 .= (Partial_Sums(Re seq)^\1) - Re seq1 by A2,SERIES_1:11 .=Re (Partial_Sums(seq)^\1)-Re seq1 by Th32 .=Re (Partial_Sums(seq)^\1-seq1) by Th18; hence thesis by A3,Th14; end; theorem Th34: Partial_Sums |.seq.| is non-decreasing proof for n holds 0 <= |.seq.|.n by Lm3; hence thesis by SERIES_1:16; end; registration let seq be Complex_Sequence; cluster Partial_Sums |.seq.| -> non-decreasing for Real_Sequence; coherence by Th34; end; theorem (for n st n <= m holds seq1.n = seq2.n) implies Partial_Sums(seq1).m = Partial_Sums(seq2).m proof defpred P[Nat] means $1 <= m implies Partial_Sums(seq1).$1= Partial_Sums(seq2).$1; assume A1: for n st n <= m holds seq1.n = seq2.n; A2: for k be Nat st P[k] holds P[k+1] proof let k be Nat such that A3: P[k]; assume A4: k+1 <= m; k < k+1 by XREAL_1:29; hence Partial_Sums(seq1).(k+1) =Partial_Sums(seq2).k+seq1.(k+1) by A3,A4, SERIES_1:def 1,XXREAL_0:2 .=Partial_Sums(seq2).k+seq2.(k+1) by A1,A4 .=Partial_Sums(seq2).(k+1) by SERIES_1:def 1; end; A5: P[0] proof assume 0 <= m; thus Partial_Sums(seq1).0=seq1.0 by SERIES_1:def 1 .=seq2.0 by A1 .=Partial_Sums(seq2).0 by SERIES_1:def 1; end; for k holds P[k] from NAT_1:sch 2(A5,A2); hence thesis; end; theorem Th36: 1r <> z implies for n holds Partial_Sums(z GeoSeq).n = (1r - z |^ (n+1))/(1r-z) proof now let z; defpred P[Nat] means Partial_Sums(z GeoSeq).$1 = (1r - z |^ ($1+1))/(1r-z); assume 1r <> z; then A1: 1r-z <>0c; A2: for n st P[n] holds P[n+1] proof let n; assume P[n]; hence Partial_Sums(z GeoSeq).(n+1) = (1r - z |^ (n+1))/(1r-z)+ z |^ (n+1) * 1r by COMPLEX1:def 4,SERIES_1:def 1 .= (1r - z |^ (n+1))/(1r-z)+ z |^ (n+1) * ((1r-z)/(1r-z)) by A1, COMPLEX1:def 4,XCMPLX_1:60 .= (1r - z |^ (n+1))/(1r-z)+ (z |^ (n+1) * (1r-z))/(1r-z) by XCMPLX_1:74 .= (1r - z |^ (n+1) + (z |^ (n+1) -z |^(n+1) * z ))/(1r-z) by COMPLEX1:def 4,XCMPLX_1:62 .= (1r - z |^(n+1) * z )/(1r-z) .= (1r - z |^ ((n+1) +1) )/(1r-z) by NEWTON:6; end; Partial_Sums(z GeoSeq).0 =(z GeoSeq).0 by SERIES_1:def 1 .=1r by Def1 .=(1r -1 * z )/(1r-z) by A1,COMPLEX1:def 4,XCMPLX_1:60 .=(1r-z |^ (0+1) )/(1r-z); then A3: P[0]; thus for n holds P[n] from NAT_1:sch 2(A3,A2); end; hence thesis; end; theorem Th37: 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)) proof assume that A1: z <> 1r and A2: for n holds seq.(n+1) = z * seq.n; defpred P[Nat] means seq.$1=seq.0 * (z GeoSeq).$1; A3: now let n be Nat; assume P[n]; then seq.(n+1)=z * (seq.0 * (z GeoSeq).n) by A2 .=seq.0 * (z * (z GeoSeq).n) .=seq.0 * (z GeoSeq).(n+1) by Def1; hence P[n+1]; end; let n; seq.0 = seq.0 * 1r by COMPLEX1:def 4 .= seq.0 * (z GeoSeq).0 by Def1; then A4: P[0]; for n being Nat holds P[n] from NAT_1:sch 2(A4,A3); then for n being Element of NAT holds P[n]; then Partial_Sums(seq)=Partial_Sums(seq.0 (#) (z GeoSeq)) by VALUED_1:7 .=seq.0 (#) Partial_Sums(z GeoSeq) by Th29; hence Partial_Sums(seq).n=seq.0 * Partial_Sums(z GeoSeq).n by VALUED_1:6 .=seq.0 * ( (1r - z |^ (n+1))/(1r -z) ) by A1,Th36; end; begin :: Convergence of Complex Sequences theorem Th38: 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 proof let a, b be Real_Sequence, c be Complex_Sequence such that A1: for n holds Re(c.n) = a.n & Im(c.n) = b.n; thus a is convergent & b is convergent implies c is convergent proof assume that A2: a is convergent and A3: b is convergent; consider a1 being Real such that A4: for p being Real st 0
as Element of COMPLEX by XCMPLX_0:def 2; take g; for p st 0
0; consider n such that A21: for m st n <= m holds |.c.m-z.| < p by A16,A20; take n; let m; assume n <= m; then A22: |.c.m-z.| < p by A21; A23: Im(c.m-z)=Im(c.m)-Im(z) by COMPLEX1:19; Im(c.m) =b.m by A1; then |.b.m-Im(z) .| <= |.c.m-z.| by A23,Th13; hence thesis by A22,XXREAL_0:2; end; theorem Th39: 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)* proof let a, b be convergent Real_Sequence, c be Complex_Sequence; reconsider g=lim(a)+lim(b)* as Element of COMPLEX by XCMPLX_0:def 2; assume A1: for n holds Re(c.n) = a.n & Im(c.n) = b.n; hence A2: c is convergent by Th38; for p being Real st 0
0; consider n such that A4: for m st n <= m holds |.c.m-lim(c).| < p by A3,COMSEQ_2:def 6; take n; let m; assume n <= m; then A5: |.c.m-lim(c).| < p by A4; Im(c.m) =b.m & Im(c.m-lim(c))=Im(c.m)-Im(lim(c)) by A1,COMPLEX1:19; then |.b.m-Im(lim(c)) .| <= |.c.m-lim(c).| by Th13; hence thesis by A5,XXREAL_0:2; end; A6: for p being Real st 0
convergent for Real_Sequence; coherence by Th41; cluster Im c -> convergent for Real_Sequence; coherence by Th41; end; theorem Th42: 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) proof let c be Complex_Sequence; assume A1: Re c is convergent & Im c is convergent; A2: ( for n holds Re c.n=Re(c.n))& for n holds Im c.n=Im(c.n) by Def5,Def6; then lim(c) = lim(Re c)+(lim(Im c))* by A1,Th39; hence thesis by A1,A2,Th39,COMPLEX1:12; end; theorem Th43: (0 < |.z.| & |.z.| < 1 & seq.0 = z & for n holds seq.(n+1) = seq .n * z) implies seq is convergent & lim(seq)=0c proof assume that A1: 0 < |.z.| and A2: |.z.| < 1; deffunc g(Nat) = |.z.| to_power ($1+1); consider rseq1 such that A3: for n holds rseq1.n=g(n) from SEQ_1:sch 1; assume that A4: seq.0 = z and A5: for n holds seq.(n+1) = seq.n * z; A6: for n holds |.seq.n.| = |.z.| to_power (n+1) proof defpred P[Nat] means |. seq.$1 .|= |.z.| to_power ($1+1); A7: for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume A8: P[k]; |.seq.(k+1).| = |.seq.k * z.| by A5 .= |.z.| to_power (k+1) * |.z.| by A8,COMPLEX1:65 .= |.z.| to_power (k+1) * |.z.| to_power 1 by POWER:25 .= |.z.| to_power ((k+1)+1) by A1,POWER:27; hence thesis; end; A9: P[0] by A4,POWER:25; for n holds P[n] from NAT_1:sch 2(A9,A7); hence thesis; end; A10: now let n; abs(Re seq).n = |.Re seq.n.| by SEQ_1:12; then A11: abs(Re seq).n = |.Re(seq.n).| by Def5; |.Re(seq.n).| <= |.seq.n.| & |.seq.n.| = |.z.| to_power (n+1) by A6,Th13; hence abs(Re seq).n <= rseq1.n by A3,A11; end; A12: now let n; A13: |.seq.n.| = |.z.| to_power (n+1) by A6; abs(Im seq).n = |.Im seq.n.| & |.Im(seq.n).| <= |.seq.n.| by Th13, SEQ_1:12; then abs(Im seq).n <= |.z.| to_power (n+1) by A13,Def6; hence abs(Im seq).n <= rseq1.n by A3; end; C.0=0; then A14: lim(C)=0 by SEQ_4:25; A15: rseq1 is convergent & lim(rseq1)=0 by A1,A2,A3,SERIES_1:1; now let n; abs(Re seq).n=|.Re seq.n.| by SEQ_1:12; then 0 <= abs(Re seq).n by COMPLEX1:46; hence C.n <= abs(Re seq).n; end; then A16: abs(Re seq) is convergent & lim(abs(Re seq))=0 by A14,A15,A10,SEQ_2:19,20; then A17: Re seq is convergent by SEQ_4:15; now let n; abs(Im seq).n=|.Im seq.n.| by SEQ_1:12; then 0 <= abs(Im seq).n by COMPLEX1:46; hence C.n <= abs(Im seq).n; end; then A18: abs(Im seq) is convergent & lim(abs(Im seq))=0 by A14,A15,A12,SEQ_2:19,20; then A19: Im seq is convergent by SEQ_4:15; lim(Im seq)=0 by A18,SEQ_4:15; then A20: Im lim(seq)=0 by A17,A19,Th42; lim(Re seq)=0 by A16,SEQ_4:15; then Re lim(seq)=0 by A17,A19,Th42; hence thesis by A17,A19,A20,Lm1,Th42,COMPLEX1:13; end; theorem Th44: |.z.| < 1 & (for n holds seq.n=z |^ (n+1)) implies seq is convergent & lim(seq)=0c proof assume that A1: |.z.| <1 and A2: for n holds seq.n=z |^ (n+1); A3: now let n; thus seq.(n+1) = z |^ ((n+1)+1) by A2 .= z |^ (n+1) * z by NEWTON:6 .= seq.n * z by A2; end; A4: now assume |.z.| = 0; then A5: z =0c by COMPLEX1:45; A6: now let n; thus seq.n = 0c |^ (n+1) by A2,A5 .=(0c GeoSeq).n * 0c by Def1 .=0c; end; hence seq is convergent by COMSEQ_2:9; thus thesis by A6,COMSEQ_2:9,10; end; A7: seq.0= z |^ (0+1) by A2 .=z; now A8: 0 <= |.z.| by COMPLEX1:46; assume |.z.| <> 0; hence thesis by A1,A7,A3,A8,Th43; end; hence thesis by A4; end; theorem r>0 & (ex m st for n st n>=m holds |.seq.n.| >= r) implies not |.seq.| is convergent or lim |.seq.| <> 0 proof assume that A1: r>0 and A2: ex m st for n st n>=m holds |.seq.n.| >= r; consider m such that A3: for n st n>=m holds |.seq.n.| >= r by A2; now let n such that A4: n>=m; 0 <= |.seq.|.n by Lm3; then |.(|.seq.|).n.| =|.seq.|.n by ABSVALUE:def 1 .=|.seq.n.| by VALUED_1:18; hence |.(|.seq.|).n.| >= r by A3,A4; end; hence thesis by A1,SERIES_1:38; end; theorem Th46: seq is convergent iff for p st 0
0c; registration cluster summable for Complex_Sequence; existence proof take D, 0c; let p be Real such that A1: 0
convergent for Complex_Sequence; coherence by Def8; end; definition let seq be Complex_Sequence; attr seq is absolutely_summable means :Def9: |.seq.| is summable; end; theorem Th51: (for n holds seq.n = 0c) implies seq is absolutely_summable proof assume A1: for n holds seq.n = 0c; take 0; let p be Real such that A2: 0
summable for Real_Sequence; coherence by Def9; end; theorem Th52: seq is summable implies seq is convergent & lim seq = 0c proof assume A1: seq is summable; then Re Partial_Sums(seq) is convergent; then Partial_Sums(Re seq) is convergent by Th26; then A2: Re seq is summable; Im Partial_Sums(seq) is convergent by A1; then Partial_Sums(Im seq) is convergent by Th26; then A3: Im seq is summable; then lim(Im seq)=0 by SERIES_1:4; then A4: Im(lim(seq))=0 by A2,A3,Th42; lim(Re seq)=0 by A2,SERIES_1:4; then Re(lim(seq))=0 by A2,A3,Th42; hence thesis by A2,A3,A4,Lm1,Th42,COMPLEX1:13; end; registration cluster summable -> convergent for Complex_Sequence; coherence by Th52; end; theorem Th53: seq is summable implies Re seq is summable & Im seq is summable & Sum(seq)= Sum(Re seq)+Sum(Im seq)* proof A1: lim(Re Partial_Sums(seq))=lim(Partial_Sums(Re seq)) & lim(Im Partial_Sums( seq))=lim(Partial_Sums(Im seq)) by Th26; assume A2: seq is summable; then Re Partial_Sums(seq) is convergent; then A3: Partial_Sums(Re seq) is convergent by Th26; Im Partial_Sums(seq) is convergent by A2; then A4: Partial_Sums(Im seq) is convergent by Th26; lim(Re Partial_Sums(seq))=Re(lim(Partial_Sums(seq))) & lim(Im Partial_Sums( seq))=Im(lim(Partial_Sums(seq))) by A2,Th41; hence thesis by A3,A4,A1,COMPLEX1:13; end; registration let seq be summable Complex_Sequence; cluster Re seq -> summable for Real_Sequence; coherence by Th53; cluster Im seq -> summable for Real_Sequence; coherence by Th53; end; theorem Th54: seq1 is summable & seq2 is summable implies seq1+seq2 is summable & Sum(seq1+seq2)= Sum(seq1)+Sum(seq2) proof assume A1: seq1 is summable & seq2 is summable; then A2: Partial_Sums(seq1)+Partial_Sums(seq2) is convergent; A3: Partial_Sums(seq1)+Partial_Sums(seq2) =Partial_Sums(seq1+seq2) by Th27; Sum(seq1+seq2)=lim(Partial_Sums(seq1)+Partial_Sums(seq2)) by Th27 .=lim(Partial_Sums(seq1))+lim(Partial_Sums(seq2)) by A1,COMSEQ_2:14; hence thesis by A2,A3; end; theorem Th55: seq1 is summable & seq2 is summable implies seq1-seq2 is summable & Sum(seq1-seq2)= Sum(seq1)-Sum(seq2) proof assume A1: seq1 is summable & seq2 is summable; then A2: Partial_Sums(seq1)-Partial_Sums(seq2) is convergent; A3: Partial_Sums(seq1)-Partial_Sums(seq2) =Partial_Sums(seq1-seq2) by Th28; Sum(seq1-seq2)=lim(Partial_Sums(seq1)-Partial_Sums(seq2)) by Th28 .=lim(Partial_Sums(seq1))-lim(Partial_Sums(seq2)) by A1,COMSEQ_2:26; hence thesis by A2,A3; end; registration let seq1, seq2 be summable Complex_Sequence; cluster seq1 + seq2 -> summable for Complex_Sequence; coherence by Th54; cluster seq1 - seq2 -> summable for Complex_Sequence; coherence by Th55; end; theorem Th56: seq is summable implies for z being Complex holds z (#) seq is summable & Sum(z (#) seq)= z * Sum(seq) proof assume A1: seq is summable; let z be Complex; A2: Partial_Sums(z (#) seq)=(z (#) Partial_Sums(seq)) by Th29; Sum(z (#) seq)=lim((z (#) Partial_Sums(seq))) by Th29 .=z * Sum(seq) by A1,COMSEQ_2:18; hence thesis by A1,A2; end; registration let z be Element of COMPLEX, seq be summable Complex_Sequence; cluster z (#) seq -> summable for Complex_Sequence; coherence by Th56; end; theorem Th57: Re seq is summable & Im seq is summable implies seq is summable & Sum(seq)=Sum(Re seq)+Sum(Im seq)* proof assume that A1: Re seq is summable and A2: Im seq is summable; Partial_Sums(Im seq) is convergent by A2; then A3: Im Partial_Sums(seq) is convergent by Th26; Partial_Sums(Re seq) is convergent by A1; then A4: Re Partial_Sums(seq) is convergent by Th26; then A5: lim(Im Partial_Sums(seq))=Im(lim(Partial_Sums(seq))) by A3,Th42; A6: lim(Re Partial_Sums(seq))=lim(Partial_Sums(Re seq)) & lim(Im Partial_Sums( seq))=lim(Partial_Sums(Im seq)) by Th26; Partial_Sums(seq) is convergent & lim(Re Partial_Sums(seq))=Re(lim( Partial_Sums(seq))) by A4,A3,Th42; hence thesis by A6,A5,COMPLEX1:13; end; theorem Th58: seq is summable implies for n holds seq^\n is summable proof assume A1: seq is summable; let n; A2: Re (seq^\n)=Re seq^\n & Im(seq^\n)=Im seq^\n by Th23; Re seq^\n is summable & Im seq^\n is summable by A1,SERIES_1:12; hence seq^\n is summable by A2,Th57; end; registration let seq be summable Complex_Sequence, n be Nat; cluster seq^\n -> summable for Complex_Sequence; coherence by Th58; end; theorem (ex n st seq^\n is summable) implies seq is summable proof given n such that A1: seq^\n is summable; Im (seq^\n)=Im seq^\n by Th23; then A2: Im seq is summable by A1,SERIES_1:13; Re (seq^\n)=Re seq^\n by Th23; then Re seq is summable by A1,SERIES_1:13; hence thesis by A2,Th57; end; theorem seq is summable implies for n holds Sum(seq) = Partial_Sums(seq).n + Sum(seq^\(n+1)) proof assume A1: seq is summable; then Sum(seq)=Sum(Re(seq))+(Sum(Im(seq)))* by Th53; then A2: Re(Sum(seq))=Sum(Re(seq)) & Im(Sum(seq))=Sum(Im(seq)) by COMPLEX1:12; let n; A3: Sum(seq^\(n+1)) = Sum(Re(seq^\(n+1)))+(Sum(Im(seq^\(n+1))))* by A1,Th53; A4: Sum(Im(seq)) =Partial_Sums(Im(seq)).n + Sum(Im(seq)^\(n+1)) by A1, SERIES_1:15 .=Im(Partial_Sums(seq)).n + Sum(Im(seq)^\(n+1)) by Th26 .=Im(Partial_Sums(seq)).n + Sum(Im(seq^\(n+1))) by Th23 .=Im(Partial_Sums(seq)).n + Im(Sum(seq^\(n+1))) by A3,COMPLEX1:12 .=Im(Partial_Sums(seq).n) + Im(Sum(seq^\(n+1))) by Def6 .=Im(Partial_Sums(seq).n+ Sum(seq^\(n+1))) by COMPLEX1:8; Sum(Re(seq)) =Partial_Sums(Re(seq)).n + Sum(Re(seq)^\(n+1)) by A1,SERIES_1:15 .=Re(Partial_Sums(seq)).n + Sum(Re(seq)^\(n+1)) by Th26 .=Re(Partial_Sums(seq)).n + Sum(Re(seq^\(n+1))) by Th23 .=Re(Partial_Sums(seq)).n + Re(Sum(seq^\(n+1))) by A3,COMPLEX1:12 .=Re(Partial_Sums(seq).n) + Re(Sum(seq^\(n+1))) by Def5 .=Re(Partial_Sums(seq).n+ Sum(seq^\(n+1))) by COMPLEX1:8; hence thesis by A2,A4,COMPLEX1:def 3; end; theorem Th61: Partial_Sums |.seq.| is bounded_above iff seq is absolutely_summable proof Partial_Sums(|.seq.|) is bounded_above iff |.seq.| is summable; hence thesis; end; registration let seq be absolutely_summable Complex_Sequence; cluster Partial_Sums |.seq.| -> bounded_above for Real_Sequence; coherence by Th61; end; theorem Th62: seq is summable iff for p st 0
summable for Complex_Sequence; coherence by Th63; end; registration cluster absolutely_summable for Complex_Sequence; existence proof set C = the absolutely_summable Complex_Sequence; take C; thus thesis; end; end; theorem Th64: |.z.| < 1 implies z GeoSeq is summable & Sum(z GeoSeq) = 1r/(1r- z) proof set seq2 = NAT --> 1r; deffunc f(Nat) = z |^ ($1+1); consider seq1 such that A1: for n holds seq1.n=f(n) from COMSEQ_1:sch 1; assume A2: |.z.|<1; then A3: lim(seq1)=0c by A1,Th44; A4: now let n be Element of NAT; thus Partial_Sums(z GeoSeq).n = (1r - z |^ (n+1))/(1r-z) by A2,Th36, COMPLEX1:48 .= (1r - seq1.n)/(1r-z) by A1 .= 1r * (seq2.n-seq1.n)/(1r-z) by COMPLEX1:def 4,FUNCOP_1:7 .= (1r/(1r-z)) * (seq2.n+-seq1.n) by XCMPLX_1:74 .= (1r/(1r-z)) * (seq2.n+(-seq1).n) by VALUED_1:8 .= (1r/(1r-z)) * (seq2-seq1).n by VALUED_1:1 .= ((1r/(1r-z))(#)(seq2-seq1)).n by VALUED_1:6; end; A5: for n holds seq2.n=1r by ORDINAL1:def 12,FUNCOP_1:7; then A6: seq2 is convergent by COMSEQ_2:9; A7: seq1 is convergent by A2,A1,Th44; then A8: seq2-seq1 is convergent by A6; hence Partial_Sums(z GeoSeq) is convergent by A4,FUNCT_2:63; lim(seq2-seq1)=lim(seq2)-lim(seq1) by A7,A6,COMSEQ_2:26 .=1r by A3,A5,COMSEQ_2:10; then lim((1r/(1r-z))(#)(seq2-seq1))=1r/(1r-z) * 1r by A8,COMSEQ_2:18 .=1r/(1r-z) by COMPLEX1:def 4; hence thesis by A4,FUNCT_2:63; end; theorem |.z.| < 1 & (for n holds seq.(n+1) = z * seq.n) implies seq is summable & Sum(seq) = seq.0/(1r-z) proof assume that A1: |.z.|< 1 and A2: for n holds seq.(n+1) = z * seq.n; now let n be Element of NAT; thus Partial_Sums(seq).n = seq.0 * ((1r - z |^ (n+1))/(1r-z)) by A1,A2,Th37 ,COMPLEX1:48 .=seq.0 * Partial_Sums(z GeoSeq).n by A1,Th36,COMPLEX1:48 .=(seq.0 (#) Partial_Sums(z GeoSeq)).n by VALUED_1:6; end; then A3: Partial_Sums(seq)=(seq.0 (#) Partial_Sums(z GeoSeq)); A4: z GeoSeq is summable by A1,Th64; hence seq is summable by A3; Sum seq=seq.0 * Sum(z GeoSeq) by A3,A4,COMSEQ_2:18 .=seq.0 * (1r/(1r-z)) by A1,Th64 .=seq.0 * 1r/(1r-z) by XCMPLX_1:74 .=seq.0/(1r-z) by COMPLEX1:def 4; hence thesis; end; theorem rseq1 is summable & (ex m st for n st m<=n holds |.seq2.n.| <= rseq1.n ) implies seq2 is absolutely_summable proof assume that A1: rseq1 is summable and A2: ex m st for n st m<=n holds |.seq2.n.| <= rseq1.n; consider m such that A3: for n st m<=n holds |.seq2.n.| <= rseq1.n by A2; A4: now let n; |.seq2.n.|=|.seq2.|.n by VALUED_1:18; hence 0 <= |.seq2.|.n by COMPLEX1:46; end; now let n; assume m <= n; then |.seq2.n.| <= rseq1.n by A3; hence |.seq2.|.n <= rseq1.n by VALUED_1:18; end; hence |.seq2.| is summable by A1,A4,SERIES_1:19; end; theorem (for n holds 0 <= |.seq1.|.n & |.seq1.|.n <= |.seq2.|.n) & seq2 is absolutely_summable implies seq1 is absolutely_summable & Sum |.seq1.| <= Sum |.seq2.| by SERIES_1:20; theorem (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 by SERIES_1:27; theorem (for n holds rseq1.n = n-root (|.seq.|.n)) & rseq1 is convergent & lim rseq1 < 1 implies seq is absolutely_summable proof assume A1: ( for n holds rseq1.n = n-root (|.seq.|.n))& rseq1 is convergent & lim rseq1 < 1; for n holds |.seq.|.n >=0 by Lm3; hence |.seq.| is summable by A1,SERIES_1:28; end; theorem (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 proof assume A1: ( for n holds rseq1.n = n-root (|.seq.|.n))& ex m st for n st m<=n holds rseq1 .n>= 1; for n holds |.seq.|.n >=0 by Lm3; hence thesis by A1,SERIES_1:29; end; theorem (for n holds rseq1.n = n-root (|.seq.|.n)) & rseq1 is convergent & lim rseq1 > 1 implies seq is not absolutely_summable proof assume A1: ( for n holds rseq1.n = n-root (|.seq.|.n))& rseq1 is convergent & lim rseq1 > 1; for n holds |.seq.|.n >=0 by Lm3; hence |.seq.| is not summable by A1,SERIES_1:30; end; theorem |.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 ) proof assume |.seq.| is non-increasing & for n holds rseq1.n = 2 to_power n * |. seq.|.(2 to_power n); then for n holds |.seq.| is non-increasing & |.seq.|.n >= 0 & rseq1.n = 2 to_power n * |.seq.|.(2 to_power n) by Lm3; then |.seq.| is summable iff rseq1 is summable by SERIES_1:31; hence thesis; end; theorem p>1 & (for n st n>=1 holds |.seq.|.n = 1/n to_power p) implies seq is absolutely_summable by SERIES_1:32; theorem p<=1 & (for n st n>=1 holds |.seq.|.n=1/n to_power p) implies not seq is absolutely_summable by SERIES_1:33; theorem (for n holds seq.n<>0c & rseq1.n=|.seq.|.(n+1)/|.seq.|.n) & rseq1 is convergent & lim rseq1 < 1 implies seq is absolutely_summable proof assume that A1: for n holds seq.n<>0c & rseq1.n=|.seq.|.(n+1)/|.seq.|.n and A2: rseq1 is convergent & lim rseq1 < 1; now let n; A3: seq.n<>0c & |.seq.|.n =|.seq.n.| by A1,VALUED_1:18; hence |.seq.|.n <>0 & rseq1.n=|.seq.|.(n+1)/|.seq.|.n by A1,COMPLEX1:47; thus (|.seq.|).n <>0 & rseq1.n=|.(|.seq.|).|.(n+1)/|.seq.|.n by A1,A3, COMPLEX1:47; thus (|.seq.|).n <>0 & rseq1.n=abs((|.seq.|)).(n+1)/abs((|.seq.|)).n by A1 ,A3,COMPLEX1:47; end; then |.seq.| is absolutely_summable by A2,SERIES_1:37; hence thesis; end; theorem (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 proof assume that A1: for n holds seq.n<>0c and A2: ex m st for n st n>=m holds |.seq.|.(n+1)/|.seq.|.n >= 1; consider m such that A3: for n st n>=m holds |.seq.|.(n+1)/|.seq.|.n >= 1 by A2; A4: now let n; seq.n<>0c by A1; then |.seq.n.|<>0 by COMPLEX1:47; hence |.seq.|.n <>0 by VALUED_1:18; end; for n st n>=m holds abs((|.seq.|)).(n+1)/abs((|.seq.|)).n >= 1 by A3; hence |.seq.| is not summable by A4,SERIES_1:39; end;