Sequences and series · The Lumenary

Lens

MotivationH

Can you add forever?

The Greek philosopher Zeno of Elea (5th century BCE) posed a puzzle. To walk across a room 2 metres wide, you must first walk 1 metre, then half of the remaining metre, then half of what remains, and so on — infinitely many steps:

1 + \frac12 + \frac14 + \frac18 + \cdots

Infinitely many positive distances: surely they add up to an infinite distance, and you never arrive? Yet people cross rooms every day.

Adding long lists of numbers is much older than Zeno. Problem 79 of the Egyptian Rhind papyrus (about 1550 BCE) adds $7 + 49 + 343 + 2401 + 16807$ — seven houses, each with seven cats, each catching seven mice, and so on. Today the same arithmetic appears in savings that earn interest, in medicine doses that decay in the body, and in the decimal expansion of every number.

In this lesson we learn to add such lists — finite ones exactly, infinite ones by a limit — and find out when an infinite sum makes sense. Zeno's sum, we will prove, is exactly $2$ .

IntuitionH

Running totals that settle down

A sequence is an infinite list of numbers, $a_1, a_2, a_3, \dots$ . A series is what you get by adding the terms one by one and keeping a running total. For Zeno's walk the running totals are

1, \quad 1\tfrac12, \quad 1\tfrac34, \quad 1\tfrac78, \quad 1\tfrac{15}{16}, \quad \dots

Each is short of $2$ by exactly the last step taken: $1, \tfrac12, \tfrac14, \tfrac18, \dots$ The gap halves every time. It never becomes zero, but it becomes smaller than any distance you care to name — smaller than a millimetre after $11$ steps, smaller than the width of an atom after about $35$ . That is what we will mean by "the infinite sum is $2$ ": not that someone finishes infinitely many additions, but that the running totals close in on $2$ and on nothing else.

Half of a unit square, then a quarter, then an eighth, … Every piece is half of what is left, and the pieces fill the whole square: $\tfrac12 + \tfrac14 + \tfrac18 + \cdots = 1$. Adding the first step of Zeno's walk gives $1 + \tfrac12 + \tfrac14 + \cdots = 2$.

DefinitionsH

Definitions

Definition— sequence

A sequence of real numbers is a function that assigns a real number $a_n$ to each positive integer $n$ (sometimes to each $n \ge 0$ ). We write it $(a_n)$ or $a_1, a_2, a_3, \dots$ A sequence may be given by a formula, such as $a_n = \tfrac1n$ , or recursively, by giving the first term(s) and a rule for each term in terms of earlier ones, such as $a_1 = 1$ , $a_{n+1} = 2a_n + 1$ .

Definition— arithmetic and geometric sequences

A sequence is arithmetic if consecutive terms have a constant difference $d$ : $a_{n+1} = a_n + d$ , so $a_n = a + (n - 1)d$ with $a = a_1$ . It is geometric if consecutive terms have a constant ratio $r$ : $a_{n+1} = r\,a_n$ , so $a_n = a\,r^{n-1}$ .

Definition— summation notation

$\displaystyle\sum_{k=1}^{n} a_k = a_1 + a_2 + \dots + a_n$ . The letter $k$ is a "dummy" index: $\sum_{k=1}^{n} k^2$ and $\sum_{j=1}^{n} j^2$ mean the same thing. For example $\sum_{k=1}^{5} k^2 = 1 + 4 + 9 + 16 + 25 = 55$ .

Definition— limit of a sequence

A sequence $(s_n)$ converges to $L$ (or tends to $L$ ), written $s_n \to L$ or $\lim_{n\to\infty} s_n = L$ , if for every tolerance $\varepsilon > 0$ there is an index $N$ such that $|s_n - L| < \varepsilon$ for all $n \ge N$ . In words: eventually every term is within $\varepsilon$ of $L$ , however small $\varepsilon$ is. Otherwise the sequence diverges.

Definition— series and partial sums

Given a sequence $(a_k)$ , its partial sums are $S_n = a_1 + \dots + a_n$ . The series $\sum_{k=1}^{\infty} a_k$ converges to $S$ , and we write $\sum_{k=1}^{\infty} a_k = S$ , if $S_n \to S$ . If the partial sums have no limit, the series diverges.

So an infinite sum is not an infinite act of adding; it is the limit of finite sums. The limit laws you may know from Introductory calculus hold for sequences too: limits of sums, products and constant multiples are the sums, products and multiples of the limits.

Worked examplesH

Worked examples

Example— Arithmetic sequences

The seats in a stadium in Lagos are arranged so that the first row has $30$ seats and each row has $4$ more than the one in front: $a_n = 30 + 4(n - 1)$ . Row $25$ has $a_{25} = 126$ seats. By the formula proved below, the first $25$ rows hold $\tfrac{25(30 + 126)}{2} = 1950$ seats: number of rows times the average of the first and last row.

Example— Geometric sequences

A medicine with a half-life of one day: if $80$ mg are in the body today, then $80 \cdot (\tfrac12)^{n}$ mg remain after $n$ days — a geometric sequence with ratio $\tfrac12$ .
Savings of $1000$ rupees earning $5\%$ a year grow to $1000 \cdot 1.05^{n}$ rupees after $n$ years: ratio $1.05$ .
$3, -6, 12, -24, \dots$ has ratio $-2$ : the signs alternate and the sizes double.

Example— A recursive sequence

The Tower of Hanoi puzzle has discs of different sizes on one of three pegs; you must move the whole stack to another peg, one disc at a time, never putting a larger disc on a smaller one. To move $n + 1$ discs, you must move the top $n$ out of the way, move the largest disc, and move the $n$ back on top. So the least number of moves $h_n$ satisfies

h_0 = 0, \qquad h_{n+1} = 2h_n + 1,

giving $0, 1, 3, 7, 15, 31, \dots$ The pattern suggests $h_n = 2^n - 1$ , and induction proves it: $h_{n+1} + 1 = 2h_n + 2 = 2(h_n + 1) = 2 \cdot 2^n$ . Another famous recursion, $F_{n+2} = F_{n+1} + F_n$ , gives the sequence $1, 1, 2, 3, 5, 8, \dots$ , studied by Indian scholars of poetic metre (Virahāṅka, Hemachandra) centuries before Fibonacci's rabbits (1202).

Example— Limits of sequences

