The Exercise

Two random variables $X$ and $Y$ take values in finite sets $\mathcal{X}$ and $\mathcal{Y}$ and have a joint distribution $p(x,y)$. The joint entropy $H(X,Y)$ measures the uncertainty in the pair, the entropies $H(X)$ and $H(Y)$ the uncertainty in each variable alone. The exercise is to show that the uncertainty in the pair never exceeds the sum of the two^✦, and that it equals the sum exactly when $X$ and $Y$ are independent.^✦

Entropy and Marginals

A joint distribution $p$ of $X$ and $Y$ is a real function on $\mathcal{X}\times\mathcal{Y}$, nonnegative at every pair and summing to one.

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

The first marginal $p_X$ of a joint distribution $p$ of $X$ and $Y$ is the distribution of $X$ alone, obtained by summing out $Y$: $$p_X(x) = \sum_{y\in\mathcal{Y}} p(x,y).$$(2)^✦ The second marginal $p_Y$ of $p$ is the distribution of $Y$ alone, obtained by summing out $X$: $$p_Y(y) = \sum_{x\in\mathcal{X}} p(x,y).$$(3)^✦

The independent product $p_X\otimes p_Y$ of a joint distribution $p$ is the distribution on $\mathcal{X}\times\mathcal{Y}$ that gives each pair the product of the two marginals, $$(p_X\otimes p_Y)(x,y) = p_X(x)\,p_Y(y),$$(4)^✦ the joint distribution that $X$ and $Y$ would have if they were independent with the same marginals.

The Claim

What Is Checked

The claim is stated over the Shannon entropy (1), the two marginals (2) and (3), and the independent product (4) of a real function on the product of two finite sets. What the library proves about these constructions is the identity (7), which ties the independent product to the entropies of $p$ and of its marginals.