The gambler's ruin chain, the coupon collector, and simple random walk on $\mathbb{Z}$

Definition

mm_classical

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

markov-chainsmixing-timesprobability

This file presents the classical chains of Chapter 2 of Levin-Peres-Wilmer directly through their driving randomness, so that all probabilities are elementary counting.

The gambler's ruin chain on $\{0,1,\dots,n\}$ moves from each interior state to its two neighbours with probability $\tfrac12$ each and is absorbed at $0$ and at $n$ .

For the coupon collector with $n$ types, the probability $\mathbb P\{\tau>t\}$ that $t$ independent uniform draws fail to collect every type is the fraction of the $n^t$ draw sequences $d:\{1,\dots,t\}\to\{1,\dots,n\}$ that are not surjective, and the expected collection time $\mathbb E(\tau)$ is the tail sum $\sum_{t\ge0}\mathbb P\{\tau>t\}$ , an infinite series with the convention that a non-summable family sums to $0$ .

Simple random walk on $\mathbb Z$ started at $k$ is presented by sign strings: to a string $\omega\in\{\pm1\}^r$ of steps is associated the deterministic position $k+\sum_{i<\min(t,r)}\omega_i$ after $t$ steps, and probabilities of walk events are counts of the $2^r$ equally likely sign strings, taken in the theorems that use these definitions.

Definition code

import Definitions.Def_mm_path
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.SpecialFunctions.Sqrt

/-!
The classical chains of Levin–Peres–Wilmer, *Markov Chains and Mixing Times*,
Chapter 2: the gambler's ruin chain (§2.1), the coupon-collector process
(§2.2), and simple random walk on `ℤ` (§2.7).

The coupon collector and the walk on `ℤ` are presented directly by their
driving randomness — uniform draws `Fin t → Fin n`, respectively uniform sign
sequences `Fin r → Bool` — so that all probabilities are elementary counting.
-/

namespace MarkovMixing

noncomputable section

open scoped BigOperators

