The Exercise

A sender has a noisy classical channel $N$. Each use takes one symbol $x$ from a finite input alphabet and returns one symbol $y$ from a finite output alphabet, at random, with probabilities that depend only on the $x$ sent and not on earlier uses. Coding a message over many uses, the sender can get information through at any rate below a certain number of bits per use, with a probability of error that vanishes as the number of uses grows. The capacity $C(N)$ of the channel is this largest such rate. Shannon’s noisy channel coding theorem computes it from a single use: $C(N)$ is the largest mutual information between the input $X$ and the output $Y$, over all distributions $p(x)$ of the input.

A Discrete Memoryless Channel

A discrete memoryless channel $N$ from a finite input alphabet $\mathcal{X}$ to a finite output alphabet $\mathcal{Y}$ is a family of transition probabilities $q(y|x)$, one distribution over outputs for each input: $$q(y|x) \ge 0, \qquad \sum_{y \in \mathcal{Y}} q(y|x) = 1 \quad \text{for every } x \in \mathcal{X}.$$(1)^✦

For an input distribution $p$, a probability distribution on $\mathcal{X}$, the joint distribution $p_{XY}$ of the input $X$ and the output $Y$ is the distribution on $\mathcal{X} \times \mathcal{Y}$ given by $$p_{XY}(x,y) = p(x)\, q(y|x).$$(2)^✦

Entropy and Mutual Information

The Shannon entropy $H(p)$ of a distribution $p$ on a finite set is $$H(p) = -\sum_i p_i \ln p_i ,$$(3)^✦ taken with the natural logarithm, so that it is measured in nats.

The first marginal $p_X$ of a joint distribution $p_{XY}$ of $X$ and $Y$ on $\mathcal{X} \times \mathcal{Y}$ is the distribution of $X$ alone^✦, and the second marginal $p_Y$ is the distribution of $Y$ alone: $$p_X(x) = \sum_{y} p_{XY}(x,y), \qquad p_Y(y) = \sum_{x} p_{XY}(x,y).$$(4)^✦

The mutual information $H(X:Y)$ of $p_{XY}$ is the sum of the entropies of its marginals less its own entropy. $$H(X:Y) = H(p_X) + H(p_Y) - H(p_{XY}).$$(5)^✦

The mutual information of the channel $N$ at an input distribution $p$ is $H(X:Y)$ for the joint distribution (2).^✦

The supremum over all input distributions on $\mathcal{X}$ of the mutual information of $N$, in nats, is the information capacity $C_I(N)$ of $N$: $$C_I(N) = \sup_{p} H(X:Y).$$(6)^✦

The Claim

What Is Checked

The claim is stated over a discrete memoryless channel, given by its transition probabilities (1), and over its information capacity (6). What the library proves about these constructions is the identity (7), for every such channel.