The Exercise

Two random variables $X$ and $Y$, such as the outcomes of two measurements made on one system, take values in finite sets $\mathcal X$ and $\mathcal Y$ with joint probabilities $p(x,y)$. Their Shannon entropies measure how uncertain the outcomes are, singly and together. Theorem 11.3 collects the basic relations among these entropies and the quantities built from them, with the cases in which an inequality becomes an equality. A third variable $Z$ enters two of them: the statement that the entropy of the three together with that of the shared variable does not exceed the entropy of the two overlapping pairs, called strong subadditivity, and the statement that conditioning on more variables does not increase entropy.

Entropy of a Pair

The Shannon entropy of a probability distribution $p$ on a finite set $\mathcal X$ is $$H(p) = -\sum_{x \in \mathcal X} p(x) \log p(x),$$(1)^✦ with the natural logarithm, so that entropy is measured in nats; the same sum defines $H(p)$ for any real function $p$ on $\mathcal X$.

The marginals of a function $p$ on $\mathcal X \times \mathcal Y$ are the functions $p_X$ on $\mathcal X$ and $p_Y$ on $\mathcal Y$ obtained by summing over the other variable, $$p_X(x) = \sum_{y \in \mathcal Y} p(x,y),$$(2)^✦ $$p_Y(y) = \sum_{x \in \mathcal X} p(x,y);$$(3)^✦ for a joint distribution of $X$ and $Y$ they are the distributions of $X$ and of $Y$ alone.

The entropy of the pair is written $H(X,Y) = H(p)$, and the entropy of each variable alone is $H(X) = H(p_X)$ and $H(Y) = H(p_Y)$.

The conditional entropy $H(X|Y)$ of $X$ given $Y$ and the mutual information $H(X:Y)$ of $X$ and $Y$ are $$H(X|Y) = H(X,Y) - H(Y),$$(4)^✦ $$H(X:Y) = H(X) + H(Y) - H(X,Y).$$(5)^✦ Exchanging the arguments of $p$ gives the function $(y,x) \mapsto p(x,y)$ on $\mathcal Y \times \mathcal X$, from which $H(Y,X)$ and $H(Y:X)$ are formed in the same way.

Multiplying the marginals of $p$ gives the function $p_X p_Y$ on $\mathcal X \times \mathcal Y$ $$(p_X p_Y)(x,y) = p_X(x)\, p_Y(y),$$(6)^✦ and $X$ and $Y$ are independent when $p = p_X p_Y$.

The variable $Y$ is a function of $X$, written $Y = f(X)$, when there is a map $f \colon \mathcal X \to \mathcal Y$ with $$y = f(x) \quad \text{whenever} \quad p(x,y) \neq 0.$$(7)^✦

Three Variables

For a function $p$ on $\mathcal X \times \mathcal Y \times \mathcal Z$, such as the joint distribution of three variables $X$, $Y$, $Z$, the marginal $p_{XY}$ of the first two is the function on $\mathcal X \times \mathcal Y$ $$p_{XY}(x,y) = \sum_{z \in \mathcal Z} p(x,y,z).$$(8)^✦ The marginal $p_{YZ}(y,z) = \sum_{x} p(x,y,z)$ of the last two is (3) with the pair $(Y,Z)$ in the place of $Y$^✦, and the marginal of the middle variable is $$p_Y(y) = \sum_{z \in \mathcal Z} p_{YZ}(y,z).$$(9)^✦

The entropy of the three together is $H(X,Y,Z) = H(p)$, of the first two $H(X,Y) = H(p_{XY})$, of the last two $H(Y,Z) = H(p_{YZ})$, and of the middle one alone $H(Y) = H(p_Y)$; the conditional entropy of $X$ given the pair is $H(X|Y,Z) = H(X,Y,Z) - H(Y,Z)$, which is (4) with $(Y,Z)$ in the place of $Y$.

The three variables form a Markov chain $Z \to Y \to X$, with $X$ and $Z$ independent given $Y$, when for all $x$, $y$, $z$ $$p(x,y,z)\, p_Y(y) = p_{XY}(x,y)\, p_{YZ}(y,z).$$(10)^✦

The Claim

What Is Checked

The theorem is stated over the entropy (1) of $p$ and of its marginals (2), (3), (8) and (9), combined into the conditional entropy (4) and the mutual information (5), with its cases of equality given by the product of the marginals (6), the dependence of $Y$ on $X$ (7) and the Markov condition (10).

What the library proves about these constructions is the theorem, each part for every $p$ that meets its hypothesis.