Evolving-set mixing bound (Morris--Peres)

Proved

MarkovMixing.evolving_sets_mixing

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

markov-chainsmixing-timesprobability

Let $P$ be an irreducible Markov chain on a finite state space $V$ that is lazy — $P(x,x)\ge\tfrac12$ at every state — with stationary distribution $\pi$ ; write $\pi_{\min}=\min_x\pi(x)$ . Reversibility is not assumed. The bottleneck constant (Mission IV) is

\Phi_\star=\min\Bigl\{\frac{\sum_{x\in S,\,y\notin S}\pi(x)P(x,y)}{\pi(S)}\;:\;\varnothing\ne S\subseteq V,\ \pi(S)\le\tfrac12\Bigr\},

the worst conditional escape probability of a half-space at stationarity. For a tolerance $\varepsilon$ , the mixing time $t_{\mathrm{mix}}(\varepsilon)$ is the first $t$ with $\max_x\|P^t(x,\cdot)-\pi\|_{TV}\le\varepsilon$ , where $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$ is the total variation distance.

The theorem (Theorem 17.10, Morris–Peres; Levin–Peres–Wilmer — the capstone of Chapter 17) asserts: for every $0<\varepsilon<1$ ,

t_{\mathrm{mix}}(\varepsilon)\;\le\;\Bigl\lceil\frac{2}{\Phi_\star^{2}}\,\log\Bigl(\frac{1}{\varepsilon\,\pi_{\min}}\Bigr)\Bigr\rceil

(the ceiling absorbs the rounding of the real-valued bound to an integer time).

For reversible chains this recovers the Cheeger-route bound of Mission VII — but no reversibility is needed, which is the theorem's point: geometry controls mixing for every lazy chain. The proof analyzes the evolving-set process of this mission: laziness keeps the thresholds tame, the bottleneck constant forces a per-step multiplicative decay of $\mathbb E\sqrt{\pi(S_t)(1-\pi(S_t))}$ , and the identity $P^t(x,y)=\tfrac{\pi(y)}{\pi(x)}\mathbb P_{\{x\}}\{y\in S_t\}$ converts that decay into total-variation mixing.

Preamble

import Definitions.Def_mm_martingale
import Mathlib.Analysis.SpecialFunctions.Log.Basic

Formal statement

namespace MarkovMixing

/-- **Theorem 17.10** (Morris–Peres; LPW), the capstone of Chapter 17: for a
lazy irreducible chain (no reversibility required!),
`t_mix(ε) ≤ ⌈(2/Φ⋆²) log(1/(ε π_min))⌉` (the ceiling absorbs
integer rounding). -/
theorem evolving_sets_mixing {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V]
    (P : Matrix V V ℝ) (hP : IsStochastic P) (hirr : Irreducible P)
    (hlazy : ∀ x : V, 2⁻¹ ≤ P x x)
    (π : V → ℝ) (hπ : IsStationary P π)
    (ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1) :
    (mixingTime P π ε : ℝ) ≤
      ⌈2 / bottleneckStar P π ^ 2 * Real.log (1 / (ε * ⨅ x : V, π x))⌉₊ := 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 17.4, Theorem 17.10, p. 235

Read-back

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

Read-back: `evolving_sets_mixing`

Let $V$ be a finite, nonempty type with decidable equality, and let $P$ be a $V \times V$ real matrix subject to three hypotheses:

Stochastic: every entry satisfies $P(x,y) \ge 0$ , and every row sums to $1$ : $\sum_y P(x,y) = 1$ for all $x$ .
Irreducible: for every ordered pair $x, y \in V$ there exists $t \in \mathbb{N}$ with $(P^t)(x,y) > 0$ . (The exponent $t = 0$ is allowed, and $P^0$ is the identity, so for $x = y$ this condition is automatically satisfiable by $t = 0$ ; the content is for $x \ne y$ .)
Laziness: $P(x,x) \ge \tfrac12$ for every $x \in V$ .

Let $\pi : V \to \mathbb{R}$ be stationary for $P$ : $\pi$ is a probability vector ( $\pi(x) \ge 0$ for all $x$ and $\sum_x \pi(x) = 1$ ) and the row-vector product satisfies $\pi P = \pi$ . Let $\varepsilon$ be a real number with $0 < \varepsilon < 1$ .

The conclusion is the inequality

t_{\mathrm{mix}}(\varepsilon) \;\le\; \Bigl\lceil \frac{2}{\Phi_\star^{2}} \cdot \log\!\frac{1}{\varepsilon \cdot \pi_{\min}} \Bigr\rceil_{\mathbb{N}},

where every symbol unfolds as follows.

$t_{\mathrm{mix}}(\varepsilon)$ is the mixing time: the least natural number $t$ such that

d(t) \;=\; \sup_{x \in V}\; \sup_{A \subseteq V} \Bigl|\, \sum_{y \in A} (P^{t})(x,y) - \sum_{y \in A} \pi(y) \Bigr| \;\le\; \varepsilon,

the suprema being over the finite $V$ and its subsets. If no time $t$ satisfies this, the infimum of the empty set of naturals is the junk value $0$ . The left-hand side is this natural number cast to $\mathbb{R}$ .

$\Phi_\star$ is the bottleneck ratio: the infimum, over all subsets $S \subseteq V$ that are nonempty and satisfy $\pi(S) := \sum_{x \in S}\pi(x) \le \tfrac12$ , of

\Phi(S) \;=\; \frac{\displaystyle\sum_{x \in S}\sum_{y \notin S} \pi(x)\, P(x,y)}{\displaystyle\sum_{x \in S} \pi(x)} .

Division here is total real division: if $\pi(S) = 0$ (possible, since $\pi$ is only assumed nonnegative), then $\Phi(S) = 0$ . Moreover, if no subset meets the two side conditions — e.g. when $V$ has exactly one element, so the only nonempty $S$ has $\pi(S) = 1 > \tfrac12$ — the infimum is taken over an empty family and equals the real junk value $\inf \varnothing = 0$ .

$\pi_{\min} = \inf_{x \in V} \pi(x)$ , a genuine minimum over the finite nonempty $V$ .
$\log$ is the real natural logarithm, and $\lceil \cdot \rceil_{\mathbb{N}}$ is the natural-number ceiling, which sends every nonpositive real to $0$ .

Two junk-value interactions materially shape the edge cases of the right-hand side. First, $2/\Phi_\star^2$ uses total division, so if $\Phi_\star = 0$ (which occurs both when the infimum family is empty and when some admissible $S$ has boundary flow or measure making the infimum $0$ ) then $2/\Phi_\star^2 = 2/0 = 0$ , and the whole right-hand side becomes $\lceil 0 \rceil_{\mathbb{N}} = 0$ , so the claim then asserts $t_{\mathrm{mix}}(\varepsilon) \le 0$ , i.e. $t_{\mathrm{mix}}(\varepsilon) = 0$ . Second, the hypotheses as stated do not force $\pi_{\min} > 0$ ; if $\pi_{\min} = 0$ then $1/(\varepsilon\,\pi_{\min}) = 1/0 = 0$ and $\log 0 = 0$ (both by convention), again collapsing the right-hand side to $0$ . When $\Phi_\star > 0$ and $\pi_{\min} > 0$ , the right-hand side is the ordinary ceiling of $\frac{2}{\Phi_\star^2}\,\log\frac{1}{\varepsilon\,\pi_{\min}}$ (a positive quantity, since $\varepsilon\,\pi_{\min} < 1$ ).

Human review

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

View graph

Evolving-set mixing bound (Morris--Peres)

Read-back: evolving_sets_mixing

Read-back: `evolving_sets_mixing`