An infinite sum is not a sum. Adding infinitely many numbers is not an operation anyone can carry out, so the value of a series is defined as the number its partial sums settle down to, if they settle at all. Everything in this chapter is a consequence of that one definition.
A sequence s0, s1, s2, … converges to L when, for every tolerance ε > 0, there is a place N after which every term is within ε of L: |sn − L| < ε for all n ≥ N. The series a0 + a1 + … converges to L when its partial sums Sn = a0 + … + an−1 do.
The Lean file states exactly this, as ConvergesTo and partialSum, and its first theorem, convergesTo_iff, proves the definition equal to Mathlib's own notion of a limit. That theorem is there so that every other statement in the file can be read against the definition above and not against a name.
For r ≠ 1, multiply Sn = 1 + r + … + rn−1 by r and subtract: everything cancels except the ends, so (1 − r)Sn = 1 − rn and Sn = (rn − 1)/(r − 1). When |r| < 1 the number 1/(1 − r) is the candidate limit, and the distance from it is exact:
For r = 1/2 this gives Sn = 2 − 21−n: below 2 at every step, and as close to 2 as you like. The script checks both formulas in exact fractions for several values of r (including a negative one) and finds, for ε = 10−6, the place N from which the error stays below ε.
In Lean this is geom_partial_sum and geom_series_converges. The second is proved by calling Mathlib's lemma for the geometric series, not by re-deriving the error formula above, so the hand argument and the machine proof are two routes to the same statement and the file does not contain the hand one.
Suppose s0 ≤ s1 ≤ … and no term exceeds a fixed number M. The completeness of the real numbers says the set of terms has a least upper bound L. Given ε > 0, the number L − ε is not an upper bound, so some sN > L − ε. From there on the sequence never decreases and never passes L, so L − ε < sn ≤ L for all n ≥ N. That is convergence to L.
The script runs the example sn = 1 − 1/(n+1): it is increasing and bounded by 1, and for ε = 1/10, 1/1000, 10−6 the place N = 1/ε works. In Lean the statement is bounded_monotone_converges, again proved with Mathlib's lemma for a monotone sequence bounded above.
If every term of a series is nonnegative, its partial sums can only grow. By § 3 they converge as soon as they are bounded. That is nonneg_series_bounded_converges. The comparison test follows in one line: if 0 ≤ an ≤ bn and the partial sums of b are bounded, then so are those of a, and a converges.
An example the script checks in exact arithmetic: 1/(i+2)2 ≤ 1/((i+1)(i+2)), and the larger series telescopes, because 1/((i+1)(i+2)) = 1/(i+1) − 1/(i+2), to 1 − 1/(n+1), which never exceeds 1. So the series of 1/(i+2)2 has bounded partial sums and converges. The chapter does not say what it converges to.
A theorem with a hypothesis is only informative if the hypothesis can fail. The partial sums of the constant sequence 1 are n, which exceeds every bound, so the boundedness hypothesis in § 4 really excludes something. The Lean file proves that as control_constant_unbounded, and the second control, control_half_geometric, confirms the geometric theorem gives 2 for r = 1/2.
Nonnegativity is also needed. The terms (−1)n have partial sums 1, 0, 1, 0, …, which are bounded and have no limit, because consecutive partial sums always differ by 1. The script checks this. The Lean file does not prove it. It is an illustration, and the chapter marks it as one.
Ratio test. Suppose no term is zero and |an+1| / |an| tends to L. If L < 1 the series converges absolutely. If L > 1 it does not converge. The idea for L < 1 is to choose r strictly between L and 1; from some place N on each term is at most r times the one before, so |an| ≤ |aN| rn−N, and the series is compared with a geometric one, as in § 4. For L > 1 the absolute values eventually increase, so the terms cannot tend to 0, and a convergent series has terms that do.
Take an = xn/n! with x ≠ 0. The ratio is |x|/(n+1), which tends to 0, so the series converges for every x. The script checks, for x = 2, 5, −7/2, the place from which the ratio stays below 1/2.
When L = 1 the test says nothing, and the script shows why: the harmonic series and the series of 1/(n+1)2 both have ratios tending to 1, yet the first diverges (its sum up to 2k terms is at least 1 + k/2) and the second converges (its partial sums stay below 2). Those are illustrations, not in the Lean file.
Alternating series test. If bn decreases and tends to 0, the series of (−1)n bn converges. The even partial sums rise, the odd ones fall, and the gap between neighbours is exactly b2k, so they close in on one number. The script checks this exactly for bn = 1/(n+1). The control: b = 1 decreases (it is constant), but the partial sums are 0, 1, 0, 1, …, so the hypothesis that b tends to 0 is doing real work. The Lean file states this as control_alternating_needs_limit_zero.
Abel’s lemma. If the terms an x0n are bounded by some M and |x| < |x0|, then the series of an xn converges. The reason: |an xn| ≤ M (|x|/|x0|)n, a geometric bound with ratio below 1. This is the step that makes a radius of convergence meaningful. I did not find this exact statement in the three held books, so its page is not checked here.
In Lean these are ratio_test_converges, ratio_test_diverges, alternating_series_test, power_series_abel and exp_series_converges_of_ne_zero, all in Series2.lean, which has been compiled once by the author: seven of its eight theorems passed with only the standard axioms, and the eighth (the exponential series) failed at one algebra step, which was then rewritten and not yet recompiled. Several proofs call Mathlib directly, so it checks that the textbook statements are true as formal sentences, not that the hand arguments above are right.
The matrix exponential in Book XXI is a power series, so this chapter is the first of the two that volume needs from here. The second is chapter 8.