Section 4.5 -- standard mixing-time inequalities

Proved

MarkovMixing.mixing_time_eps

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

markov-chainsmixing-timesprobability

Let $P$ be an irreducible, aperiodic Markov chain on a finite state space $V$ with stationary distribution $\pi$ . Write $P^t(x,\cdot)$ for the distribution at time $t$ started at $x$ , $\|\mu-\nu\|_{TV}=\max_{A\subseteq V}|\mu(A)-\nu(A)|$ for the total variation distance, and

d(t)=\max_{x\in V}\bigl\|P^t(x,\cdot)-\pi\bigr\|_{TV}

for the worst-case distance to stationarity. For a tolerance $\varepsilon$ , the mixing time is the first time this distance drops to $\varepsilon$ ,

t_{\mathrm{mix}}(\varepsilon)=\min\{t\in\mathbb N: d(t)\le\varepsilon\},\qquad t_{\mathrm{mix}}=t_{\mathrm{mix}}(1/4).

The theorem asserts, for any tolerance $0<\varepsilon\le1$ , the two standard consequences of submultiplicativity (displays (4.34)–(4.36) of Levin–Peres–Wilmer). First, running the chain for $\ell$ blocks of length $t_{\mathrm{mix}}(\varepsilon)$ shrinks the distance geometrically:

d\bigl(\ell\cdot t_{\mathrm{mix}}(\varepsilon)\bigr)\le(2\varepsilon)^{\ell}\qquad\text{for every }\ell\in\mathbb N.

Second, mixing to any tolerance costs only logarithmically many standard mixing times:

t_{\mathrm{mix}}(\varepsilon)\;\le\;\bigl\lceil\log_2\varepsilon^{-1}\bigr\rceil\;t_{\mathrm{mix}}.

This is why the convention $\varepsilon=1/4$ is harmless: any other tolerance changes the mixing time by at most a logarithmic factor.

Preamble

import Definitions.Def_mm_mixing
import Mathlib.Analysis.SpecialFunctions.Log.Base

Formal statement

namespace MarkovMixing

/-- **§4.5, Eqs. (4.34)–(4.36)** (LPW): for an irreducible aperiodic chain,
`d(ℓ · t_mix(ε)) ≤ (2ε)^ℓ`, and consequently
`t_mix(ε) ≤ ⌈log₂ ε⁻¹⌉ · t_mix`. -/
theorem mixing_time_eps {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V]
    (P : Matrix V V ℝ) (hP : IsStochastic P) (hirr : Irreducible P)
    (hap : Aperiodic P) (π : V → ℝ) (hπ : IsStationary P π)
    (ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1) :
    (∀ ℓ : ℕ, distStationary P π (ℓ * mixingTime P π ε) ≤ (2 * ε) ^ ℓ) ∧
    mixingTime P π ε ≤ ⌈Real.logb 2 ε⁻¹⌉₊ * tMix P π := 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 4.5, Eqs. (4.34)-(4.36), p. 55

Read-back

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

Let $V$ be a finite, nonempty set and let $P$ be a $V \times V$ matrix of real numbers that is stochastic, meaning every entry satisfies $P(x,y) \ge 0$ and every row sums to $1$ ( $\sum_y P(x,y) = 1$ for each $x$ ). Assume $P$ is irreducible in the sense that for every ordered pair of states $x, y$ there exists a natural number $t \ge 0$ with $(P^t)(x,y) > 0$ (note $t = 0$ is allowed, so for $x = y$ this condition is automatic since $P^0$ is the identity). Assume $P$ is aperiodic in the following custom sense: for every state $x$ , the quantity $\operatorname{per}(x) := \sup\{d \in \mathbb{N} : d \text{ divides every } t \in R_x\}$ equals $1$ , where $R_x = \{t \ge 1 : (P^t)(x,x) > 0\}$ is the set of return times of $x$ ; here the supremum is taken in $\mathbb{N}$ , with the convention that the supremum of an unbounded or empty-bounded situation is the junk value $0$ (in particular, if $R_x = \varnothing$ the divisor set is all of $\mathbb{N}$ and $\operatorname{per}(x) = 0 \ne 1$ , so the aperiodicity hypothesis forces every state to have at least one return time). Let $\pi : V \to \mathbb{R}$ be stationary for $P$ , meaning $\pi$ is a probability distribution ( $\pi(x) \ge 0$ for all $x$ and $\sum_x \pi(x) = 1$ ) and the row vector $\pi$ satisfies $\pi P = \pi$ . Finally, let $\varepsilon$ be a real number with $0 < \varepsilon \le 1$ .

Define the total-variation-style distance between two functions $\mu, \nu : V \to \mathbb{R}$ as

\operatorname{tv}(\mu, \nu) = \sup_{A \subseteq V} \Bigl| \sum_{x \in A} \mu(x) - \sum_{x \in A} \nu(x) \Bigr|,

the supremum over all (finite) subsets $A$ of $V$ of the absolute difference of the masses of $A$ (note this is the sup of $|\mu(A) - \nu(A)|$ , without the factor $\tfrac12$ sometimes used for total variation). Define the distance-to-stationarity at time $t \in \mathbb{N}$ as

d(t) = \sup_{x \in V} \operatorname{tv}\bigl((P^t)(x, \cdot),\, \pi\bigr),

the worst case over starting states $x$ of the distance between row $x$ of $P^t$ and $\pi$ . Define the mixing time at level $\delta$ as

t_{\mathrm{mix}}(\delta) = \inf\{t \in \mathbb{N} : d(t) \le \delta\},

an infimum over natural numbers, with the convention that the infimum of the empty set is $0$ — so if $d(t)$ never drops to $\delta$ or below, $t_{\mathrm{mix}}(\delta)$ is $0$ , not $\infty$ . Write $t_{\mathrm{mix}} = t_{\mathrm{mix}}(1/4)$ for the mixing time at the fixed level $\tfrac14$ .

Under all these hypotheses, the theorem asserts the conjunction of two claims:

For every natural number $\ell \ge 0$ ,

d\bigl(\ell \cdot t_{\mathrm{mix}}(\varepsilon)\bigr) \le (2\varepsilon)^{\ell},

where $\ell \cdot t_{\mathrm{mix}}(\varepsilon)$ is the product of natural numbers. (For $\ell = 0$ this reads $d(0) \le 1$ ; note the base of the exponential is $2\varepsilon$ , not $\varepsilon$ , and $2\varepsilon$ may be as large as $2$ since $\varepsilon$ is only assumed $\le 1$ , in which case the bound grows with $\ell$ .)

t_{\mathrm{mix}}(\varepsilon) \le \bigl\lceil \log_2(\varepsilon^{-1}) \bigr\rceil \cdot t_{\mathrm{mix}},

where $\lceil \cdot \rceil$ is the ceiling taken as a natural number (any nonpositive real value is clamped to $0$ ). In particular, when $\varepsilon = 1$ the right-hand side is $0$ and the claim becomes $t_{\mathrm{mix}}(1) = 0$ ; and $\log_2$ here is the real base-2 logarithm, which takes the junk value $0$ at $0$ .

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