The Theorem

A noisy channel turns a random variable $X$ into $Y$ , and a second procedure, which sees only $Y$ , turns $Y$ into $Z$ . The three variables then form a Markov chain $X \to Y \to Z$ : once $Y$ is known, $Z$ is independent of $X$ . The data processing inequality says that the second step cannot add information about $X$ : $Z$ shares no more mutual information with $X$ than $Y$ does.^✦ The theorem pairs it with a bound on the first step. The information $Y$ carries about $X$ never exceeds the entropy of $X$ ^✦, and equals it exactly when $X$ can be recovered from $Y$ .^✦

Entropy and Mutual Information

The Shannon entropy $H(q)$ of a distribution $q$ on a finite set $\iota$ is the number $H(q) = -\sum_{i \in \iota} q(i) \log q(i),$ (1)^✦ with the natural logarithm, so that entropies are measured in nats.

The first marginal $q_X$ of a joint distribution $q$ of $X$ and $Y$ on $\iota \times \kappa$ is the distribution of $X$ alone^✦, and its second marginal $q_Y$ is the distribution of $Y$ alone; each sums out the other variable: $q_X(x) = \sum_{y \in \kappa} q(x,y), \qquad q_Y(y) = \sum_{x \in \iota} q(x,y).$ (2)

The mutual information $H(X:Y)$ of a joint distribution $q$ of $X$ and $Y$ is the sum of the entropies of its two marginals less the joint entropy $H(q)$ : $H(X:Y) = H(q_X) + H(q_Y) - H(q).$ (3)^✦

Let a third variable $Z$ take values in a finite set $\mu$ . The marginal $p_{XY}$ of a joint distribution $p$ of $X$ , $Y$ , $Z$ on $\iota \times \kappa \times \mu$ is the joint distribution of $X$ and $Y$ , obtained by summing out $Z$ : $p_{XY}(x,y) = \sum_{z \in \mu} p(x,y,z).$ (4)^✦ The marginal $p_{XZ}$ of $p$ is the joint distribution of $X$ and $Z$ , obtained by summing out the middle variable $Y$ : $p_{XZ}(x,z) = \sum_{y \in \kappa} p(x,y,z).$ (5)^✦ The mutual informations $H(X:Y)$ and $H(X:Z)$ of the three variables are those of $p_{XY}$ and $p_{XZ}$ , by (3). Read as a joint distribution of $X$ and the pair $(Y,Z)$ , $p$ has the first marginal $p_X(x) = \sum_{y,z} p(x,y,z)$ , the distribution of $X$ , and $H(X)$ is its entropy.

The Claim

Theorem 1. Let $p$ be a nonnegative function on $\iota \times \kappa \times \mu$ , and let $H(X)$ , $H(X:Y)$ and $H(X:Z)$ be formed from $p$ by (1) to (5). Then $H(X:Y) \le H(X).$ (6)^✦ If $\iota$ is not empty, then $H(X:Y) = H(X)$ (7)^✦ if and only if $X$ is a function of $Y$ , $X = f(Y)$ . If moreover $p$ sums to one and $X \to Y \to Z$ is a Markov chain, then $H(X:Z) \le H(X:Y).$ (8)^✦

What Is Checked

The claim is stated over the Shannon entropy (1) and the mutual information (3), taken on the marginals $p_X$ , $p_{XY}$ and $p_{XZ}$ of a single function $p$ of three variables. About these quantities the library proves the bound (6), its equality case (7) and the data processing inequality (8).