Gibbs' inequality (non-negativity of KL divergence)

Gibbs' inequality (equivalently, the non-negativity of Kullback-Leibler divergence), in elementary finite form. Let $p, q : \gamma \to \mathbb{R}$ be two probability distributions on a finite set $\gamma$ ($p, q \ge 0$, $\sum_x p(x) = \sum_x q(x) = 1$), and suppose $q$ is positive wherever $p$ is (so the ratio $q(x)/p(x)$ is well-defined and finite on the support of $p$). Then

with equality exactly when $p = q$. Equivalently, $D(p \| q) := -\sum_{x : p(x)\neq0} p(x)\log(q(x)/p(x)) \ge 0$.

This is one of the two or three most-used inequalities in information theory: it underlies the fact that entropy is maximized by the uniform distribution, the data-processing inequality, and — as used in the entropy method in combinatorics (Spencer's partial coloring lemma) — the subadditivity of Shannon entropy for a pair of jointly distributed random variables, $H(X,Y) \le H(X) + H(Y)$.

The proof is elementary: for each $x$ with $p(x) > 0$, the standard bound $\log(t) \le t - 1$ applied at $t = q(x)/p(x)$ gives $p(x)\log(q(x)/p(x)) \le q(x) - p(x)$; summing over the support of $p$ and using $\sum q(x) \le 1 = \sum_{p(x)\neq 0} p(x)$ closes the inequality.

Formalization Note The hypothesis that $q$ does not vanish on the support of $p$ is necessary: without it, $q(x)/p(x)$ could be $0$ at a point where $p(x) > 0$, and $\log(0) = 0$ under Lean's junk-value convention would make the elementary per-term bound false there.