Proposition 9.1.1 — exact total-variation contraction coefficient

Proved

DuchiSIT.dobrushin_eq_tvContraction

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

information-theoryprobabilitytotal-variation

For every Markov kernel between arbitrary measurable spaces, its Dobrushin row coefficient equals its strong total-variation data-processing coefficient. Both coefficients are independently defined using the same event-supremum total-variation normalization. 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_eq_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$ , each equipped with an arbitrary measurable-space structure, and every measurable probability kernel $K$ from $X$ to $Y$ (so $K_x$ is a probability measure on $Y$ for every $x\in X$ , and $x\mapsto K_x(B)$ is measurable for every measurable $B\subseteq Y$ ), the following equality of real numbers holds:

\sup\{D_Y(K_x,K_y):x,y\in X\}=\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\}.

Here, for measures $\alpha,\beta$ on a measurable space $Z$ , the real number $D_Z(\alpha,\beta)$ is defined to be

D_Z(\alpha,\beta)=\sup\{|\operatorname{toReal}(\alpha(A))-\operatorname{toReal}(\beta(A))|:A\subseteq Z\text{ is measurable}\},

where $\operatorname{toReal}$ converts a finite nonnegative extended real to the corresponding real and sends $+\infty$ to $0$ ; all measures occurring in the displayed equality are probability measures, so their values on sets are finite. For each probability measure $\mu$ on $X$ , $C_K\mu$ is the probability measure obtained by composing $K$ with $\mu$ , characterized on measurable $B\subseteq Y$ by $(C_K\mu)(B)=\int_X K_x(B)\,d\mu(x)$ , with this integral taken in the nonnegative extended reals. Every supremum in these definitions is the real supremum: it is the least upper bound for a nonempty set bounded above, and has value $0$ for an empty set or a set unbounded above. Division is real division, with division by $0$ defined to be $0$ . The left supremum permits $x=y$ ; the right supremum requires distinct probability measures but imposes no separate positive-denominator hypothesis. There is no assumption that either type is nonempty, that $X$ supports two distinct probability measures, or that either measurable-space structure separates points. In particular, if $X$ is empty, both outer sets are empty and both sides have value $0$ ; if there are no two distinct probability measures on $X$ , the right-hand set is empty and its supremum is $0$ . The kernel hypothesis still applies in all such cases; if $Y$ is empty and $X$ is nonempty, no such probability kernel exists.

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