:: Series :: by Konrad Raczkowski and Andrzej N\c{e}dzusiak :: :: Received October 15, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin theorem Th1: :: SERIES_1:1 for a being real number for s being Real_Sequence st 0 < a & a < 1 & ( for n being Element of NAT holds s . n = a to_power (n + 1) ) holds ( s is convergent & lim s = 0 ) proofend; theorem Th2: :: SERIES_1:2 for a being real number for n being Nat holds (abs a) to_power n = abs (a to_power n) proofend; theorem Th3: :: SERIES_1:3 for a being real number for s being Real_Sequence st abs a < 1 & ( for n being Element of NAT holds s . n = a to_power (n + 1) ) holds ( s is convergent & lim s = 0 ) proofend; definition let X be non empty complex-membered add-closed set ; let s1, s2 be sequence of X; :: original:+ redefine funcs1 + s2 -> sequence of X; coherence s1 + s2 is sequence of X proofend; end; definition let s be complex-valued ManySortedSet of NAT ; func Partial_Sums s -> complex-valued ManySortedSet of NAT means :Def1: :: SERIES_1:def 1 ( it . 0 = s . 0 & ( for n being Element of NAT holds it . (n + 1) = (it . n) + (s . (n + 1)) ) ); existence ex b1 being complex-valued ManySortedSet of NAT st ( b1 . 0 = s . 0 & ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) + (s . (n + 1)) ) ) proofend; uniqueness for b1, b2 being complex-valued ManySortedSet of NAT st b1 . 0 = s . 0 & ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) + (s . (n + 1)) ) & b2 . 0 = s . 0 & ( for n being Element of NAT holds b2 . (n + 1) = (b2 . n) + (s . (n + 1)) ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines Partial_Sums SERIES_1:def_1_:_ for s, b2 being complex-valued ManySortedSet of NAT holds ( b2 = Partial_Sums s iff ( b2 . 0 = s . 0 & ( for n being Element of NAT holds b2 . (n + 1) = (b2 . n) + (s . (n + 1)) ) ) ); registration let s be real-valued ManySortedSet of NAT ; cluster Partial_Sums s -> complex-valued real-valued ; coherence Partial_Sums s is real-valued proofend; end; definition let s be Real_Sequence; :: original:Partial_Sums redefine func Partial_Sums s -> Real_Sequence; coherence Partial_Sums s is Real_Sequence proofend; end; definition let s be Real_Sequence; attrs is summable means :Def2: :: SERIES_1:def 2 Partial_Sums s is convergent ; func Sum s -> Real equals :: SERIES_1:def 3 lim (Partial_Sums s); correctness coherence lim (Partial_Sums s) is Real; ; end; :: deftheorem Def2 defines summable SERIES_1:def_2_:_ for s being Real_Sequence holds ( s is summable iff Partial_Sums s is convergent ); :: deftheorem defines Sum SERIES_1:def_3_:_ for s being Real_Sequence holds Sum s = lim (Partial_Sums s); theorem Th4: :: SERIES_1:4 for s being Real_Sequence st s is summable holds ( s is convergent & lim s = 0 ) proofend; Lm1: for seq, seq1, seq2 being complex-valued ManySortedSet of NAT holds ( seq = seq1 + seq2 iff for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) ) proofend; theorem Th5: :: SERIES_1:5 for X being non empty complex-membered add-closed set for s1, s2 being sequence of X holds (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2) proofend; theorem Th6: :: SERIES_1:6 for s1, s2 being Real_Sequence holds (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2) proofend; theorem :: SERIES_1:7 for s1, s2 being Real_Sequence st s1 is summable & s2 is summable holds ( s1 + s2 is summable & Sum (s1 + s2) = (Sum s1) + (Sum s2) ) proofend; theorem :: SERIES_1:8 for s1, s2 being Real_Sequence st s1 is summable & s2 is summable holds ( s1 - s2 is summable & Sum (s1 - s2) = (Sum s1) - (Sum s2) ) proofend; theorem Th9: :: SERIES_1:9 for r being real number for s being Real_Sequence holds Partial_Sums (r (#) s) = r (#) (Partial_Sums s) proofend; theorem Th10: :: SERIES_1:10 for r being real number for s being Real_Sequence st s is summable holds ( r (#) s is summable & Sum (r (#) s) = r * (Sum s) ) proofend; theorem Th11: :: SERIES_1:11 for s, s1 being Real_Sequence st ( for n being Element of NAT holds s1 . n = s . 0 ) holds Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1 proofend; theorem Th12: :: SERIES_1:12 for s being Real_Sequence st s is summable holds for n being Element of NAT holds s ^\ n is summable proofend; theorem Th13: :: SERIES_1:13 for s being Real_Sequence st ex n being Element of NAT st s ^\ n is summable holds s is summable proofend; theorem Th14: :: SERIES_1:14 for s1, s2 being Real_Sequence st ( for n being Element of NAT holds s1 . n <= s2 . n ) holds for n being Element of NAT holds (Partial_Sums s1) . n <= (Partial_Sums s2) . n proofend; theorem :: SERIES_1:15 for s being Real_Sequence st s is summable holds for n being Element of NAT holds Sum s = ((Partial_Sums s) . n) + (Sum (s ^\ (n + 1))) proofend; theorem Th16: :: SERIES_1:16 for s being Real_Sequence st ( for n being Element of NAT holds 0 <= s . n ) holds Partial_Sums s is V41() proofend; theorem Th17: :: SERIES_1:17 for s being Real_Sequence st ( for n being Element of NAT holds 0 <= s . n ) holds ( Partial_Sums s is bounded_above iff s is summable ) proofend; theorem :: SERIES_1:18 for s being Real_Sequence st s is summable & ( for n being Element of NAT holds 0 <= s . n ) holds 0 <= Sum s proofend; theorem Th19: :: SERIES_1:19 for s2, s1 being Real_Sequence st ( for n being Element of NAT holds 0 <= s2 . n ) & s1 is summable & ex m being Element of NAT st for n being Element of NAT st m <= n holds s2 . n <= s1 . n holds s2 is summable proofend; theorem :: SERIES_1:20 for s1, s2 being Real_Sequence st ( for n being Element of NAT holds ( 0 <= s1 . n & s1 . n <= s2 . n ) ) & s2 is summable holds ( s1 is summable & Sum s1 <= Sum s2 ) proofend; theorem Th21: :: SERIES_1:21 for s being Real_Sequence holds ( s is summable iff for r being real number st 0 < r holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r ) proofend; :: [WP: ] Sum_of_a_Geometric_Series theorem Th22: :: SERIES_1:22 for n being Element of NAT for a being real number st a <> 1 holds (Partial_Sums (a GeoSeq)) . n = (1 - (a to_power (n + 1))) / (1 - a) proofend; theorem :: SERIES_1:23 for a being real number for s being Real_Sequence st a <> 1 & ( for n being Element of NAT holds s . (n + 1) = a * (s . n) ) holds for n being Element of NAT holds (Partial_Sums s) . n = ((s . 0) * (1 - (a to_power (n + 1)))) / (1 - a) proofend; theorem Th24: :: SERIES_1:24 for a being real number st abs a < 1 holds ( a GeoSeq is summable & Sum (a GeoSeq) = 1 / (1 - a) ) proofend; theorem :: SERIES_1:25 for a being real number for s being Real_Sequence st abs a < 1 & ( for n being Element of NAT holds s . (n + 1) = a * (s . n) ) holds ( s is summable & Sum s = (s . 0) / (1 - a) ) proofend; theorem Th26: :: SERIES_1:26 for s, s1 being Real_Sequence st ( for n being Element of NAT holds ( s . n > 0 & s1 . n = (s . (n + 1)) / (s . n) ) ) & s1 is convergent & lim s1 < 1 holds s is summable proofend; theorem :: SERIES_1:27 for s being Real_Sequence st ( for n being Element of NAT holds s . n > 0 ) & ex m being Element of NAT st for n being Element of NAT st n >= m holds (s . (n + 1)) / (s . n) >= 1 holds not s is summable proofend; theorem Th28: :: SERIES_1:28 for s, s1 being Real_Sequence st ( for n being Element of NAT holds ( s . n >= 0 & s1 . n = n -root (s . n) ) ) & s1 is convergent & lim s1 < 1 holds s is summable proofend; theorem Th29: :: SERIES_1:29 for s, s1 being Real_Sequence st ( for n being Element of NAT holds ( s . n >= 0 & s1 . n = n -root (s . n) ) ) & ex m being Element of NAT st for n being Element of NAT st m <= n holds s1 . n >= 1 holds not s is summable proofend; theorem :: SERIES_1:30 for s, s1 being Real_Sequence st ( for n being Element of NAT holds ( s . n >= 0 & s1 . n = n -root (s . n) ) ) & s1 is convergent & lim s1 > 1 holds not s is summable proofend; registration let k, n be Nat; clusterk to_power n -> natural ; coherence k to_power n is natural ; end; definition let k, n be Nat; :: original:to_power redefine funck to_power n -> Element of NAT ; coherence k to_power n is Element of NAT by ORDINAL1:def_12; end; theorem Th31: :: SERIES_1:31 for s, s1 being Real_Sequence st s is V42() & ( for n being Element of NAT holds ( s . n >= 0 & s1 . n = (2 to_power n) * (s . (2 to_power n)) ) ) holds ( s is summable iff s1 is summable ) proofend; theorem :: SERIES_1:32 for p being real number for s being Real_Sequence st p > 1 & ( for n being Element of NAT st n >= 1 holds s . n = 1 / (n to_power p) ) holds s is summable proofend; :: [WP: ] Divergence_of_the_Harmonic_Series theorem :: SERIES_1:33 for p being real number for s being Real_Sequence st p <= 1 & ( for n being Element of NAT st n >= 1 holds s . n = 1 / (n to_power p) ) holds not s is summable proofend; definition let s be Real_Sequence; attrs is absolutely_summable means :Def4: :: SERIES_1:def 4 abs s is summable ; end; :: deftheorem Def4 defines absolutely_summable SERIES_1:def_4_:_ for s being Real_Sequence holds ( s is absolutely_summable iff abs s is summable ); theorem Th34: :: SERIES_1:34 for s being Real_Sequence for n, m being Element of NAT st n <= m holds abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)) proofend; registration cluster Function-like V18( NAT , REAL ) absolutely_summable -> summable for Element of K19(K20(NAT,REAL)); coherence for b1 being Real_Sequence st b1 is absolutely_summable holds b1 is summable proofend; end; theorem :: SERIES_1:35 for s being Real_Sequence st s is absolutely_summable holds s is summable ; theorem :: SERIES_1:36 for s being Real_Sequence st ( for n being Element of NAT holds 0 <= s . n ) & s is summable holds s is absolutely_summable proofend; theorem :: SERIES_1:37 for s, s1 being Real_Sequence st ( for n being Element of NAT holds ( s . n <> 0 & s1 . n = ((abs s) . (n + 1)) / ((abs s) . n) ) ) & s1 is convergent & lim s1 < 1 holds s is absolutely_summable proofend; theorem Th38: :: SERIES_1:38 for r being real number for s being Real_Sequence st r > 0 & ex m being Element of NAT st for n being Element of NAT st n >= m holds abs (s . n) >= r & s is convergent holds lim s <> 0 proofend; theorem :: SERIES_1:39 for s being Real_Sequence st ( for n being Element of NAT holds s . n <> 0 ) & ex m being Element of NAT st for n being Element of NAT st n >= m holds ((abs s) . (n + 1)) / ((abs s) . n) >= 1 holds not s is summable proofend; theorem :: SERIES_1:40 for s1, s being Real_Sequence st ( for n being Element of NAT holds s1 . n = n -root ((abs s) . n) ) & s1 is convergent & lim s1 < 1 holds s is absolutely_summable proofend; theorem :: SERIES_1:41 for s1, s being Real_Sequence st ( for n being Element of NAT holds s1 . n = n -root ((abs s) . n) ) & ex m being Element of NAT st for n being Element of NAT st m <= n holds s1 . n >= 1 holds not s is summable proofend; theorem :: SERIES_1:42 for s1, s being Real_Sequence st ( for n being Element of NAT holds s1 . n = n -root ((abs s) . n) ) & s1 is convergent & lim s1 > 1 holds not s is summable proofend; begin :: from BHSP_4, 2006.03.04, A.T. definition let s be Real_Sequence; let n be Nat; func Sum (s,n) -> Real equals :: SERIES_1:def 5 (Partial_Sums s) . n; coherence (Partial_Sums s) . n is Real ; end; :: deftheorem defines Sum SERIES_1:def_5_:_ for s being Real_Sequence for n being Nat holds Sum (s,n) = (Partial_Sums s) . n; definition let s be Real_Sequence; let n, m be Nat; func Sum (s,n,m) -> Real equals :: SERIES_1:def 6 (Sum (s,n)) - (Sum (s,m)); coherence (Sum (s,n)) - (Sum (s,m)) is Real ; end; :: deftheorem defines Sum SERIES_1:def_6_:_ for s being Real_Sequence for n, m being Nat holds Sum (s,n,m) = (Sum (s,n)) - (Sum (s,m));