Lean, informalized

Nielsen & Chuang · Chapter 11, Entropy and information · p. 505

Theorem 11.2 - The Shannon entropy of a distribution on dd outcomes, and when it equals log⁡d\log d

Only the uniform distribution has entropy log⁡d\log d.

Hover over a blue or green term in the text, or a node in the graph, to find it in the other. Select it to read its declaration both in Lean and in words.

The Exercise

A random variable XX takes one of dd values, the iith with probability pip_i; the pip_i are nonnegative and add up to one. Its Shannon entropy measures the uncertainty about the outcome before XX is observed. Theorem 11.2 identifies the distributions whose entropy is exactly log⁡d\log d, the logarithm of the number of values.

The Shannon Entropy

The Shannon entropy H(p)H(p) of a family of real numbers p=(pi)i∈ιp = (p_i)_{i \in \iota}, indexed by a finite set ι\iota, is the real number H(p)=−∑i∈ιpilog⁡pi,H(p) = -\sum_{i \in \iota} p_i \log p_i ,(1)✦ with log\log the natural logarithm and 0log⁡0=00 \log 0 = 0. For a random variable, ι\iota is the set of its values and pp its distribution.

The Claim

Theorem 1. Let ι\iota be a nonempty finite set with dd elements, and let p=(pi)i∈ιp = (p_i)_{i \in \iota} be a probability distribution on ι\iota: every pip_i is nonnegative and ∑i∈ιpi=1\sum_{i \in \iota} p_i = 1. Then H(p)=log⁡d⇔pi=1dfor every i∈ι.H(p) = \log d \iff p_i = \frac{1}{d} \ \text{for every } i \in \iota .(2)✦

What Is Checked

The claim is stated over one construction, the Shannon entropy (1), taken of a probability distribution on a nonempty finite set. The library proves the equivalence (2) for every such distribution, whatever the number d≥1d \ge 1 of outcomes.