The abstract of the Mizar article:

Series

by

Konrad Raczkowski, and

Andrzej Nedzusiak

Received October 15, 1990

MML identifier: SERIES_1

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM, SEQ_1, FUNCT_1, POWER, SEQ_2, ORDINAL2, ARYTM_3, ARYTM_1,
      ABSVALUE, INT_1, SEQM_3, SUPINF_2, RLVECT_1, PROB_1, LATTICES, PREPOWER,
      SERIES_1, GROUP_1;
 notation ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, ABSVALUE, SEQ_1,
      SEQ_2, FUNCT_2, SEQM_3, INT_1, PREPOWER, POWER;
 constructors REAL_1, NAT_1, SEQ_2, SEQM_3, PREPOWER, POWER, PARTFUN1,
      MEMBERED, XBOOLE_0;
 clusters INT_1, XREAL_0, SEQ_1, NEWTON, RELSET_1, MEMBERED, ZFMISC_1,
      XBOOLE_0;
 requirements REAL, NUMERALS, SUBSET, ARITHM;


begin

reserve n,m,k for Nat;
reserve a,p,r for real number;
reserve s,s1,s2,s3 for Real_Sequence;

theorem :: SERIES_1:1
0<a & a<1 & (for n holds s.n=a to_power (n+1)) implies
s is convergent & lim s = 0;

theorem :: SERIES_1:2
a <> 0 implies abs(a) to_power n = abs(a to_power n);

theorem :: SERIES_1:3
abs(a)<1 & (for n holds s.n=a to_power (n+1)) implies
s is convergent & lim s = 0;

definition let s;
 func Partial_Sums(s) -> Real_Sequence means
:: SERIES_1:def 1
 it.0=s.0 & for n holds it.(n+1) = it.n + s.(n+1);
end;

definition let s;
 attr s is summable means
:: SERIES_1:def 2
 Partial_Sums(s) is convergent;

 func Sum(s) -> Real equals
:: SERIES_1:def 3
  lim Partial_Sums(s);
end;

canceled 3;

theorem :: SERIES_1:7
s is summable implies s is convergent & lim s = 0;

theorem :: SERIES_1:8
Partial_Sums(s1) + Partial_Sums(s2) = Partial_Sums(s1+s2);

theorem :: SERIES_1:9
Partial_Sums(s1) - Partial_Sums(s2) = Partial_Sums(s1-s2);

theorem :: SERIES_1:10
  s1 is summable & s2 is summable implies
s1+s2 is summable & Sum(s1+s2) = Sum(s1) + Sum(s2);

theorem :: SERIES_1:11
  s1 is summable & s2 is summable implies
s1-s2 is summable & Sum(s1-s2) = Sum(s1) - Sum(s2);

