The Theorem

Theorem 11.4 is the chain rule for conditional entropies. Let $X_1, \dots, X_n$ and $Y$ be random variables, each with finitely many values. The uncertainty about the whole string $X_1, \dots, X_n$ once $Y$ is known is counted one variable at a time: the uncertainty about $X_1$ given $Y$, plus that about $X_2$ given $Y$ and $X_1$, and so on up to $X_n$, given $Y$ and all the variables before it.^✦

Distributions and Entropy

A random variable $X$ with values in a finite set $\mathcal{X}$ is a function from a finite sample space $\Omega$ to $\mathcal{X}$, where each point $\omega$ of $\Omega$ carries a real weight $\mu(\omega)$. The law $p_X$ of $X$, the image of $\mu$ under $X$, is the distribution on $\mathcal{X}$ that gives each value $x$ the total weight of the points where $X$ takes it: $$p_X(x) = \sum_{\omega \,:\, X(\omega) = x} \mu(\omega).$$(1)^✦

Random variables taken together form one random variable, with the list of their values: for a second random variable $Y$ with values in a finite set $\mathcal{Y}$, the law of the pair $\omega \mapsto (X(\omega), Y(\omega))$ is the joint distribution $p_{XY}$ of $X$ and $Y$ on $\mathcal{X} \times \mathcal{Y}$.

The Shannon entropy $H(p)$ of a distribution $p$ on a finite set $\mathcal{X}$ is $$H(p) = -\sum_{x \in \mathcal{X}} p(x) \log p(x),$$(2)^✦ with the natural logarithm, so that it is measured in nats.

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

For random variables, $p$ is their joint distribution $p_{XY}$; subtracting the entropy of its second marginal $p_Y$ from that of $p$ gives the conditional entropy $H(X \mid Y)$: $$H(X \mid Y) = H(p) - H(p_Y).$$(4)^✦ A list of random variables on either side of the bar, as in $H(X_i \mid Y, X_1, \dots, X_{i-1})$, is the one random variable the list forms.

The Claim

For $\mu$ a probability distribution on $\Omega$ this is Theorem 11.4.

What Is Checked

The claim is stated over the law (1) of a random variable on a finite sample space and over the conditional entropy (4) of the joint laws so formed, which rests on the Shannon entropy (2) and the second marginal (3). What the library proves about these constructions is the chain rule (5) itself.