Proposition 2.3 -- the coupon collector's expected time

Open

MarkovMixing.coupon_expectation

by Shuze Chen · Aug 21, 2026 · Mathlib c5ea003 (Lean v4.30.0)

markov-chainsmixing-timesprobability

The expected number of independent uniform draws needed to collect all $n$ coupon types is

\mathbb{E}(\tau)=n\sum_{k=1}^n\frac{1}{k},

where $\mathbb{E}(\tau)$ is encoded by the tail-sum $\sum_{t\ge0}\mathbb{P}\{\tau>t\}$ and $\mathbb{P}\{\tau>t\}$ is the fraction of draw sequences of length $t$ that miss some type.

Preamble

import Definitions.Def_mm_classical

Formal statement

namespace MarkovMixing

/-- **Proposition 2.3** (LPW): the expected number of uniform draws needed to
collect all `n` coupon types is `n ∑_{k=1}^n 1/k`. -/
theorem coupon_expectation (n : ℕ) (hn : 1 ≤ n) :
    couponExpTime n = n * ∑ k ∈ Finset.Icc 1 n, (1 : ℝ) / k := by
  sorry

end MarkovMixing

Source

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, AMS 2009, https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf, Section 2.2, Proposition 2.3, p. 22

Read-back

What the Lean code literally says, in plain math · claude-fable-5

For every natural number $n$ with $1 \le n$ , the statement asserts the equality of real numbers

T(n) \;=\; n \cdot \sum_{k=1}^{n} \frac{1}{k},

where the right-hand side is the natural number $n$ (cast to $\mathbb{R}$ ) times the sum of $1/k$ over the integers $k$ in the closed interval $[1, n]$ (each $k$ cast to $\mathbb{R}$ before taking the reciprocal), and $T(n)$ abbreviates the custom quantity couponExpTime n, defined as the infinite series

T(n) \;=\; \sum_{t=0}^{\infty} q(n, t), \qquad q(n, t) \;=\; \frac{\#\{\, d : \{0,\dots,t-1\} \to \{0,\dots,n-1\} \mid d \text{ is not surjective} \,\}}{n^{t}},

i.e. $q(n,t)$ (couponMissProb n t) is the number of functions from a $t$ -element set to an $n$ -element set that fail to be surjective, cast to $\mathbb{R}$ and divided by the real number $n^t$ . Two conventions of the encoding are worth noting: the infinite sum is Lean's tsum, which equals the limit of the series when the family is summable and is defined to be $0$ when it is not summable, so the statement as written equates the right-hand side with $0$ in any case where the series $\sum_t q(n,t)$ fails to converge; and for $t = 0$ the counting set consists of the single empty function, which is not surjective onto a nonempty codomain, so $q(n,0) = 1$ for $n \ge 1$ (while $n^0 = 1$ avoids division by zero; the hypothesis $n \ge 1$ also rules out the degenerate denominator case $n = 0$ with $t \ge 1$ ). No probability-theory structure is involved: the "expected time" is this explicitly defined series of counting ratios, not an expectation with respect to any formal probability measure, and the theorem claims exactly the equality displayed above, for every $n \ge 1$ .

Human review

Endorsed by Community (Bot) · Aug 21, 2026
Endorsed by Shuze Chen · Aug 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph