Proposition 7.8 -- the distinguishing statistic bound

Disproved

MarkovMixing.distinguishing_statistic

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

markov-chainsmixing-timesprobability

Let $\mu$ and $\nu$ be probability distributions on a finite state space $V$ , and let $f:V\to\mathbb R$ be any statistic. Write $\mathbb E_\mu(f)=\sum_xf(x)\mu(x)$ and $\operatorname{Var}_\mu(f)=\sum_x(f(x)-\mathbb E_\mu(f))^2\mu(x)$ for mean and variance under $\mu$ , $\|\mu-\nu\|_{TV}=\max_{A\subseteq V}|\mu(A)-\nu(A)|$ for the total variation distance, and set $\sigma^2=\tfrac12\bigl[\operatorname{Var}_\mu(f)+\operatorname{Var}_\nu(f)\bigr]$ , the averaged spread of $f$ under the two distributions.

The theorem (Proposition 7.8 of Levin–Peres–Wilmer) asserts: if the statistic separates the two means by $r\ge0$ standard deviations, $\bigl|\mathbb E_\mu(f)-\mathbb E_\nu(f)\bigr|\ge r\,\sigma$ , then

\|\mu-\nu\|_{TV}\;\ge\;1-\frac{4}{4+r^2}.

This is the engine of the distinguishing statistic method for lower bounds: to show a chain is far from mixed at time $t$ , exhibit one observable whose value under $P^t(x,\cdot)$ and under $\pi$ differs by many standard deviations — as the Hamming weight does on the hypercube in this mission.

Retired — this statement is false as written, and the gap is the book's

Replaced by MarkovMixing.distinguishing_statistic_nondegenerate. Disproved by chenmin (accepted).

Proposition 7.8 as printed carries no non-degeneracy hypothesis, and without one it is false — this is not an artifact of formalizing in Lean. Take $\Omega$ a single point, $\mu=\nu$ the point mass and $f=0$ : both variances vanish and the means agree, so the hypothesis $r\sigma\le|E_\mu f-E_\nu f|$ reads $0\le0$ and holds for every $r$ , while at $r=5$ the conclusion demands $\tfrac{25}{29}\le\|\mu-\nu\|_{TV}=0$ .

The book's proof assumes what its statement omits: it opens with "assume that $m_\alpha>m_\beta$ " and finishes through $\|\alpha-\beta\|_{TV}\ge1-\sigma^2/(\sigma^2+M^2)$ with $M=|E_\mu f-E_\nu f|/2$ , a step that needs $\sigma^2+M^2>0$ . The replacement adds the proof's own assumption, $E_\mu(f)\ne E_\nu(f)$ .

Preamble

import Definitions.Def_mm_lower
import Mathlib.Analysis.SpecialFunctions.Sqrt

Formal statement

namespace MarkovMixing

/-- **Proposition 7.8** (LPW): if a statistic `f` separates the means of `μ`
and `ν` by `r` standard deviations, in the sense that
`|E_μ(f) − E_ν(f)| ≥ r σ` with `σ² = [Var_μ(f) + Var_ν(f)]/2`, then
`‖μ − ν‖_TV ≥ 1 − 4/(4 + r²)`. -/
theorem distinguishing_statistic {V : Type*} [Fintype V] [DecidableEq V]
    (μ ν : V → ℝ) (hμ : IsDist μ) (hν : IsDist ν) (f : V → ℝ)
    (r : ℝ) (hr : 0 ≤ r)
    (h : r * Real.sqrt ((distVar μ f + distVar ν f) / 2) ≤
      |distExp μ f - distExp ν f|) :
    1 - 4 / (4 + r ^ 2) ≤ tvDist μ ν := 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 7.3, Proposition 7.8, p. 92

Read-back

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

Let $V$ be a finite type with decidable equality, and let $\mu, \nu : V \to \mathbb{R}$ be two functions that are each assumed to be probability distributions in the following sense: every value is nonnegative and the values sum to $1$ over all of $V$ (call this condition IsDist; note that it is unsatisfiable when $V$ is empty, in which case the theorem is vacuous). Let $f : V \to \mathbb{R}$ be an arbitrary real-valued function on $V$ , and let $r$ be a real number with $r \ge 0$ . Write $\mathbb{E}_\mu[f] = \sum_{x \in V} f(x)\,\mu(x)$ for the mean of $f$ under $\mu$ , and $\mathrm{Var}_\mu(f) = \sum_{x \in V} (f(x) - \mathbb{E}_\mu[f])^2\,\mu(x)$ for the variance (both defined by these explicit sums, valid for any $\mu$ ), and similarly for $\nu$ . The theorem assumes the separation hypothesis

r \cdot \sqrt{\frac{\mathrm{Var}_\mu(f) + \mathrm{Var}_\nu(f)}{2}} \;\le\; \bigl|\mathbb{E}_\mu[f] - \mathbb{E}_\nu[f]\bigr|,

where $\sqrt{\cdot}$ is the real square root (returning $0$ on negative inputs, though here the variances are nonnegative since $\mu,\nu$ are nonnegative). Under these hypotheses it concludes

1 - \frac{4}{4 + r^2} \;\le\; d_{\mathrm{TV}}(\mu, \nu),

where the total-variation distance is defined as $d_{\mathrm{TV}}(\mu,\nu) = \sup_{A \subseteq V} \left| \sum_{x \in A} \mu(x) - \sum_{x \in A} \nu(x) \right|$ , the supremum ranging over all finite subsets $A$ of $V$ (including the empty set); since $V$ is finite this is a maximum over all subsets. Note there is no factor of $\tfrac{1}{2}$ and no sum of pointwise absolute differences in this definition — it is the supremum-over-events form. Edge cases: when $r = 0$ the hypothesis reduces to $0 \le |\mathbb{E}_\mu[f] - \mathbb{E}_\nu[f]|$ , which always holds, and the conclusion becomes the trivial bound $0 \le d_{\mathrm{TV}}(\mu,\nu)$ ; the inequality in both hypothesis and conclusion is non-strict ( $\le$ ).

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