Prove2Me

Lemma 13.17: a discrete co-area inequality for the bottleneck ratio

Proved
MarkovMixing.bottleneck_coarea

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

markov-chainprobability

Let PP be an irreducible transition matrix on a finite state space VV, reversible with respect to its stationary distribution π\pi, and write Q(x,y)=π(x)P(x,y)Q(x,y) = \pi(x)P(x,y) for the edge measure and

Φ⋆=min⁡{Q(S,Sc)π(S):S≠∅, π(S)≤12}\Phi_\star = \min\Bigl\{\tfrac{Q(S,S^c)}{\pi(S)} : S \ne \emptyset,\ \pi(S) \le \tfrac12\Bigr\}

for the bottleneck ratio of the chain.

Claim. Let ψ:V→R\psi : V \to \mathbb{R} be nonnegative and suppose its support is small, π{ψ>0}≤12\pi\{\psi > 0\} \le \tfrac12. Then

Φ⋆⋅Eπ(ψ)  ≤  ∑x,y∈V(ψ(x)−ψ(y))+Q(x,y),\Phi_\star \cdot \mathbb E_\pi(\psi) \;\le\; \sum_{x,y \in V} \bigl(\psi(x)-\psi(y)\bigr)^{+} Q(x,y),

where a+=max⁡(a,0)a^{+} = \max(a,0).

In words: the total mass of ψ\psi is controlled by how much ψ\psi decreases across the edges of the chain, at the rate set by the worst bottleneck. It is a discrete co-area inequality — the proof applies the definition of Φ⋆\Phi_\star to each super-level set St={ψ>t}S_t = \{\psi > t\}, which is legitimate because St⊆{ψ>0}S_t \subseteq \{\psi > 0\} has stationary measure at most 12\tfrac12, and then integrates the resulting bound Φ⋆ π{ψ>t}≤∑x,yQ(x,y)1{ψ(x)>t≥ψ(y)}\Phi_\star\,\pi\{\psi>t\} \le \sum_{x,y} Q(x,y)\mathbb 1\{\psi(x) > t \ge \psi(y)\} over t∈(0,∞)t \in (0,\infty), using ∫0∞1{ψ(x)>t≥ψ(y)} dt=(ψ(x)−ψ(y))+\int_0^\infty \mathbb 1\{\psi(x)>t\ge\psi(y)\}\,dt = (\psi(x)-\psi(y))^{+}.

This is Lemma 13.17 of Levin--Peres--Wilmer, the engine behind the hard half Φ⋆2/2≤γ\Phi_\star^2/2 \le \gamma of the discrete Cheeger inequality: applied to ψ=f2\psi = f^2, where ff is the positive part of a λ2\lambda_2-eigenfunction, together with the Cauchy--Schwarz inequality it converts the bottleneck ratio into a bound on the Dirichlet form.

Formalization note. LPW state the right-hand side as ∑x<y[ψ(x)−ψ(y)]Q(x,y)\sum_{x<y}[\psi(x)-\psi(y)]Q(x,y) after choosing a linear order on VV that makes ψ\psi non-increasing. For such an order, and using the symmetry of QQ, that sum equals the order-free expression above: pairs with ψ(x)≤ψ(y)\psi(x) \le \psi(y) contribute nothing to either side.

Preamble
import Definitions.Def_mm_spectral
import Definitions.Def_mm_lower
Formal statement
namespace MarkovMixing

/-- **Lemma 13.17** (LPW): for a nonnegative `ψ` supported on a set of
stationary measure at most `1/2`, the mean of `ψ` is controlled by the
`Q`-weighted total decrease of `ψ` across edges, at rate `Φ⋆`:
`Φ⋆ · E_π(ψ) ≤ ∑_{x,y} (ψ(x) − ψ(y))⁺ Q(x,y)`.  LPW order the state space so
that `ψ` is non-increasing and sum over `x < y`; taking positive parts makes
the statement independent of that ordering. -/
theorem bottleneck_coarea {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V]
    (P : Matrix V V ℝ) (hP : IsStochastic P) (hirr : Irreducible P)
    (π : V → ℝ) (hπ : IsStationary P π) (hrev : DetailedBalance P π)
    (ψ : V → ℝ) (hψ : ∀ x : V, 0 ≤ ψ x)
    (hsupp : ∑ x ∈ Finset.univ.filter (fun x : V => 0 < ψ x), π x ≤ 2⁻¹) :
    bottleneckStar P π * distExp π ψ ≤
      ∑ x, ∑ y, max (ψ x - ψ y) 0 * edgeMeasure P π x y := 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 13.3.3, Lemma 13.17, p. 178 (the sum over x<y for a psi-decreasing order is rewritten order-free with positive parts)

View graph