:: Series
:: by Konrad Raczkowski and Andrzej N\c{e}dzusiak
::
:: Received October 15, 1990
:: Copyright (c) 1990-2018 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, SUBSET_1, XREAL_0, ORDINAL1, SEQ_1, ARYTM_3, CARD_1,
FUNCT_1, POWER, SEQ_2, ORDINAL2, ARYTM_1, XXREAL_0, COMPLEX1, RELAT_1,
INT_1, NAT_1, REAL_1, CARD_3, VALUED_1, VALUED_0, XXREAL_2, PREPOWER,
NEWTON, SERIES_1, ABIAN, MEMBERED, XBOOLE_0, IDEAL_1, PBOOLE, TARSKI,
FUNCT_7, ASYMPT_1;
notations XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1,
REAL_1, MEMBERED, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, INT_1, NAT_1,
VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, PBOOLE, FUNCT_2, NEWTON,
ABIAN, PREPOWER, POWER, FUNCOP_1, XXREAL_0;
constructors FUNCOP_1, XXREAL_0, REAL_1, NAT_1, SEQ_2, SEQM_3, NEWTON,
PREPOWER, POWER, PARTFUN1, VALUED_1, SEQ_4, RELSET_1, ABIAN, BINOP_2,
COMSEQ_2, SEQ_1, NUMBERS;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1,
MEMBERED, NEWTON, XBOOLE_0, VALUED_0, VALUED_1, FUNCT_2, POWER, SEQ_2,
SEQ_4, XCMPLX_0, SEQ_1;
requirements REAL, NUMERALS, SUBSET, ARITHM, BOOLE;
begin
reserve n,m,k for Nat;
reserve a,p,r for Real;
reserve s,s1,s2,s3 for Real_Sequence;
theorem :: SERIES_1:1
0 sequence of X;
end;
definition
let s be complex-valued ManySortedSet of NAT;
func Partial_Sums(s) -> complex-valued ManySortedSet of NAT means
:: SERIES_1:def 1
it.0 = s.0 & for n holds it.(n+1) = it.n + s.(n+1);
end;
registration
let s be real-valued ManySortedSet of NAT;
cluster Partial_Sums s -> real-valued;
end;
definition
let s be Real_Sequence;
redefine func Partial_Sums s -> Real_Sequence;
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;
theorem :: SERIES_1:4
s is summable implies s is convergent & lim s = 0;
theorem :: SERIES_1:5
for X being non empty add-closed complex-membered set
for s1,s2 being sequence of X holds
Partial_Sums(s1) + Partial_Sums(s2) = Partial_Sums(s1+s2);
theorem :: SERIES_1:6
Partial_Sums(s1) - Partial_Sums(s2) = Partial_Sums(s1-s2);
theorem :: SERIES_1:7
s1 is summable & s2 is summable implies s1+s2 is summable &
Sum(s1+s2) = Sum(s1) + Sum(s2);
theorem :: SERIES_1:8
s1 is summable & s2 is summable implies s1-s2 is summable & Sum(s1-s2)
= Sum(s1) - Sum(s2);
theorem :: SERIES_1:9
Partial_Sums(r(#)s) = r(#)Partial_Sums(s);
theorem :: SERIES_1:10
s is summable implies r(#)s is summable & Sum(r(#)s) =r*Sum(s);
theorem :: SERIES_1:11
for s,s1 st for n holds s1.n=s.0 holds Partial_Sums(s^\1) = (
Partial_Sums(s)^\1) - s1;
theorem :: SERIES_1:12
s is summable implies for n holds s^\n is summable;
theorem :: SERIES_1:13
(ex n st s^\n is summable) implies s is summable;
theorem :: SERIES_1:14
(for n holds s1.n<=s2.n) implies for n holds Partial_Sums(s1).n
<=Partial_Sums(s2).n;
theorem :: SERIES_1:15
s is summable implies
for n holds Sum(s) = Partial_Sums(s).n + Sum(s^\(n+1));
theorem :: SERIES_1:16
(for n holds 0<=s.n) implies Partial_Sums(s) is non-decreasing;
theorem :: SERIES_1:17
(for n holds 0<=s.n) implies (Partial_Sums(s) is bounded_above
iff s is summable);
theorem :: SERIES_1:18
s is summable & (for n holds 0<=s.n) implies 0<=Sum(s);
theorem :: SERIES_1:19
(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;
theorem :: SERIES_1:20
(for n holds 0<=s1.n & s1.n<=s2.n) & s2 is summable implies s1 is
summable & Sum(s1)<=Sum(s2);
theorem :: SERIES_1:21
s is summable iff for r st 0 1 implies Partial_Sums(a GeoSeq).n = (1 - a to_power (n+1)) /(1-a);
theorem :: SERIES_1:23
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:24
|.a.|<1 implies a GeoSeq is summable & Sum(a GeoSeq) = 1/(1-a);
theorem :: SERIES_1:25
|.a.| < 1 & (for n holds s.(n+1) = a * s.n) implies s is summable &
Sum(s) = s.0/(1-a);
theorem :: SERIES_1:26
(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:27
(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:28
(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:29
(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:30
(for n holds s.n>=0 & s1.n = n-root (s.n)) & s1 is convergent & lim s1
> 1 implies s is not summable;
registration
let k, n be Nat;
cluster k to_power n -> natural;
end;
definition
let k, n be Nat;
redefine func k to_power n -> Element of NAT;
end;
theorem :: SERIES_1:31
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:32
p>1 & (for n st n>=1 holds s.n = 1/n to_power p) implies s is summable;
::$N Divergence of the Harmonic Series
theorem :: SERIES_1:33
p<=1 & (for n st n>=1 holds s.n=1/n to_power p) implies s is not summable;
definition
let s;
attr s is absolutely_summable means
:: SERIES_1:def 4
abs s is summable;
end;
theorem :: SERIES_1:34
for n,m st n<=m holds |.Partial_Sums(s).m - Partial_Sums(s).n.|
<= |.Partial_Sums(|.s.|).m - Partial_Sums(|.s.|).n.|;
registration
cluster absolutely_summable -> summable for Real_Sequence;
end;
theorem :: SERIES_1:35
s is absolutely_summable implies s is summable;
theorem :: SERIES_1:36
(for n holds 0<=s.n) & s is summable implies s is absolutely_summable;
theorem :: SERIES_1:37
(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:38
r>0 & (ex m st for n st n>=m holds |.s.n.|>=r) implies s is not
convergent or lim s <> 0;
theorem :: SERIES_1:39
(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:40
(for n holds s1.n = n-root (abs(s).n)) & s1 is convergent & lim s1 < 1
implies s is absolutely_summable;
theorem :: SERIES_1:41
(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:42
(for n holds s1.n = n-root (abs(s).n)) & s1 is convergent & lim s1 > 1
implies s is not summable;
begin :: Addenda
:: from BHSP_4, 2006.03.04, A.T.
definition
let s;
let n be Nat;
func Sum(s, n) -> Real equals
:: SERIES_1:def 5
Partial_Sums(s).n;
end;
definition
let s;
let n,m be Nat;
func Sum(s, n, m) -> Real equals
:: SERIES_1:def 6
Sum(s, n) - Sum(s, m);
end;