Proposition 4.5 -- total variation via bounded test functions

Proved

MarkovMixing.tv_sup_functions

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 $\|\mu-\nu\|_{TV}=\max_{A\subseteq V}|\mu(A)-\nu(A)|$ denote their total variation distance, the largest discrepancy in the probability of a single event. Write $\mathbb E_\mu(f)=\sum_x f(x)\,\mu(x)$ for the expectation of an observable $f:V\to\mathbb R$ under $\mu$ .

The theorem (Proposition 4.5 of Levin–Peres–Wilmer) characterizes the distance by expectations of bounded observables:

\|\mu-\nu\|_{TV}=\frac12\,\sup_{f:\,\max_x|f(x)|\le1}\bigl|\mathbb E_\mu(f)-\mathbb E_\nu(f)\bigr|,

the supremum running over all functions $f$ on $V$ bounded by $1$ in absolute value. In words: two distributions are far in total variation exactly when some $[-1,1]$ -valued statistic has visibly different means under the two.

Preamble

import Definitions.Def_mm_mixing

Formal statement

namespace MarkovMixing

/-- **Proposition 4.5** (LPW): the total variation distance equals half the
supremum, over functions bounded by `1` in absolute value, of the difference
of expectations. -/
theorem tv_sup_functions {V : Type*} [Fintype V] [DecidableEq V]
    (μ ν : V → ℝ) (hμ : IsDist μ) (hν : IsDist ν) :
    tvDist μ ν =
      2⁻¹ * ⨆ f : {f : V → ℝ // ∀ x, |f x| ≤ 1},
        |∑ x, (f : V → ℝ) x * μ x - ∑ x, (f : V → ℝ) x * ν 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 4.1, Proposition 4.5, p. 49

Read-back

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

Let $V$ be any finite type with decidable equality, and let $\mu, \nu : V \to \mathbb{R}$ be two functions, each assumed to be a probability distribution in the sense that all its values are nonnegative and its values sum to $1$ ( $\forall x,\ 0 \le \mu(x)$ and $\sum_{x \in V} \mu(x) = 1$ , and likewise for $\nu$ ). The theorem asserts the equality

\mathrm{tvDist}(\mu,\nu) \;=\; \frac{1}{2}\,\sup_{f}\ \Bigl|\sum_{x \in V} f(x)\,\mu(x) \;-\; \sum_{x \in V} f(x)\,\nu(x)\Bigr|,

where the supremum on the right ranges over all functions $f : V \to \mathbb{R}$ satisfying $|f(x)| \le 1$ for every $x \in V$ , and where $\mathrm{tvDist}$ is the custom definition

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

the supremum ranging over all (finite) subsets $A$ of $V$ — since $V$ is finite, this is all subsets of $V$ , including the empty set. Note that $\mathrm{tvDist}$ carries no factor of $\tfrac12$ in its definition; the factor $\tfrac12$ appears only on the right-hand side of the claimed equality. Both suprema are taken in the real numbers using the convention that the supremum of an empty or unbounded family is $0$ ; here both index families are nonempty (the empty subset $A = \varnothing$ , and the constant function $f \equiv 0$ ) and, given the distribution hypotheses, bounded, so the convention is not invoked under the hypotheses. Edge case: if $V$ is empty, the hypotheses are unsatisfiable (an empty sum is $0$ , not $1$ ), so the statement is vacuous in that case; no nonemptiness assumption on $V$ is made explicitly.

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