Proposition 9.1.1 — contraction inequality

For any two types $X$ and $Y$, each equipped with an arbitrary measurable-space structure, any measurable probability kernel $K$ from $X$ to $Y$ (so $K(x,\cdot)$ is a probability measure for every $x\in X$, and $x\mapsto K(x,A)$ is measurable for every measurable $A\subseteq Y$), and any probability measures $\mu$ and $\nu$ on $X$, let $\mu K$ and $\nu K$ be the probability measures whose underlying measures are the kernel–measure compositions $K\circ\mu$ and $K\circ\nu$; on each measurable $A\subseteq Y$, $(\mu K)(A)=\int_X K(x,A)\,d\mu(x)$ and $(\nu K)(A)=\int_X K(x,A)\,d\nu(x)$. For measures $\alpha,\beta$ on any one of these measurable spaces, define $d(\alpha,\beta)=\sup\{ |(\alpha(A)).\mathrm{toReal}-(\beta(A)).\mathrm{toReal}|:A\text{ is measurable}\}$, where measure values lie in the extended nonnegative reals and $\mathrm{toReal}$ sends a finite value to its real value and sends $+\infty$ to $0$. Define $\delta(K)=\sup\{d(K(x,\cdot),K(y,\cdot)):x,y\in X\}$, with the supremum taken in the real numbers. The assertion is

Every measure appearing here is a probability measure, hence every set value in these distance expressions is finite; consequently this is the normalization $d(\alpha,\beta)=\sup_{A\text{ measurable}}|\alpha(A)-\beta(A)|$, with values in $[0,1]$, and $\delta(K)$ is also in $[0,1]$. There are no assumptions of finiteness, countability, a topology, or a standard Borel structure, and the measures may coincide and the coefficient may be zero. Empty types are not explicitly excluded by the type binders: for an empty $X$ the real supremum defining $\delta(K)$ is the empty supremum, equal to $0$, but no probability measures $\mu,\nu$ on that $X$ exist, so there is no instance of the theorem's hypotheses; an empty $Y$ likewise admits no such Markov kernel when $X$ carries these probability measures.