Proposition 9.1.1 — sharpness of the row coefficient

Proved

DuchiSIT.dobrushin_le_tvContraction

by Mrnaiq · Nov 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

information-theoryprobabilitytotal-variation

For every Markov kernel, the Dobrushin row coefficient is at most the supremum of its output-to-input total-variation ratios over distinct input probability laws. The spaces are arbitrary measurable spaces; no finite-state, topology, stationarity or irreducibility assumption is imposed. Real suprema use zero on an empty index set. The source notation is extended explicitly to empty spaces and spaces with at most one probability measure.

Preamble

import Definitions.Def_DuchiSIT_TVContractionCoefficient
set_option autoImplicit false
open MeasureTheory ProbabilityTheory

Formal statement

namespace DuchiSIT

theorem dobrushin_le_tvContraction {X Y : Type*}
    [MeasurableSpace X] [MeasurableSpace Y]
    (K : Kernel X Y) [IsMarkovKernel K] :
    dobrushin K ≤ tvContraction K := by sorry

end DuchiSIT

Source

John Duchi, Lecture Notes on Statistics and Information Theory, December 6, 2023, Section 9.1, printed pp. 220–222, Definitions 9.1–9.2 and Proposition 9.1.1; total variation uses Lemma 2.2.4. https://web.stanford.edu/class/stats311/lecture-notes.pdf

Read-back

What the Lean code literally says, in plain math · gpt-6

For every pair of types $X,Y$ equipped with arbitrary measurable-space structures, and every Markov kernel $K$ from $X$ to $Y$ (so $K(x)$ is a probability measure on $Y$ for every $x$ , with the measurability required of a kernel), the following inequality holds. For two measures $\alpha,\beta$ on any one of these measurable spaces $Z$ , define separately

d_Z(\alpha,\beta)=\sup\{\lvert (\alpha(A))_{\mathbb R}-(\beta(A))_{\mathbb R}\rvert:A\subseteq Z\text{ is measurable}\},

where $(t)_{\mathbb R}$ is the conversion of a nonnegative extended real to a real: finite values retain their value and $+\infty$ becomes $0$ . For a probability measure $\mu$ on $X$ , let $C_K\mu$ be the probability measure whose underlying measure is the composition $K\circ_m\mu$ , equivalently $(C_K\mu)(B)=\int_X K(x)(B)\,d\mu(x)$ for measurable $B\subseteq Y$ , with this integral understood as a nonnegative extended-real integral. Define the two further, separate real suprema

D_K=\sup\{d_Y(K(x),K(y)):x,y\in X\},\qquad T_K=\sup\left\{\frac{d_Y(C_K\mu,C_K\nu)}{d_X(\mu,\nu)}:\mu,\nu\text{ are probability measures on }X,\ \mu\ne\nu\right\}.

Then $D_K\le T_K$ . All the displayed suprema are suprema in $\mathbb R$ of the indicated sets of real values, not suprema in the extended reals; the real supremum of the empty set is $0$ (and the total real supremum operation also returns $0$ for a set unbounded above). Division is real division, including the convention $a/0=0$ ; the defining set for $T_K$ requires only that the probability measures differ, and has no separate positive-denominator condition. There are no assumptions that $X$ or $Y$ is nonempty, that measurable sets distinguish points, or that either space has any further regularity. In particular the first coefficient's defining set is empty if $X$ is empty, and the second coefficient's defining set is empty whenever $X$ has no pair of distinct probability measures; these sets then have supremum $0$ . The set defining $d_Z$ always contains the value $0$ from the empty measurable set. All measures entering these distances in this assertion are probability measures, so their values on measurable sets are finite.

Human review

Endorsed by Shuze Chen · Nov 12, 2026
Confirmed by the moderator at approval.
Endorsed by Mrnaiq · Nov 12, 2026
Confirmed by the mission captain (proposal self-audit).

View graph