$\tfrac1n \to 0$ : given $\varepsilon > 0$ , choose $N > \tfrac1\varepsilon$ ; then $\tfrac1n \le \tfrac1N < \varepsilon$ for $n \ge N$ .
$\tfrac{2n + 1}{n} = 2 + \tfrac1n \to 2$ .
$(-1)^n$ diverges: its terms jump between $-1$ and $1$ and stay $2$ apart, so they cannot all be within $\varepsilon = \tfrac12$ of a single number.

Explore

Explore: watching partial sums

The partial sums of Zeno's series $\sum (\tfrac12)^{n-1}$ , with the limit $2$ drawn as a dashed line:

1 + 1/2 + 1/4 + ⋯

How many terms until the partial sums are within 0.001 of 2?

Examples

Term aₙ of the series

a_n =

partial sums Sₙ
terms aₙ
Known sum

Partial sums up to NN = 20

S₂₀ = a₁ + … + a₂₀ = 1.999998

Known sum: L = 2 · still missing: L − S₂₀ ≈ 0.000002

Partial sums on a screen are evidence, never proof: a series can look settled and still diverge, as the harmonic series does.

Now move the ratio $r$ . For which values do the partial sums of $1 + r + r^2 + \cdots$ settle down? Try $r = 0.9$ , $r = -0.9$ , $r = 1$ and $r = -1$ .

The geometric series 1 + r + r² + ⋯

Add the terms one by one. Do the partial sums Sₙ settle down, or keep growing?

Examples

Term aₙ of the series

a_n =

partial sums Sₙ
terms aₙ

Partial sums up to NN = 60

rr = 0.5

S₆₀ = a₁ + … + a₆₀ = 2

Partial sums on a screen are evidence, never proof: a series can look settled and still diverge, as the harmonic series does.

Finally the harmonic series $1 + \tfrac12 + \tfrac13 + \cdots$ . Switch on the logarithmic axis: the partial sums keep climbing, by about the same amount each time $n$ is multiplied by $10$ .

The harmonic series

The terms shrink to 0. Do the partial sums settle down?

Examples

Term aₙ of the series

a_n =

partial sums Sₙ
terms aₙ
ln n + γ

Partial sums up to NN = 1000

S₁₀₀₀ = a₁ + … + a₁₀₀₀ = 7.485471

This is the harmonic series. Its partial sums grow without bound, but very slowly, like ln n + γ (γ ≈ 0.5772): S₁₀₀₀ ≈ 7.49, and Sₙ first passes 100 only after about 1.5 × 10⁴³ terms. The graph seems to level off; it never does.

Partial sums on a screen are evidence, never proof: a series can look settled and still diverge, as the harmonic series does.

Recursive sequences can be explored with a cobweb diagram. Iterating $x \mapsto \tfrac{x}{2} + 1$ from any start gives a sequence converging to $2$ , the solution of $x = \tfrac x2 + 1$ . Iterating the logistic map $x \mapsto r x(1 - x)$ instead can converge, oscillate or behave chaotically depending on $r$ — the start of the theory of dynamical systems.

Iterating the logistic map x ↦ r x (1 − x)

Try r = 2.8, 3.2, 3.5 and 3.9.

The map f

f(x) =

Iterates xₖ against k

y = f(x)
y = x
cobweb path

Starting value x₀x₀ = 0.2Iterationsk = 60

rr = 3.2

Last iterates: x₅₈ = 0.79946, x₅₉ = 0.51304, x₆₀ = 0.79946

The orbit appears to settle into a cycle of period 2: 0.513, 0.7995.

Fixed points in view (numerical): x* = 0 (repelling: |f′(x*)| > 1); x* = 0.6875 (repelling: |f′(x*)| > 1)

Based on 3,000 iterations in floating-point arithmetic: numerical evidence, not proof.

ProofH

Finite sums

Theorem— Theorem 1 (arithmetic series)

The sum of the first $n$ terms of the arithmetic sequence $a, a + d, a + 2d, \dots$ is

S_n = \sum_{k=0}^{n-1} (a + kd) = \frac{n\big(2a + (n - 1)d\big)}{2} = \frac{n\,(\text{first} + \text{last})}{2}.

Proof

Write the sum forwards and backwards and add the two lines term by term:

\begin{aligned} S_n &= a + (a + d) + \dots + \big(a + (n - 1)d\big), \\ S_n &= \big(a + (n - 1)d\big) + \big(a + (n - 2)d\big) + \dots + a. \end{aligned}

Each of the $n$ columns adds up to $2a + (n - 1)d$ , so $2S_n = n\big(2a + (n - 1)d\big)$ .

∎

With $a = d = 1$ this gives $1 + 2 + \dots + n = \tfrac{n(n + 1)}{2}$ . A famous story — probably embellished — tells that the young Gauss found $1 + 2 + \dots + 100 = 5050$ this way in seconds.

Theorem— Theorem 2 (geometric series, finite)

If $r \ne 1$ , then for every $n \ge 0$

a + ar + ar^2 + \dots + ar^{n-1} = \frac{a(1 - r^n)}{1 - r}.

Proof

Let $S = 1 + r + \dots + r^{n-1}$ . Then $rS = r + r^2 + \dots + r^n$ , and subtracting, every term except the first of $S$ and the last of $rS$ cancels:

(1 - r)S = 1 - r^n.

(This "telescoping" can also be proved by induction on $n$ : $(1 - r)\big(S + r^n\big) = 1 - r^n + r^n - r^{n+1} = 1 - r^{n+1}$ .) Divide by $1 - r \ne 0$ and multiply by $a$ .

∎

For $r = 1$ the sum is simply $na$ .

ProofH

Infinite series

To let $n \to \infty$ in Theorem 2 we need to know what happens to $r^n$ .

