The Exercise

A coin shows heads with probability $p$ and tails with probability $1-p$ . Its entropy, measured in bits, is called the binary entropy. The exercise is to show that the binary entropy, written $H_{\mathrm{bin}}$ , is a concave function of $p$ . Take a coin of bias $p$ and a coin of bias $q$ , pick the first with probability $\lambda$ and the second otherwise, and toss the one picked without recording which it was. Heads comes up with probability $\lambda p + (1-\lambda) q$ , and concavity says that the entropy of this toss is at least the average of the two coins’ entropies, with weights $\lambda$ and $1-\lambda$ .^✦

The Binary Entropy

The binary entropy $H_{\mathrm{bin}}(p)$ of a real number $p$ is the real number $H_{\mathrm{bin}}(p) = -p \log_2 p - (1-p) \log_2 (1-p),$ (1)^✦ with the logarithm to base 2 and the convention $0 \log_2 0 = 0$ .

The Claim

The library states concavity on the closed interval $[0,1]$ together with its strict form.

Theorem 1. Let $p$ and $q$ be numbers in $[0,1]$ and let $0 \le \lambda \le 1$ . Then the binary entropy is concave on $[0,1]$ : $H_{\mathrm{bin}}\bigl(\lambda p + (1-\lambda) q\bigr) \ge \lambda H_{\mathrm{bin}}(p) + (1-\lambda) H_{\mathrm{bin}}(q).$ (2)^✦ If moreover $p \neq q$ and $0 < \lambda < 1$ , it is strictly concave there: $H_{\mathrm{bin}}\bigl(\lambda p + (1-\lambda) q\bigr) > \lambda H_{\mathrm{bin}}(p) + (1-\lambda) H_{\mathrm{bin}}(q).$ (3)^✦

What Is Checked

The claim is stated over the binary entropy (1) on the closed interval $0 \le p \le 1$ of coin biases. About that function on that interval the library proves both inequalities of the theorem, (2) and (3).