/-- The **gambler's ruin** chain on `{0, 1, …, n}`: fair ±1 steps at the
interior states, absorption at `0` and at `n` (LPW §2.1). -/
def gamblersChain (n : ℕ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ :=
  fun k l =>
    if k = 0 ∨ k = Fin.last n then (if l = k then 1 else 0)
    else if l.val = k.val + 1 ∨ l.val + 1 = k.val then 1 / 2 else 0

/-- `P{τ > t}` for the **coupon collector** with `n` coupon types: the
probability that `t` independent uniform draws miss at least one type, i.e.
the fraction of functions `Fin t → Fin n` that are not surjective (LPW §2.2). -/
def couponMissProb (n t : ℕ) : ℝ :=
  ((Finset.univ.filter fun d : Fin t → Fin n => ¬Function.Surjective d).card : ℝ) / n ^ t

/-- `E(τ)` for the coupon collector with `n` types, via the tail-sum formula
`E τ = ∑_{t ≥ 0} P{τ > t}` (LPW §2.2). -/
def couponExpTime (n : ℕ) : ℝ :=
  ∑' t : ℕ, couponMissProb n t

/-- The position at time `t` of the **simple random walk on `ℤ`** started at
`k`, driven by the sign sequence `ω` (`true` = step `+1`, `false` = step `-1`);
each `ω : Fin r → Bool` is equally likely (LPW §2.7). -/
def srwPos {r : ℕ} (k : ℤ) (ω : Fin r → Bool) (t : ℕ) : ℤ :=
  k + ∑ i : Fin r, if (i : ℕ) < t then (if ω i then 1 else -1) else 0

end

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, Sections 2.1, 2.2 and 2.7

Read-back

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

Read-back: Def_mm_classical

gamblersChain. For every natural number $n$ , this defines a real-valued square matrix $G$ indexed by the $n+1$ states $\{0, 1, \dots, n\}$ . Its entry $G(k, \ell)$ is determined by cases on the row index $k$ : if $k = 0$ or $k = n$ (the two endpoint states), the row is that of an absorbing state — $G(k, \ell) = 1$ when $\ell = k$ and $G(k, \ell) = 0$ otherwise; for every other row index $k$ (so $0 < k < n$ ), the entry is $G(k, \ell) = \tfrac{1}{2}$ when $\ell = k + 1$ or $\ell + 1 = k$ (i.e. $\ell$ is the immediate right or left neighbor of $k$ , as natural numbers), and $0$ otherwise. Note the degenerate case $n = 0$ : there is a single state $0$ , which is simultaneously both endpoints, and the matrix is the $1 \times 1$ identity. When $n = 1$ both states are endpoints and the matrix is the $2 \times 2$ identity. No claim is made here that this matrix is stochastic; it is simply this explicit matrix of reals.

couponMissProb. For all natural numbers $n$ and $t$ , this defines the real number

\mathrm{couponMissProb}(n, t) \;=\; \frac{\#\{\,d : \{1,\dots,t\} \to \{1,\dots,n\} \;\mid\; d \text{ is not surjective}\,\}}{n^{t}},

that is: the number of functions from a $t$ -element index set to an $n$ -element set that fail to be surjective (fail to hit every one of the $n$ values), divided by $n^t$ . Both numerator and denominator are cast to real numbers and the division is real division. Edge cases forced by the totality conventions: when $t = 0$ and $n \ge 1$ , the unique empty function is not surjective, so the value is $1/n^0 = 1$ ; when $n = 0$ and $t = 0$ , the unique function between empty types is (vacuously) surjective and $0^0 = 1$ , so the value is $0$ ; when $n = 0$ and $t \ge 1$ there are no such functions at all and the denominator $0^t$ is $0$ , so the expression is $0/0$ , which by the convention for real division equals $0$ .

couponExpTime. For every natural number $n$ , this defines the real number

\mathrm{couponExpTime}(n) \;=\; \sum_{t=0}^{\infty} \mathrm{couponMissProb}(n, t),

the sum over all natural numbers $t \ge 0$ of the quantity defined above (the fraction of functions from a $t$ -element set to an $n$ -element set that are not surjective). The infinite sum is the topological sum operator: if the family of terms is not summable, the expression takes the junk value $0$ by convention rather than $+\infty$ ; it equals the limit of the partial sums only when the family is summable. For $n = 0$ the terms are $0$ for all $t \ge 1$ and $0$ at $t = 0$ , so the sum is $0$ .

srwPos. For an implicit natural number $r$ , an integer $k$ , a function $\omega : \{0, \dots, r-1\} \to \{\mathrm{true}, \mathrm{false}\}$ (a string of $r$ Booleans), and a natural number $t$ , this defines the integer

\mathrm{srwPos}(k, \omega, t) \;=\; k \;+\; \sum_{i=0}^{r-1} \begin{cases} +1 & \text{if } i < t \text{ and } \omega_i = \mathrm{true},\\ -1 & \text{if } i < t \text{ and } \omega_i = \mathrm{false},\\ 0 & \text{if } i \ge t. \end{cases}

In words: starting from $k$ , each of the first $\min(t, r)$ coordinates of $\omega$ contributes a step of $+1$ (if that coordinate is true) or $-1$ (if false), and coordinates with index $\ge t$ contribute nothing. In particular, when $t \ge r$ all $r$ coordinates contribute, and increasing $t$ beyond $r$ changes nothing; when $t = 0$ or $r = 0$ the value is just $k$ . This is a plain arithmetic expression in the given data; no probability measure or randomness is defined here.

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

The gambler's ruin chain, the coupon collector, and simple random walk on Z\mathbb{Z}Z

Read-back: Def_mm_classical

The gambler's ruin chain, the coupon collector, and simple random walk on $\mathbb{Z}$