Prove2Me

Binary entropy function h2(p)h_2(p) (Definition 10.1.2)

Definition
WildeQIT_binaryEntropy

by aadarwal · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

classical-informationentropyinformation-theorywilde-qit

Definition 10.1.2 (Binary entropy). The binary entropy of p∈[0,1]p\in[0,1] is

h2(p)≡−plog⁡p−(1−p)log⁡(1−p),h_2(p) \equiv -p\log p - (1-p)\log(1-p),

with the logarithm taken base 22 and the convention 0log⁡0=00\log 0=0, so that h2(0)=h2(1)=0h_2(0)=h_2(1)=0.

The binary entropy is the entropy of a Bernoulli random variable with parameter pp; it is the function that appears in Fano's inequality (Theorem 10.7.3), in the Zhang–Audenaert continuity bound (Theorem 10.7.4), and throughout the rate expressions of classical and quantum Shannon theory.

Formalization Note. WildeQIT.binaryEntropy p is defined for every real pp by the same formula, −(plog⁡2p)−(1−p)log⁡2(1−p)-(p\log_2 p) - (1-p)\log_2(1-p), using Real.logb 2. Since Mathlib sets Real.logb 2 0 = 0, the endpoint values h2(0)=h2(1)=0h_2(0)=h_2(1)=0 hold automatically; outside [0,1][0,1] the formula returns a real number that carries no meaning (Mathlib's Real.log of a negative number is the log of its absolute value). Statements that use h2h_2 carry the hypothesis p∈[0,1]p\in[0,1] where it matters.

Definition code
import Mathlib.Analysis.SpecialFunctions.Log.Base

/-!
Wilde, *Quantum Information Theory* (2nd ed.), Definition 10.1.2 (Binary entropy):
`h₂(p) ≡ -p log p - (1-p) log(1-p)` for `p ∈ [0,1]`, logarithm base 2.
-/

namespace WildeQIT

/-- Definition 10.1.2. The binary entropy function `h₂(p) = -p log₂ p - (1-p) log₂ (1-p)`.
Defined for every real `p` (Wilde: `p ∈ [0,1]`); at `p = 0` and `p = 1` the convention
`0 log 0 = 0` is automatic since `Real.logb 2 0 = 0`. -/
noncomputable def binaryEntropy (p : ℝ) : ℝ :=
  -(p * Real.logb 2 p) - (1 - p) * Real.logb 2 (1 - p)

end WildeQIT
Source
Wilde, Quantum Information Theory, 2nd ed. (Cambridge University Press, 2017; arXiv:1106.1445v8), Chapter 10 (Classical Information and Entropy), §The Binary Entropy Function, Definition 10.1.2 (book source roster-items.csv line 16236).

View graph