theorem :: SERIES_1:12
Partial_Sums(r(#)s) = r(#)Partial_Sums(s);

theorem :: SERIES_1:13
s is summable implies r(#)s is summable & Sum(r(#)s) =r*Sum(s);

theorem :: SERIES_1:14
for s,s1 st for n holds s1.n=s.0 holds
Partial_Sums(s^\1) = (Partial_Sums(s)^\1) - s1;

theorem :: SERIES_1:15
s is summable implies for n holds s^\n is summable;

theorem :: SERIES_1:16
(ex n st s^\n is summable) implies s is summable;

theorem :: SERIES_1:17
(for n holds s1.n<=s2.n) implies
for n holds Partial_Sums(s1).n<=Partial_Sums(s2).n;

theorem :: SERIES_1:18
  s is summable implies for n holds Sum(s) = Partial_Sums(s).n + Sum(s^\(n+1));

theorem :: SERIES_1:19
(for n holds 0<=s.n) implies Partial_Sums(s) is non-decreasing;

theorem :: SERIES_1:20
(for n holds 0<=s.n) implies
(Partial_Sums(s) is bounded_above iff s is summable);

theorem :: SERIES_1:21
  s is summable & (for n holds 0<=s.n) implies 0<=Sum(s);

theorem :: SERIES_1:22
(for n holds 0<=s2.n) & s1 is summable &
(ex m st for n st m<=n holds s2.n<=s1.n) implies s2 is summable;

canceled;

theorem :: SERIES_1:24
  (for n holds 0<=s1.n & s1.n<=s2.n) & s2 is summable implies
s1 is summable & Sum(s1)<=Sum(s2);

theorem :: SERIES_1:25
s is summable iff for r st 0<r ex n st
for m st n<=m holds abs(Partial_Sums(s).m - Partial_Sums(s).n)<r;

theorem :: SERIES_1:26
a <> 1 implies Partial_Sums(a GeoSeq).n = (1 - a to_power (n+1))/(1-a);

theorem :: SERIES_1:27
  a <> 1 & (for n holds s.(n+1) = a * s.n) implies
for n holds Partial_Sums(s).n = s.0 * (1 - a to_power (n+1))/(1-a);

theorem :: SERIES_1:28
abs(a)<1 implies a GeoSeq is summable & Sum(a GeoSeq) = 1/(1-a);

theorem :: SERIES_1:29
  abs(a) < 1 & (for n holds s.(n+1) = a * s.n) implies
s is summable & Sum(s) = s.0/(1-a);

theorem :: SERIES_1:30
(for n holds s.n>0 & s1.n=s.(n+1)/s.n) & s1 is convergent & lim s1 < 1
implies s is summable;

theorem :: SERIES_1:31
  (for n holds s.n>0) & (ex m st for n st n>=m holds s.(n+1)/s.n >= 1)
implies s is not summable;

theorem :: SERIES_1:32
(for n holds s.n>=0 & s1.n = n-root (s.n)) & s1 is convergent & lim s1 < 1
implies s is summable;

theorem :: SERIES_1:33
(for n holds s.n>=0 & s1.n = n-root (s.n)) &
 (ex m st for n st m<=n holds s1.n>=1)
implies s is not summable;

theorem :: SERIES_1:34
  (for n holds s.n>=0 & s1.n = n-root (s.n)) & s1 is convergent & lim s1 > 1
implies s is not summable;

definition let k, n be Nat;
  redefine func k to_power n -> Nat;
end;

theorem :: SERIES_1:35
s is non-increasing & (for n holds s.n>=0 &
s1.n = 2 to_power n * s.(2 to_power n)) implies
(s is summable iff s1 is summable);

theorem :: SERIES_1:36
  p>1 & (for n st n>=1 holds s.n = 1/n to_power p) implies s is summable;

theorem :: SERIES_1:37
  p<=1 & (for n st n>=1 holds s.n=1/n to_power p) implies s is not summable;

definition let s;
 canceled;

 attr s is absolutely_summable means
:: SERIES_1:def 5
 abs(s) is summable;
end;

canceled;

theorem :: SERIES_1:39
for n,m st n<=m holds abs(Partial_Sums(s).m - Partial_Sums(s).n) <=
abs(Partial_Sums(abs(s)).m - Partial_Sums(abs(s)).n);

theorem :: SERIES_1:40
  s is absolutely_summable implies s is summable;

theorem :: SERIES_1:41
  (for n holds 0<=s.n) & s is summable implies s is absolutely_summable;

theorem :: SERIES_1:42
  (for n holds s.n<>0 & s1.n=abs(s).(n+1)/abs(s).n) &
 s1 is convergent & lim s1 < 1
implies s is absolutely_summable;

theorem :: SERIES_1:43
r>0 & (ex m st for n st n>=m holds abs(s.n)>=r) implies
 s is not convergent or lim s <> 0;

theorem :: SERIES_1:44
  (for n holds s.n<>0) &
 (ex m st for n st n>=m holds abs(s).(n+1)/abs(s).n >= 1)
implies s is not summable;

theorem :: SERIES_1:45
  (for n holds s1.n = n-root (abs(s).n)) & s1 is convergent & lim s1 < 1
implies s is absolutely_summable;

theorem :: SERIES_1:46
  (for n holds s1.n = n-root(abs(s).n)) & (ex m st for n st m<=n holds s1.n>=1)
implies s is not summable;

theorem :: SERIES_1:47
  (for n holds s1.n = n-root (abs(s).n)) & s1 is convergent & lim s1 > 1
implies s is not summable;