Mutual information $I(X;Y)$ (Definition 10.4.1)

Definition 10.4.1 (Mutual information). Let $X$ and $Y$ be discrete random variables with joint probability distribution $p_{XY}(x,y)$. The mutual information $I(X;Y)$ is the marginal entropy $H(X)$ less the conditional entropy $H(X|Y)$:

where $H(X)=-\sum_x p_X(x)\log p_X(x)$ is the entropy of the marginal $p_X(x)=\sum_y p_{XY}(x,y)$ and $H(X|Y)=-\sum_{x,y}p_{XY}(x,y)\log\bigl(p_{XY}(x,y)/p_Y(y)\bigr)$ (Definition 10.2.1); logarithms are base $2$.

The mutual information quantifies how much uncertainty about $X$ is removed by learning $Y$; it is the classical correlation measure underlying channel capacity, and Wilde's Chapter 10 establishes its symmetry, non-negativity, and data-processing property.

Formalization Note. WildeQIT.mutualInfo p is WildeQIT.entropy p.fst - WildeQIT.condEntropy p for a joint distribution p : WildeQIT.FinDist (α × β); here p.fst is the marginal of the first component and condEntropy p conditions the first component on the second, exactly matching $H(X)-H(X|Y)$.