Entropy of a Bernoulli measure

The Bernoulli measure Ber(x, y, p) on two distinct points has entropy binEntropy p, the binary entropy function. Its zeros, its maximum log 2 at p = 1/2 and its monotonicity on either side of 1/2 are therefore facts about the entropy of any two-point law.

Main statements

• measureEntropy_bernoulliMeasure: Hm[Ber(x, y, p)] = binEntropy p for x ≠ y.

References

• [CT06]

theorem InformationTheory.measureEntropy_bernoulliMeasure {S : Type u_1} [MeasurableSpace S] [MeasurableSingletonClass S] {x y : S} (h : x ≠ y) (p : ↑unitInterval) : measureEntropy (ProbabilityTheory.bernoulliMeasure x y p) = Real.binEntropy ↑p

A Bernoulli measure on two distinct points has the binary entropy of its parameter.