Lemma 7.9 -- projections do not increase total variation

Proved

MarkovMixing.projection_lower_bound

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$ , let $f:V\to\Lambda$ be any map to a finite set $\Lambda$ , and write $f_*\mu$ for the pushforward of $\mu$ along $f$ — the law of the statistic, $(f_*\mu)(b)=\sum_{a:f(a)=b}\mu(a)$ . Let $\|\mu-\nu\|_{TV}=\max_{A}|\mu(A)-\nu(A)|$ denote the total variation distance (on $V$ or on $\Lambda$ as appropriate).

The theorem (Lemma 7.9 of Levin–Peres–Wilmer) asserts that projecting can only lose information:

\bigl\|f_*\mu-f_*\nu\bigr\|_{TV}\;\le\;\|\mu-\nu\|_{TV}.

Consequently any lower bound on the distance between the projected laws — for instance one produced by the distinguishing-statistic inequality applied on $\Lambda$ — is automatically a lower bound on the distance between the original distributions. This is the step that turns observable-level separations into total-variation lower bounds for chains.

Preamble

import Definitions.Def_mm_lower

Formal statement

namespace MarkovMixing

/-- **Lemma 7.9** (LPW): projecting by a statistic `f : Ω → Λ` can only
decrease total variation distance:
`‖μ f⁻¹ − ν f⁻¹‖_TV ≤ ‖μ − ν‖_TV`. -/
theorem projection_lower_bound {V : Type*} [Fintype V] [DecidableEq V]
    {Λ : Type*} [Fintype Λ] [DecidableEq Λ]
    (μ ν : V → ℝ) (hμ : IsDist μ) (hν : IsDist ν) (f : V → Λ) :
    tvDist (pushforward μ f) (pushforward ν f) ≤ 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, Lemma 7.9, pp. 92-93

Read-back

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

Let $V$ and $\Lambda$ both be finite types with decidable equality, and let $\mu, \nu : V \to \mathbb{R}$ be two functions that are each assumed to be probability distributions in the sense that all their values are nonnegative and their values sum to $1$ over $V$ (a condition that is unsatisfiable when $V$ is empty, making the theorem vacuous in that case; no assumption at all is placed on whether $\Lambda$ is empty beyond finiteness — though if $V$ is nonempty then $f$ forces $\Lambda$ to be nonempty too). Let $f : V \to \Lambda$ be an arbitrary function, with no further hypotheses. For a function $\mu$ on $V$ , its pushforward along $f$ is the function $f_*\mu : \Lambda \to \mathbb{R}$ defined pointwise by $f_*\mu(b) = \sum_{a \in V,\, f(a) = b} \mu(a)$ , the sum of $\mu$ over the fiber of $b$ (an empty sum, hence $0$ , when $b$ has no preimage). The total-variation distance used here is defined, for two real-valued functions $\alpha, \beta$ on a finite type $W$ , as

d_{\mathrm{TV}}(\alpha, \beta) \;=\; \sup_{A \subseteq W} \left| \sum_{x \in A} \alpha(x) - \sum_{x \in A} \beta(x) \right|,

the supremum over all finite subsets $A$ of $W$ (including the empty set); since $W$ is finite this is a maximum over all subsets, and note this definition carries no factor of $\tfrac{1}{2}$ and is not a pointwise $\ell^1$ sum. The theorem asserts the single non-strict inequality

d_{\mathrm{TV}}\bigl(f_*\mu,\; f_*\nu\bigr) \;\le\; d_{\mathrm{TV}}(\mu, \nu),

i.e., the total-variation distance between the pushforward distributions on $\Lambda$ is at most the total-variation distance between the original distributions on $V$ . The two distribution hypotheses on $\mu$ and $\nu$ are the only substantive assumptions; nothing is assumed about $f$ (it need not be surjective or injective), and the inequality is $\le$ , not $<$ .

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