Lean, informalized

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

Exercise 11.3 - The binary entropy in bits takes its greatest value, one, at p=1/2p = 1/2

The binary entropy is largest at one half.

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 coin lands heads with probability pp and tails with probability 1−p1 - p. The Shannon entropy of one toss, measured in bits, is the binary entropy H(p)H(p). The exercise asks to show that HH attains its maximum value, one bit, at p=1/2p = 1/2, the fair coin.

The Binary Entropy

The binary entropy in bits is the function HH that assigns to a real number pp the value H(p)=−plog⁡2p−(1−p)log⁡2(1−p),H(p) = -p \log_2 p - (1 - p) \log_2 (1 - p),(1)✦ where log⁡2\log_2 is the logarithm to base two and 0log⁡20=00 \log_2 0 = 0.

The Claim

Theorem 1. The binary entropy takes the value one at p=1/2p = 1/2, H(1/2)=1,H(1/2) = 1,(2)✦ and one is the greatest value it takes on the real line: maxp∈ℝH(p)=1.\max_{p \in \mathbb{R}} H(p) = 1.(3)✦

For 0≤p≤10 \le p \le 1 this is the exercise.

What Is Checked

The claim is stated over the binary entropy HH of (1) alone, a function of one real variable. What the library proves about HH is the theorem itself: the value (2) at one half and the maximum (3).