Proposition 4.2 -- total variation as half the $\ell^1$ distance

Proved

MarkovMixing.tv_eq_half_l1

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}\bigl|\mu(A)-\nu(A)\bigr|

denote their total variation distance — the largest discrepancy the two distributions assign to a single event.

The theorem gives the two standard closed forms for this distance (Proposition 4.2 and Remark 4.3 of Levin–Peres–Wilmer). First, it is half the $\ell^1$ distance between the mass functions:

\|\mu-\nu\|_{TV}=\frac12\sum_{x\in V}\bigl|\mu(x)-\nu(x)\bigr|.

Second, it equals the total excess of $\mu$ over $\nu$ on the set where $\mu$ dominates:

\|\mu-\nu\|_{TV}=\sum_{x:\,\mu(x)\ge\nu(x)}\bigl(\mu(x)-\nu(x)\bigr),

i.e. the maximum in the definition is attained at the event $\{x:\mu(x)\ge\nu(x)\}$ .

Preamble

import Definitions.Def_mm_mixing

Formal statement

namespace MarkovMixing

/-- **Proposition 4.2 and Remark 4.3** (LPW): the total variation distance is
half the `ℓ¹` distance, and equals the excess of `μ` over `ν` on the set
where `μ ≥ ν`. -/
theorem tv_eq_half_l1 {V : Type*} [Fintype V] [DecidableEq V]
    (μ ν : V → ℝ) (hμ : IsDist μ) (hν : IsDist ν) :
    tvDist μ ν = 2⁻¹ * ∑ x, |μ x - ν x| ∧
    tvDist μ ν = ∑ x ∈ Finset.univ.filter (fun x : V => ν x ≤ μ x), (μ 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.2 and Remark 4.3, p. 48

Read-back

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

Let $V$ be an arbitrary finite type (with decidable equality). Let $\mu, \nu : V \to \mathbb{R}$ each be a distribution: all values are nonnegative and each sums to one, $\sum_x \mu(x) = 1 = \sum_x \nu(x)$ . (If $V$ is empty these hypotheses are unsatisfiable, since empty sums are $0$ , and the theorem holds vacuously.) Define the total variation distance here as

d_{TV}(\mu,\nu) \;=\; \sup_{A \subseteq V} \left| \sum_{x \in A} \mu(x) \;-\; \sum_{x \in A} \nu(x) \right|,

the supremum over all subsets $A$ of $V$ (finite subsets of $V$ , which, $V$ being finite, means all subsets, including $\emptyset$ and $V$ itself) of the absolute difference of the two masses assigned to $A$ ; since $V$ is finite this supremum ranges over a nonempty finite set of reals (the empty set contributes the value $0$ ), so it is a genuine maximum. Note the absolute value: no restriction such as $\mu(A) \ge \nu(A)$ is imposed inside the supremum. The theorem asserts the conjunction of two identities:

$d_{TV}(\mu,\nu)$ equals half the $\ell^1$ distance:

d_{TV}(\mu,\nu) \;=\; \frac{1}{2} \sum_{x \in V} \bigl|\mu(x) - \nu(x)\bigr|;

$d_{TV}(\mu,\nu)$ equals the sum of the (signed) differences over the set where $\mu$ dominates:

d_{TV}(\mu,\nu) \;=\; \sum_{\substack{x \in V \\ \nu(x) \le \mu(x)}} \bigl(\mu(x) - \nu(x)\bigr),

where the sum runs over exactly those $x \in V$ satisfying the non-strict inequality $\nu(x) \le \mu(x)$ (points with $\mu(x) = \nu(x)$ are included, contributing $0$ ), and the summand is the plain difference $\mu(x) - \nu(x)$ , not its absolute value.

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

Proposition 4.2 -- total variation as half the ℓ1\ell^1ℓ1 distance

Proposition 4.2 -- total variation as half the $\ell^1$ distance