3.3 Mutual information

Definition 3.9 Real-valued mutual information

Lean: InformationTheory.mutualInformationReal

For a probability measure \(P\) on \(X \times Y\) with marginals \(P_X, P_Y\), \(\mathrm{MI}_\mathbb {R}(P) \; :=\; \mathrm{KL}_\mathbb {R}(P, P_X \otimes P_Y)\) [ 7 , § 2.3, Defn 2.28 ] , [ 16 , § 3.1 ] .

Theorem 3.10 Non-negativity of mutual information

Lean: InformationTheory.mutualInformationReal_nonneg

\(\mathrm{MI}_\mathbb {R}(P) \ge 0\) (Gibbs applied to the joint vs. product-of-marginals) [ 7 , Thm 2.6.3 ] .

Theorem 3.11 Mutual information vanishes iff independent

Lean: InformationTheory.mutualInformationReal_eq_zero_iff_product

Under \(P \ll P_X \otimes P_Y\) and \(\mathrm{KL}(P, P_X \otimes P_Y) \ne \infty \), \(\mathrm{MI}_\mathbb {R}(P) = 0 \iff P = P_X \otimes P_Y\) [ 7 , Thm 2.6.5 ] .