Proposition 4.7 -- the coupling characterization of total variation

Proved

MarkovMixing.tv_coupling

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. A coupling of $\mu$ and $\nu$ is a probability distribution $q$ on ordered pairs $V\times V$ whose marginals are $\mu$ and $\nu$ — that is, $\sum_y q(x,y)=\mu(x)$ for every $x$ and $\sum_x q(x,y)=\nu(y)$ for every $y$ ; one thinks of $q$ as the joint law of a pair of random variables $(X,Y)$ with $X\sim\mu$ and $Y\sim\nu$ .

The theorem (Proposition 4.7 and Remark 4.8 of Levin–Peres–Wilmer) asserts two things. First, every coupling $q$ places at least $\|\mu-\nu\|_{TV}$ of its mass off the diagonal:

\|\mu-\nu\|_{TV}\;\le\;\sum_{(x,y):\,x\ne y}q(x,y)\;=\;\mathbb P\{X\ne Y\}.

Second, some coupling attains this bound — an optimal coupling, whose off-diagonal mass is exactly $\|\mu-\nu\|_{TV}$ . Together: the total variation distance is the minimal probability of disagreement achievable by any joint realization of the two distributions, and the minimum is attained.

Preamble

import Definitions.Def_mm_mixing

Formal statement

namespace MarkovMixing

/-- **Proposition 4.7 and Remark 4.8** (LPW): every coupling `(X,Y)` of `μ`
and `ν` has `P{X ≠ Y} ≥ ‖μ − ν‖_TV`, and there is an *optimal* coupling
attaining equality. -/
theorem tv_coupling {V : Type*} [Fintype V] [DecidableEq V]
    (μ ν : V → ℝ) (hμ : IsDist μ) (hν : IsDist ν) :
    (∀ q : V × V → ℝ, IsCoupling μ ν q →
      tvDist μ ν ≤ ∑ p ∈ Finset.univ.filter (fun p : V × V => p.1 ≠ p.2), q p) ∧
    ∃ q : V × V → ℝ, IsCoupling μ ν q ∧
      tvDist μ ν = ∑ p ∈ Finset.univ.filter (fun p : V × V => p.1 ≠ p.2), q p := 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.2, Proposition 4.7 and Remark 4.8, pp. 50-51

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 (all values nonnegative and summing to $1$ : $\forall x,\ 0 \le \mu(x)$ and $\sum_{x \in V}\mu(x) = 1$ , likewise for $\nu$ ). Call $q : V \times V \to \mathbb{R}$ a coupling of $\mu$ and $\nu$ when $q$ is itself a probability distribution on the product type $V \times V$ (all values nonnegative, $\sum_{(x,y)} q(x,y) = 1$ ) whose first marginal is $\mu$ ( $\forall x,\ \sum_{y} q(x,y) = \mu(x)$ ) and whose second marginal is $\nu$ ( $\forall y,\ \sum_{x} q(x,y) = \nu(y)$ ). Writing

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

for the custom total-variation quantity (a supremum over all subsets $A$ of the finite type $V$ , with no factor $\tfrac12$ ; taken in $\mathbb{R}$ with the convention that an empty or unbounded supremum is $0$ , though here the family is nonempty and, under the hypotheses, bounded), the theorem asserts the conjunction of two claims:

for every coupling $q$ of $\mu$ and $\nu$ ,

\mathrm{tvDist}(\mu,\nu) \;\le\; \sum_{\substack{(x,y) \in V \times V \\ x \ne y}} q(x,y),

i.e. the total variation quantity is at most the total mass $q$ places off the diagonal; and

there exists a coupling $q$ of $\mu$ and $\nu$ for which this holds with equality:

\mathrm{tvDist}(\mu,\nu) \;=\; \sum_{\substack{(x,y) \in V \times V \\ x \ne y}} q(x,y).

The existence in (2) is plain existence, not unique existence. Edge case: if $V$ is empty, the hypotheses $\mathrm{IsDist}$ are unsatisfiable (an empty sum is $0$ , not $1$ ), so the statement is vacuous there; note also that when $V$ is empty no coupling exists either, since $\sum_{(x,y)} q(x,y) = 1$ is likewise impossible.

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