Lean, informalized

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

Exercise 11.2 - Information that adds over independent events is klog⁡pk \log p, and its average is −k-k times the entropy

An additive measure of information is a logarithm.

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

An event of probability pp carries an amount of information I(p)I(p). Two independent events with probabilities pp and qq occur together with probability pqpq, and the information of the joint event is the sum of the two: I(pq)=I(p)+I(q).I(pq) = I(p) + I(q).(1) The exercise asks to show that a differentiable function with this property is a constant multiple of the logarithm, and that the information averaged over the outcomes of a trial is then proportional to the entropy of their probabilities.

Shannon Entropy

The Shannon entropy H(p)H(p) of a family of real numbers p=(pi)p = (p_i) indexed by a finite set is the real number H(p)=−∑ipilog⁡pi,H(p) = -\sum_i p_i \log p_i ,(2)✦ with log\log the natural logarithm and a term 0log⁡00 \log 0 taken as zero.

The Claim

Theorem 1. Let II be a real function, differentiable at every positive point, that satisfies (1) for all positive pp and qq. Then there is a constant kk such that I(p)=klog⁡pfor all p>0.I(p) = k \log p \qquad \text{for all } p > 0 .(3)✦ If a real function II has the form (3) for a constant kk, then for every family p=(pi)p = (p_i) of positive numbers indexed by a finite set ∑ipiI(pi)=−kH(p).\sum_i p_i \, I(p_i) = -k \, H(p) .(4)✦

For probabilities summing to one, the left side of (4) is the average information of the outcome.

What Is Checked

The first part is stated over real functions differentiable at every positive point, the second over the Shannon entropy (2) of a finite family of positive numbers. About the entropy, the library proves (4), which ties it to every information function of logarithmic form, whatever the constant kk.