:: 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;


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 <> 0c & (n+1)*<i> <> 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;

registration
  cluster summable -> convergent for Real_Sequence;
end;

registration
  cluster absolutely_summable -> summable for Real_Sequence;
end;

registration
  cluster absolutely_summable for 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 |.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 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 |.
Partial_Sums(rseq).m-Partial_Sums(rseq).n.| =Partial_Sums(rseq).m-Partial_Sums(
  rseq).n) & for n holds |.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 Complex;
reserve Nseq,Nseq1 for increasing sequence of NAT;

definition
  let z be 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 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)*<i>;

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<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

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 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 8

  Partial_Sums seq is convergent;
end;

registration
  cluster summable for Complex_Sequence;
end;

registration
  let seq be summable Complex_Sequence;
  cluster Partial_Sums seq -> 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)*<i>;

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)*<i>;

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<p holds ex n st for m st n <= m
  holds |.Partial_Sums(seq).m-Partial_Sums(seq).n.|<p;

theorem :: COMSEQ_3:63
  seq is absolutely_summable implies seq is summable;

registration
  cluster absolutely_summable -> 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;