:: Series :: by Konrad Raczkowski and Andrzej N\c{e}dzusiak :: :: Received October 15, 1990 :: Copyright (c) 1990-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, 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; 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;