Theorem— Lemma 3 (Bernoulli's inequality)

If $t \ge 0$ , then $(1 + t)^n \ge 1 + nt$ for every $n \ge 0$ .

Proof

Induction on $n$ . For $n = 0$ : $1 \ge 1$ . If $(1 + t)^n \ge 1 + nt$ , then

(1 + t)^{n+1} = (1 + t)^n(1 + t) \ge (1 + nt)(1 + t) = 1 + (n + 1)t + nt^2 \ge 1 + (n + 1)t.

∎

Theorem— Theorem 4 (powers of a small ratio)

If $|r| < 1$ , then $r^n \to 0$ as $n \to \infty$ .

Proof

If $r = 0$ there is nothing to prove. Otherwise $\tfrac{1}{|r|} > 1$ ; write $\tfrac{1}{|r|} = 1 + t$ with $t > 0$ . By Lemma 3, $\tfrac{1}{|r|^n} = (1 + t)^n \ge 1 + nt > nt$ , so

|r^n - 0| = |r|^n < \frac{1}{nt}.

Given $\varepsilon > 0$ , choose $N > \tfrac{1}{t\varepsilon}$ ; then $|r^n| < \tfrac{1}{nt} \le \tfrac{1}{Nt} < \varepsilon$ for all $n \ge N$ .

∎

Theorem— Theorem 5 (infinite geometric series)

Let $a \ne 0$ . If $|r| < 1$ , then

\sum_{k=0}^{\infty} a r^k = a + ar + ar^2 + \cdots = \frac{a}{1 - r}.

If $|r| \ge 1$ , the series diverges.

Proof

Case $|r| < 1$ . By Theorem 2 the $n$ -th partial sum is $S_n = \tfrac{a(1 - r^n)}{1 - r} = \tfrac{a}{1 - r} - \tfrac{a}{1 - r}\,r^n$ . By Theorem 4, $r^n \to 0$ , so $S_n \to \tfrac{a}{1 - r}$ .

Case $|r| \ge 1$ . Then $|ar^k| = |a|\,|r|^k \ge |a| > 0$ for every $k$ , so the terms do not tend to $0$ , and the series diverges by the term test (Theorem 6 below).

∎

Example— Zeno, 0.999… and repeating decimals

$1 + \tfrac12 + \tfrac14 + \cdots$ : $a = 1$ , $r = \tfrac12$ , sum $\tfrac{1}{1 - 1/2} = 2$ . Zeno's walker arrives.
$0.999\ldots$ means $\tfrac{9}{10} + \tfrac{9}{100} + \tfrac{9}{1000} + \cdots$ : $a = \tfrac{9}{10}$ , $r = \tfrac{1}{10}$ , sum $\tfrac{9/10}{9/10} = 1$ . So $0.999\ldots = 1$ exactly: the partial sums $0.9, 0.99, \dots$ fall short of $1$ by $10^{-n}$ , which tends to $0$ .
$0.272727\ldots = \tfrac{27}{100} + \tfrac{27}{100^2} + \cdots = \tfrac{27/100}{1 - 1/100} = \tfrac{27}{99} = \tfrac{3}{11}$ . Every repeating decimal is a geometric series, which is why it is a fraction (compare Real numbers and irrationality).
$1 - \tfrac12 + \tfrac14 - \tfrac18 + \cdots$ : $r = -\tfrac12$ , sum $\tfrac{1}{3/2} = \tfrac23$ .

Theorem— Theorem 6 (term test)

If $\sum a_k$ converges, then $a_k \to 0$ . Equivalently: if the terms do not tend to $0$ , the series diverges.

Proof

Let $S_n \to S$ . Then also $S_{n-1} \to S$ (it is the same sequence, shifted by one place), so $a_n = S_n - S_{n-1} \to S - S = 0$ .

∎

The term test can only prove divergence. Terms tending to $0$ is necessary for convergence, but not sufficient — as the most famous series of all shows.

Theorem— Theorem 7 (the harmonic series diverges)

The partial sums $H_n = 1 + \tfrac12 + \tfrac13 + \dots + \tfrac1n$ satisfy $H_{2^m} \ge 1 + \tfrac m2$ for every $m \ge 0$ . Hence $H_n$ grows without bound, and $\sum_{k=1}^{\infty} \tfrac1k$ diverges, although $\tfrac1k \to 0$ .

Proof

Group the terms after the first into blocks that end at powers of $2$ :

1 + \tfrac12 + \Big(\tfrac13 + \tfrac14\Big) + \Big(\tfrac15 + \tfrac16 + \tfrac17 + \tfrac18\Big) + \Big(\tfrac19 + \dots + \tfrac1{16}\Big) + \cdots

The block $\tfrac{1}{2^j + 1} + \dots + \tfrac{1}{2^{j+1}}$ has $2^j$ terms, each at least $\tfrac{1}{2^{j+1}}$ , so it adds up to at least $2^j \cdot \tfrac{1}{2^{j+1}} = \tfrac12$ . The first $2^m$ terms consist of the term $1$ and the $m$ blocks $j = 0, \dots, m - 1$ , so $H_{2^m} \ge 1 + \tfrac m2$ .

Given any number $B$ , choose $m > 2B$ ; then $H_n \ge H_{2^m} > B$ for all $n \ge 2^m$ , because the partial sums increase. So $(H_n)$ is unbounded and cannot converge.

∎

The divergence is extraordinarily slow: $H_n$ first exceeds $10$ at $n = 12\,367$ and first exceeds $100$ only after more than $10^{43}$ terms. (In fact $H_n$ is close to $\ln n + 0.5772\ldots$ ; see Exponential and logarithmic functions.) By contrast, squaring the denominators makes the series converge:

Theorem— Proposition 8 (the sum of 1/k² is less than 2)

For every $n \ge 1$ : $\;1 + \tfrac14 + \tfrac19 + \dots + \tfrac1{n^2} < 2$ .

Proof

For $k \ge 2$ , $\tfrac{1}{k^2} < \tfrac{1}{k(k - 1)} = \tfrac{1}{k - 1} - \tfrac1k$ . Adding these for $k = 2, \dots, n$ , the right-hand sides telescope:

\sum_{k=1}^{n}\frac{1}{k^2} < 1 + \Big(1 - \tfrac12\Big) + \Big(\tfrac12 - \tfrac13\Big) + \dots + \Big(\tfrac1{n-1} - \tfrac1n\Big) = 2 - \tfrac1n < 2.

(For $n = 1$ the sum is $1 < 2$ .)

∎

The partial sums of $\sum \tfrac{1}{k^2}$ increase and stay below $2$ ; the completeness of the real numbers (an increasing sequence that is bounded above converges) then guarantees that the series converges. Its sum, $\tfrac{\pi^2}{6} \approx 1.6449$ , was found by Euler in 1734 — the "Basel problem".

Formal mathematicsF

Series in Lean

In Mathlib a sequence is a function ℕ → ℝ, starting at index $0$ , and ∑ k ∈ range n, f k is $f(0) + \dots + f(n - 1)$ — the first $n$ terms. HasSum f S means the series $\sum f(k)$ converges to $S$ , and Summable f that it converges to something.

First the finite sums: Theorem 1 and the telescoping of Theorem 2, both by induction, and the closed form (with Mathlib's version for comparison):

arith_sumLean 4Proved here from basic factsFormally verified

/-- **Sum of an arithmetic progression.** The first `n` terms of `a, a + d, a + 2d, …` add up to
`n(2a + (n − 1)d)/2`: "number of terms times the average of the first and last". Proved by
induction on `n`. -/
theorem arith_sum (a d : ℝ) (n : ℕ) :
    ∑ k ∈ range n, (a + k * d) = n * (2 * a + (n - 1) * d) / 2 := by
  induction n with
  | zero => simp
  | succ m ih =>
    rw [sum_range_succ, ih]
    push_cast
    ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/SequencesSeries.leanTry it in the Lean web editor

geom_telescopeLean 4Proved here from basic factsFormally verified

/-- **The telescoping step.** `(1 − r)(1 + r + ⋯ + rⁿ⁻¹) = 1 − rⁿ`: multiplying by `1 − r`
makes every middle term cancel. Proved by induction on `n`. -/
theorem geom_telescope (r : ℝ) (n : ℕ) : (1 - r) * ∑ k ∈ range n, r ^ k = 1 - r ^ n := by
  induction n with
  | zero => simp
  | succ m ih =>
    rw [sum_range_succ, mul_add, ih, pow_succ]
    ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/SequencesSeries.leanTry it in the Lean web editor

geom_sumLean 4Proved here from basic factsFormally verified

/-- **Finite geometric sum.** For `r ≠ 1`, `a + ar + ⋯ + arⁿ⁻¹ = a(1 − rⁿ)/(1 − r)`:
divide the telescoping identity by `1 − r ≠ 0`. -/
theorem geom_sum (a r : ℝ) (hr : r ≠ 1) (n : ℕ) :
    ∑ k ∈ range n, a * r ^ k = a * (1 - r ^ n) / (1 - r) := by
  have h1 : 1 - r ≠ 0 := sub_ne_zero.mpr (Ne.symm hr)
  rw [← mul_sum, ← geom_telescope r n]
  field_simp

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/SequencesSeries.leanTry it in the Lean web editor

geom_sum_libraryLean 4Applies a library theoremFormally verified

/-- The same sum in Mathlib's form `(rⁿ − 1)/(r − 1)`, from `geom_sum_eq`, which holds in every
division ring. -/
theorem geom_sum_library (r : ℝ) (hr : r ≠ 1) (n : ℕ) :
    ∑ k ∈ range n, r ^ k = (r ^ n - 1) / (r - 1) :=
  geom_sum_eq hr n

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/SequencesSeries.leanTry it in the Lean web editor

The Tower of Hanoi recursion, as a Lean definition by pattern matching, and its closed form:

hanoiLean 4Formally verified

/-- The **Tower of Hanoi numbers**, defined recursively: no moves for `0` discs, and to move
`n + 1` discs, move `n` discs aside, move the largest disc, and move the `n` discs back on top:
`h(n + 1) = 2 h(n) + 1`. -/
def hanoi : ℕ → ℕ
  | 0 => 0
  | n + 1 => 2 * hanoi n + 1

Axioms used: No axiomsformal/Lumenary/SequencesSeries.leanTry it in the Lean web editor

hanoi_formulaLean 4Proved here from basic factsFormally verified

/-- **A closed form for the recursion:** `h(n) + 1 = 2ⁿ`, i.e. `h(n) = 2ⁿ − 1`. Induction:
`h(n + 1) + 1 = 2h(n) + 2 = 2(h(n) + 1) = 2 · 2ⁿ`. (Stated with `+ 1` to avoid natural-number
subtraction.) -/
theorem hanoi_formula (n : ℕ) : hanoi n + 1 = 2 ^ n := by
  induction n with
  | zero => rfl
  | succ m ih =>
    rw [hanoi, pow_succ, ← ih]
    ring

Axioms used: propextformal/Lumenary/SequencesSeries.leanTry it in the Lean web editor

Theorem 5 for $|r| < 1$ . Our proof combines the closed form with Mathlib's lemma that $r^n \to 0$ (Theorem 4, which we proved by hand above but do not re-prove in Lean):

geom_series_tendstoLean 4Proved here from basic factsFormally verified

/-- **Infinite geometric series.** If `|r| < 1`, the partial sums of `a + ar + ar² + ⋯` tend to
`a/(1 − r)`. The partial sum is `a(1 − rⁿ)/(1 − r)` (`geom_sum`), and `rⁿ → 0` when `|r| < 1`
(Mathlib's `tendsto_pow_atTop_nhds_zero_of_abs_lt_one`), so the partial sums tend to
`a(1 − 0)/(1 − r)`. -/
theorem geom_series_tendsto (a r : ℝ) (hr : |r| < 1) :
    Tendsto (fun n => ∑ k ∈ range n, a * r ^ k) atTop (𝓝 (a / (1 - r))) := by
  have hr1 : r ≠ 1 := by
    intro h
    rw [h, abs_one] at hr
    exact lt_irrefl 1 hr
  have hpow := tendsto_pow_atTop_nhds_zero_of_abs_lt_one hr
  have hlim : Tendsto (fun n => a * (1 - r ^ n) / (1 - r)) atTop (𝓝 (a * (1 - 0) / (1 - r))) :=
    ((tendsto_const_nhds.sub hpow).const_mul a).div_const (1 - r)
  rw [sub_zero, mul_one] at hlim
  refine hlim.congr (fun n => ?_)
  exact (geom_sum a r hr1 n).symm

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/SequencesSeries.leanTry it in the Lean web editor

geom_series_hasSumLean 4Applies a library theoremFormally verified

/-- The same result as a statement about the series: `Σ a rᵏ = a/(1 − r)` for `|r| < 1`. This
applies Mathlib's `hasSum_geometric_of_abs_lt_one` (the case `a = 1`) and multiplies by `a`. -/
theorem geom_series_hasSum (a r : ℝ) (hr : |r| < 1) :
    HasSum (fun n => a * r ^ n) (a / (1 - r)) := by
  rw [div_eq_mul_inv]
  exact (hasSum_geometric_of_abs_lt_one hr).mul_left a

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/SequencesSeries.leanTry it in the Lean web editor

halvesLean 4Applies a library theoremFormally verified

/-- **`1 + 1/2 + 1/4 + 1/8 + ⋯ = 2`.** This applies Mathlib's `hasSum_geometric_two`. -/
theorem halves : HasSum (fun n : ℕ => (1 / 2 : ℝ) ^ n) 2 := hasSum_geometric_two

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/SequencesSeries.leanTry it in the Lean web editor

point_nine_recurringLean 4Proved here from basic factsFormally verified

/-- **`0.999… = 1`.** The decimal `0.999…` *means* the series `9/10 + 9/100 + 9/1000 + ⋯`, a
geometric series with first term `9/10` and ratio `1/10`. Its terms are positive, so it converges
to `S` exactly when its partial sums tend to `S`; and by `geom_series_tendsto` they tend to
`(9/10)/(1 − 1/10) = 1`. -/
theorem point_nine_recurring : HasSum (fun n : ℕ => (9 : ℝ) / 10 ^ (n + 1)) 1 := by
  rw [hasSum_iff_tendsto_nat_of_nonneg (fun n => by positivity)]
  have h := geom_series_tendsto (9 / 10) (1 / 10) (by rw [abs_of_pos (by norm_num)]; norm_num)
  norm_num at h
  refine h.congr (fun n => sum_congr rfl (fun k _ => ?_))
  rw [pow_succ, div_pow, one_pow]
  field_simp

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/SequencesSeries.leanTry it in the Lean web editor

The term test (from Mathlib), divergence for $|r| \ge 1$ , and the harmonic series: Oresme's estimate, the unbounded growth of the partial sums, and the conclusion that terms tending to $0$ do not force convergence:

term_testLean 4Applies a library theoremFormally verified

/-- **The term test.** If `Σ aₙ` converges, then `aₙ → 0`. Equivalently: if the terms do *not*
tend to `0`, the series diverges. This applies Mathlib's `Summable.tendsto_atTop_zero`. The
converse is false — see `harmonic_terms_tend_to_zero_but_diverges`. -/
theorem term_test {f : ℕ → ℝ} (h : Summable f) : Tendsto f atTop (𝓝 0) :=
  h.tendsto_atTop_zero

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/SequencesSeries.leanTry it in the Lean web editor

geom_divergesLean 4Proved here from basic factsFormally verified

/-- **If `|r| ≥ 1`, then `Σ rⁿ` diverges.** Its terms satisfy `|rⁿ| = |r|ⁿ ≥ 1`, so they do not
tend to `0`, and the term test rules out convergence. (Mathlib:
`summable_geometric_iff_norm_lt_one`.) -/
theorem geom_diverges (r : ℝ) (hr : 1 ≤ |r|) : ¬ Summable (fun n : ℕ => r ^ n) := by
  intro hs
  have h0 : Tendsto (fun n : ℕ => |r ^ n|) atTop (𝓝 0) := by
    simpa using (term_test hs).abs
  -- Eventually `|rⁿ| < 1`, but every `|rⁿ| = |r|ⁿ ≥ 1`.
  obtain ⟨N, hN⟩ := eventually_atTop.mp (h0.eventually (gt_mem_nhds zero_lt_one))
  have hlt := hN N le_rfl
  rw [abs_pow] at hlt
  exact absurd (one_le_pow₀ hr) (not_le.mpr hlt)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/SequencesSeries.leanTry it in the Lean web editor

harmonic_two_powLean 4Proved here from basic factsFormally verified

/-- **Oresme's estimate (c. 1350).** `1 + 1/2 + ⋯ + 1/2ⁿ ≥ 1 + n/2`. Group the terms:
the block `1/(2ᵐ + 1) + ⋯ + 1/2ᵐ⁺¹` has `2ᵐ` terms, each at least `1/2ᵐ⁺¹`, so it adds at least
`1/2`. Induction on `n` adds one block at a time. -/
theorem harmonic_two_pow (n : ℕ) :
    1 + (n : ℝ) / 2 ≤ ∑ k ∈ range (2 ^ n), (1 : ℝ) / (k + 1) := by
  induction n with
  | zero => norm_num
  | succ m ih =>
    rw [pow_succ, mul_two, sum_range_add]
    -- The new block: `2ᵐ` terms, each `≥ 1/2ᵐ⁺¹`.
    have hblock : (1 : ℝ) / 2 ≤ ∑ x ∈ range (2 ^ m), (1 : ℝ) / ((2 ^ m + x : ℕ) + 1) := by
      have hterm : ∀ x ∈ range (2 ^ m),
          (1 : ℝ) / (2 ^ (m + 1)) ≤ (1 : ℝ) / ((2 ^ m + x : ℕ) + 1) := by
        intro x hx
        have hx' : x < 2 ^ m := mem_range.mp hx
        apply one_div_le_one_div_of_le (by positivity)
        have : (2 ^ m + x + 1 : ℕ) ≤ 2 ^ (m + 1) := by rw [pow_succ]; omega
        exact_mod_cast this
      calc (1 : ℝ) / 2 = ∑ _x ∈ range (2 ^ m), (1 : ℝ) / (2 ^ (m + 1)) := by
            rw [sum_const, card_range, nsmul_eq_mul, pow_succ]
            push_cast
            field_simp
        _ ≤ _ := sum_le_sum hterm
    push_cast at hblock ih ⊢
    linarith

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/SequencesSeries.leanTry it in the Lean web editor

harmonic_tendsto_atTopLean 4Proved here from basic factsFormally verified

/-- **The harmonic partial sums grow without bound.** `Hₙ = 1 + 1/2 + ⋯ + 1/n` increases with
`n`, and `H_{2ᵐ} ≥ 1 + m/2` exceeds any given bound for large `m`. An increasing sequence that is
not bounded above tends to infinity. (Mathlib: `Real.tendsto_sum_range_one_div_nat_succ_atTop`.) -/
theorem harmonic_tendsto_atTop :
    Tendsto (fun n => ∑ k ∈ range n, (1 : ℝ) / (k + 1)) atTop atTop := by
  apply tendsto_atTop_atTop_of_monotone
  · intro m n hmn
    exact sum_le_sum_of_subset_of_nonneg (range_mono hmn) (fun _ _ _ => by positivity)
  · intro b
    obtain ⟨m, hm⟩ := exists_nat_gt (2 * b)
    refine ⟨2 ^ m, le_trans ?_ (harmonic_two_pow m)⟩
    linarith

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/SequencesSeries.leanTry it in the Lean web editor

harmonic_terms_tend_to_zero_but_divergesLean 4Proved here from basic factsFormally verified

/-- **Terms tending to `0` do not guarantee convergence.** The terms `1/(n + 1)` of the harmonic
series tend to `0`, yet the series diverges: if it converged, its partial sums would tend to a
finite limit, but they tend to infinity (`harmonic_tendsto_atTop`). -/
theorem harmonic_terms_tend_to_zero_but_diverges :
    Tendsto (fun n : ℕ => (1 : ℝ) / (n + 1)) atTop (𝓝 0) ∧
      ¬ Summable (fun n : ℕ => (1 : ℝ) / (n + 1)) := by
  constructor
  · exact tendsto_one_div_add_atTop_nhds_zero_nat
  · intro hs
    exact not_tendsto_nhds_of_tendsto_atTop harmonic_tendsto_atTop _ hs.hasSum.tendsto_sum_nat

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/SequencesSeries.leanTry it in the Lean web editor

harmonic_not_summable_libraryLean 4Applies a library theoremFormally verified

/-- The divergence of the harmonic series in Mathlib's form, `Real.not_summable_one_div_natCast`
(the `n = 0` term is `1/0 = 0` in Lean, which does not affect convergence). -/
theorem harmonic_not_summable_library : ¬ Summable (fun n : ℕ => (1 : ℝ) / n) :=
  Real.not_summable_one_div_natCast

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/SequencesSeries.leanTry it in the Lean web editor

A remark for the curious: Mathlib's HasSum asks for unconditional convergence (the sum must not depend on the order of the terms). For the series in this lesson — with terms of one sign, or geometric with $|r| < 1$ — that agrees with the definition by partial sums used above. For a series like $1 - \tfrac12 + \tfrac13 - \tfrac14 + \cdots$ , whose partial sums converge (to $\ln 2$ ) but which can be rearranged to converge to anything, the two notions differ. Proposition 8 is not formalised here.

ComputationC

Partial sums, exactly and numerically

Geometric series: exact partial sums and gapsPythonExact computationExhaustive finite checkComputationally tested

"""Geometric series in exact arithmetic: 1 + 1/2 + 1/4 + ... and 0.999...

With fractions the partial sums S_n = a(1 - r^n)/(1 - r) are computed with no
rounding, so we can watch the gap a/(1 - r) - S_n = a r^n/(1 - r) shrink
exactly: for 1 + 1/2 + 1/4 + ... the gap after n terms is 1/2^(n-1), and for
0.9 + 0.09 + 0.009 + ... it is 1/10^n. For |r| >= 1 the partial sums
oscillate or grow instead, and the terms do not tend to 0.
"""

from fractions import Fraction

def partial_sums(a, r, n):
    """[S_1, ..., S_n] for a + ar + ar^2 + ..., exact for Fractions."""
    if n < 0:
        raise ValueError("n must be non-negative")
    sums, total, term = [], 0 * a, a
    for _ in range(n):
        total += term
        sums.append(total)
        term *= r
    return sums

def closed_form(a, r, n):
    """a(1 - r^n)/(1 - r) for r != 1; n * a when r = 1."""
    if r == 1:
        return n * a
    return a * (1 - r ** n) / (1 - r)

def gap(a, r, n):
    """a/(1 - r) - S_n, the part of the infinite sum still missing."""
    return a / (1 - r) - closed_form(a, r, n)

def terms_needed(a, r, eps):
    """Smallest n with |a/(1 - r) - S_n| < eps (requires |r| < 1)."""
    if not abs(r) < 1:
        raise ValueError("needs |r| < 1")
    n = 0
    while abs(gap(a, r, n)) >= eps:
        n += 1
    return n

def main():
    half, tenth = Fraction(1, 2), Fraction(1, 10)
    print("1 + 1/2 + 1/4 + ...  (a = 1, r = 1/2, limit 2)")
    for n, s in enumerate(partial_sums(Fraction(1), half, 8), start=1):
        print(f"  S_{n} = {str(s):>7}   gap = {str(2 - s)}")
    print()
    print("0.9 + 0.09 + 0.009 + ...  (a = 9/10, r = 1/10, limit 1)")
    for n, s in enumerate(partial_sums(Fraction(9, 10), tenth, 5), start=1):
        print(f"  S_{n} = {float(s):.{n}f}   gap = 1 - S_{n} = {1 - s}")
    print("The gap 1/10^n eventually drops below any positive number, so the")
    print("limit of the partial sums, which is what 0.999... means, is exactly 1.")
    print()
    ok = all(
        partial_sums(Fraction(3), r, 30)[-1] == closed_form(Fraction(3), r, 30)
        for r in (half, -half, Fraction(2, 3), Fraction(-9, 10), Fraction(5))
    )
    print(f"Closed form a(1 - r^n)/(1 - r) agrees with term-by-term sums: {ok}")
    need = terms_needed(Fraction(1), half, Fraction(1, 10 ** 6))
    print(f"Terms of 1 + 1/2 + ... needed to come within 10^-6 of 2: {need}")
    print()
    for r in (1, -1, 2):
        sums = partial_sums(1, r, 8)
        print(f"r = {r:2d}: partial sums {sums} - no limit")
    print()
    print("Epistemic status: exact rational arithmetic for finitely many n;")
    print("the closed form and the limits are proved in the lesson (and in")
    print("Lean); a table of partial sums can only illustrate convergence.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

The exact gaps $\tfrac{1}{2^{n-1}}$ and $\tfrac{1}{10^n}$ are the "error terms" $\tfrac{a\,r^n}{1 - r}$ of Theorem 5's proof, made visible. But a table of finitely many partial sums never proves convergence: it is the formula, valid for every $n$ , together with $r^n \to 0$ , that does.

The harmonic series grows without bound, slowlyPythonExact computationNumerical approximationComputationally tested

"""The harmonic series: terms that shrink to 0, sums that never stop growing.

Oresme's grouping says the block 1/(2^k + 1) + ... + 1/2^(k+1) is at least 1/2;
we compute these blocks exactly with fractions. Then, with 40-digit decimal
arithmetic, we find the first n with H_n = 1 + 1/2 + ... + 1/n > t for
t = 1, ..., 10 (H_n first exceeds 10 at n = 12367) and compare H_n with
ln n + 0.5772 (Euler's constant). By contrast, 1 + 1/4 + 1/9 + ... stays
below 2.
"""

import math
from decimal import Decimal, localcontext
from fractions import Fraction

#: Euler's constant gamma, to 16 digits (used only for comparison).
EULER_GAMMA = 0.5772156649015329

def oresme_block(k):
    """1/(2^k + 1) + ... + 1/2^(k+1), exactly (2^k terms)."""
    if k < 0:
        raise ValueError("k must be non-negative")
    return sum(Fraction(1, j) for j in range(2 ** k + 1, 2 ** (k + 1) + 1))

def harmonic_exact(n):
    """H_n = 1 + 1/2 + ... + 1/n as a Fraction (for small n)."""
    return sum((Fraction(1, j) for j in range(1, n + 1)), Fraction(0))

def first_exceeding(targets):
    """For each target t (increasing), the least n with H_n > t.

    Uses Decimal with 40 significant digits: after 10^5 additions the
    accumulated rounding error is far below the gaps 1/n near the answers.
    """
    answers = []
    with localcontext() as ctx:
        ctx.prec = 40
        total, n = Decimal(0), 0
        for t in targets:
            while total <= t:
                n += 1
                total += Decimal(1) / n
            answers.append(n)
    return answers

def basel_partial(n):
    """1 + 1/4 + ... + 1/n^2 in floating point (math.fsum)."""
    return math.fsum(1.0 / (j * j) for j in range(1, n + 1))

def main():
    print("Oresme's blocks (exact): each block of 2^k terms is at least 1/2")
    for k in range(5):
        block = oresme_block(k)
        terms = f"1/{2 ** k + 1} + ... + 1/{2 ** (k + 1)}" if k else "1/2"
        print(f"  k = {k}: {terms} = {float(block):.4f}"
              f"  >= 1/2: {block >= Fraction(1, 2)}")
    print("So H(2^m) >= 1 + m/2: the partial sums pass every bound.")
    print()
    targets = list(range(1, 11))
    print("t    first n with H_n > t    ln n + gamma")
    for t, n in zip(targets, first_exceeding(targets)):
        print(f"{t:2d}   {n:12d}             {math.log(n) + EULER_GAMMA:.4f}")
    print("The terms 1/n tend to 0, yet the sums still reach any height -")
    print("it takes roughly e^(t - 0.58) terms to reach height t.")
    print()
    for n in [10, 1000, 100000]:
        print(f"1 + 1/4 + ... + 1/{n}^2 = {basel_partial(n):.6f}   (< 2)")
    print(f"pi^2/6 = {math.pi ** 2 / 6:.6f}, Euler's value of the whole sum")
    print()
    print("Epistemic status: the blocks are exact for k <= 4 (the lesson")
    print("proves the bound for all k); the first-exceeding table uses")
    print("40-digit decimals, numerical but with error far below 1/n; the")
    print("ln n + gamma column is an approximation. No finite table proves")
    print("divergence: the grouping argument does.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

The harmonic experiment shows why evidence can mislead in both directions. After $12\,367$ terms the sum has only just passed $10$ , and it creeps upward so slowly that a computer adding a billion terms a second would need longer than the age of the universe to pass $100$ . A computer alone could never show that the series diverges; Oresme's grouping argument does it in four lines.

Exercises

1. Sequences and series

Warm-upHuman

Find the sum of the first $20$ terms of the arithmetic sequence $5, 8, 11, 14, \dots$

2. Sequences and series

Warm-upHuman

Compute $3 + 6 + 12 + 24 + \dots + 3 \cdot 2^{9}$ (ten terms).

3. Sequences and series

Warm-upHuman

A sequence is defined by $a_1 = 2$ and $a_{n+1} = 3a_n - 1$ . What is $a_5$ ?

4. Sequences and series

CoreHuman

Which of these infinite series converge? (Choose all that apply.)

Choose all that apply

\displaystyle\sum_{k=0}^{\infty} \left(\tfrac{2}{3}\right)^k

\displaystyle\sum_{k=0}^{\infty} \left(-\tfrac{9}{10}\right)^k

\displaystyle\sum_{k=0}^{\infty} (-1)^k

\displaystyle\sum_{k=1}^{\infty} \tfrac{1}{k}

\displaystyle\sum_{k=1}^{\infty} \tfrac{1}{k^2}

\displaystyle\sum_{k=0}^{\infty} \left(\tfrac{11}{10}\right)^k

5. Sequences and series

CoreHuman

Write $0.\overline{45} = 0.454545\ldots$ as a geometric series $a + ar + ar^2 + \cdots$ and find its sum $\tfrac pq$ in lowest terms. Enter $q$ .

6. Sequences and series

CoreHuman

A student argues: "The terms $\tfrac{1}{\sqrt k}$ tend to $0$ , so by the term test $\sum_{k=1}^{\infty} \tfrac{1}{\sqrt k}$ converges." What is wrong?

Choose one

The term test only proves divergence; terms tending to

0

prove nothing about convergenceThe terms

\tfrac{1}{\sqrt k}

do not tend to

0

Nothing: the series convergesThe term test only applies to geometric series

7. Sequences and series

StretchHuman

In the proof that the harmonic series diverges, why is $\tfrac{1}{9} + \tfrac{1}{10} + \dots + \tfrac{1}{16} \ge \tfrac12$ ?

Choose one

There are

8

terms, each at least

\tfrac{1}{16}

There are

8

terms, each at least

\tfrac{1}{9}

Because

\tfrac19 > \tfrac12

Because the terms tend to

0

8. Sequences and series

CoreFormal

In Lean, HasSum f S means "the series $\sum_{n \ge 0} f(n)$ converges to $S$ ". Which statement formalises $0.999\ldots = 1$ ?

Choose one

HasSum (fun n : ℕ => (9 : ℝ) / 10 ^ (n + 1)) 1HasSum (fun n : ℕ => (9 : ℝ) / 10 ^ n) 1(0.999 : ℝ) = 1∀ n : ℕ, ∑ k ∈ Finset.range n, (9 : ℝ) / 10 ^ (k + 1) = 1

9. Sequences and series

StretchComputational

Write terms_needed(a, r, eps) for $0 < r < 1$ and $a > 0$ : the smallest $n$ such that the partial sum $S_n = a + ar + \dots + ar^{n-1}$ is within eps of the limit $\tfrac{a}{1 - r}$ . Use Fraction for exact arithmetic (the tests pass fractions). By Theorem 5 the gap is $\tfrac{a\,r^n}{1 - r}$ .

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

"If the terms tend to $0$ , the series converges." The harmonic series $1 + \tfrac12 + \tfrac13 + \cdots$ has terms tending to $0$ and diverges. Terms tending to $0$ is necessary for convergence (Theorem 6), but not sufficient.

Misconception

"An infinite sum of positive numbers must be infinite." $1 + \tfrac12 + \tfrac14 + \cdots = 2$ . What matters is how fast the terms shrink: geometrically shrinking terms add up to a finite total.

Misconception

" $0.999\ldots$ is slightly less than $1$ ." $0.999\ldots$ is the geometric series $\tfrac{9}{10} + \tfrac{9}{100} + \cdots$ , whose sum is exactly $1$ . There is no real number strictly between $0.999\ldots$ and $1$ : any gap would have to be smaller than $10^{-n}$ for every $n$ , hence $0$ .

Misconception

" $1 + r + r^2 + \cdots = \tfrac{1}{1 - r}$ for every $r \ne 1$ ." Only for $|r| < 1$ . For $r = 2$ the formula would give $1 + 2 + 4 + \cdots = -1$ , which is nonsense for real numbers: the partial sums $2^n - 1$ grow without bound. The finite formula $\tfrac{1 - r^n}{1 - r}$ is valid for all $r \ne 1$ ; the infinite one needs $r^n \to 0$ .

Misconception

"A sequence converges if its terms get closer together." $\sqrt n$ has consecutive differences $\sqrt{n + 1} - \sqrt n = \tfrac{1}{\sqrt{n + 1} + \sqrt n} \to 0$ , yet $\sqrt n \to \infty$ . Convergence is about getting close to a fixed limit, not just to the next term.

ViewpointsH

Other ways of seeing

Geometry— Self-similar pictures

Geometric series describe self-similar shapes. In the figure above, the square minus its left half is a half-size copy of a familiar shape, and the series records the copies. The Koch snowflake — repeatedly add an equilateral bump to the middle third of every edge — has perimeter multiplied by $\tfrac43$ at every stage, so its perimeter is infinite ( $r = \tfrac43 > 1$ ), while the areas of the bumps form a geometric series with ratio $\tfrac49$ , so its area is finite: $\tfrac85$ of the starting triangle.

Probability— Waiting for heads

Toss a fair coin until it lands heads. The probability that the first head comes on toss $n$ is $\big(\tfrac12\big)^{n-1}\cdot\tfrac12 = \tfrac{1}{2^n}$ , and these probabilities add up to $\tfrac12 + \tfrac14 + \cdots = 1$ — as total probability must. The expected number of tosses is $\sum_{n \ge 1} \tfrac{n}{2^n} = 2$ , a sum one can find by differentiating the geometric series $\sum x^n = \tfrac{1}{1 - x}$ term by term. Infinite series are the language of probability with infinitely many outcomes.

Number theory— Decimals, and a world where 1 + 2 + 4 + ⋯ = −1

Every decimal $0.d_1d_2d_3\ldots$ is the series $\sum d_k\,10^{-k}$ , and the theory of geometric series is exactly why repeating decimals are fractions. Number theorists also measure size differently: in the $2$ -adic numbers a number is "small" when it is divisible by a high power of $2$ , so $2^n \to 0$ ! There the geometric series formula holds for $r = 2$ and $1 + 2 + 4 + 8 + \cdots = \tfrac{1}{1 - 2} = -1$ is a genuine theorem. This is not a trick about real numbers — in $\R$ that series diverges — but a different notion of distance, and $p$ -adic numbers are central in modern number theory.

Analysis— Convergence without knowing the limit

The definition of convergence needs the limit $L$ in advance. Cauchy found a test that does not: a sequence converges if and only if its terms eventually stay arbitrarily close to each other ( $|s_m - s_n| < \varepsilon$ for all large $m, n$ ). That this works is equivalent to the completeness of $\R$ , the property that also makes increasing bounded sequences converge, as used for $\sum \tfrac1{k^2}$ . Series whose signs alternate bring new subtleties: $1 - \tfrac12 + \tfrac13 - \cdots$ converges to $\ln 2$ , but Riemann proved that its terms can be rearranged to converge to any number you like. See Real analysis.

History & global context

History and global context

Ancient sums. The Egyptian Rhind papyrus (about 1550 BCE) adds the geometric sequence $7, 49, 343, 2401, 16807$ . Zeno of Elea's paradoxes (5th century BCE) raised the question of infinite sums. Archimedes (3rd century BCE) summed $1 + \tfrac14 + \tfrac1{16} + \cdots = \tfrac43$ to find the area of a parabolic segment, by an argument that avoided the infinite through a double reductio ad absurdum.
India. Āryabhaṭa (499 CE) gave rules for arithmetic series and for the sums of squares and cubes. Writers on Sanskrit prosody, from Virahāṅka to Hemachandra (about 1150), counted poetic metres with the recursion now called Fibonacci's. In the 14th century, Mādhava of Saṅgamagrāma and the Kerala school found infinite series such as $\tfrac\pi4 = 1 - \tfrac13 + \tfrac15 - \cdots$ .
Europe. Nicole Oresme proved the divergence of the harmonic series around 1350, by the grouping in Theorem 7. Pietro Mengoli asked for the sum of $\sum \tfrac{1}{k^2}$ in 1650, and Leonhard Euler found $\tfrac{\pi^2}{6}$ in 1734. Augustin-Louis Cauchy's Cours d'analyse (1821) gave the modern definition of convergence through limits of partial sums.

Can you add forever?

Running totals that settle down

Definitions

Worked examples

Explore: watching partial sums

Finite sums

Infinite series

Series in Lean

Partial sums, exactly and numerically

Exercises

Common misconceptions

Other ways of seeing

History and global context

Further reading