Discrete Shannon entropy under the uniform measure

Definition

DiscreteEntropy

by xbgxjack · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsdiscrepancy-theoryentropyinformation-theory

The Shannon entropy of a discrete random variable $Z$ taking values in a finite set $\beta$ , distributed according to the uniform measure on a finite sample space $\Omega$ , is

H(Z) = \sum_{b \in \beta} p_b \log_2\frac{1}{p_b}, \qquad p_b = \Pr[Z = b] = \frac{\#\{\omega \in \Omega : Z(\omega) = b\}}{\#\Omega},

with the usual convention that a term with $p_b = 0$ contributes $0$ to the sum (matching the limit $p\log_2(1/p) \to 0$ as $p \to 0^+$ ).

This module fixes empiricalProb Z b as $p_b$ above and shannonEntropy Z as $H(Z)$ , together with the two basic structural facts that make empiricalProb a genuine probability distribution: it is nonnegative (empiricalProb_nonneg) and sums to $1$ over $\beta$ (sum_empiricalProb).

Shannon entropy of this kind underlies the entropy/pigeonhole method in combinatorics (Spencer's partial coloring lemma, Beck-Fiala type arguments): a random variable of low entropy must place a disproportionately large amount of probability mass on a single outcome, which is exactly the counting leverage such arguments exploit.

Formalization Note Entropy is taken base $2$ (in bits), matching the convention used throughout the combinatorics literature that applies it (e.g. Alon-Spencer, The Probabilistic Method). empiricalProb and shannonEntropy are defined for any random variable into a Fintype, under the uniform (counting) measure on a Fintype sample space; no independence or other distributional assumption is built into the definition itself.

Definition code

import Mathlib

open Finset

noncomputable section

variable {Ω β : Type*} [Fintype Ω] [Fintype β] [DecidableEq β]

/-- The empirical probability that `Z : Ω → β` takes the value `b`, under the uniform
distribution on the finite sample space `Ω`. -/
def empiricalProb (Z : Ω → β) (b : β) : ℝ :=
  ((univ.filter (fun ω => Z ω = b)).card : ℝ) / (Fintype.card Ω : ℝ)

/-- The base-2 Shannon entropy of `Z : Ω → β`, computed from its empirical distribution under
the uniform measure on `Ω`, following the usual convention that a zero-probability outcome
contributes `0` to the sum (since `p log(1/p) → 0` as `p → 0⁺`). -/
def shannonEntropy (Z : Ω → β) : ℝ :=
  ∑ b : β, (fun p => if p = 0 then 0 else p * Real.logb 2 (1 / p)) (empiricalProb Z b)

lemma empiricalProb_nonneg (Z : Ω → β) (b : β) : 0 ≤ empiricalProb Z b := by
  unfold empiricalProb
  positivity

lemma sum_empiricalProb (Z : Ω → β) [Nonempty Ω] :
    ∑ b : β, empiricalProb Z b = 1 := by
  unfold empiricalProb
  rw [← Finset.sum_div]
  have hsum : ∑ b : β, ((univ.filter (fun ω => Z ω = b)).card : ℝ) = (Fintype.card Ω : ℝ) := by
    have h1 : (univ : Finset Ω).card
        = ∑ b ∈ (univ : Finset β), (univ.filter (fun ω => Z ω = b)).card :=
      Finset.card_eq_sum_card_fiberwise (fun a _ => mem_univ _)
    rw [Fintype.card]
    exact_mod_cast h1.symm
  rw [hsum]
  have hne : (Fintype.card Ω : ℝ) ≠ 0 := by
    have := Fintype.card_pos (α := Ω)
    positivity
  field_simp

end

Source

T. M. Cover and J. A. Thomas, Elements of Information Theory, 2nd ed., Wiley, 2006, Chapter 2 (Entropy, Relative Entropy, and Mutual Information), Section 2.1, Eq. (2.1); as used in J. Spencer, Six standard deviations suffice, Trans. Amer. Math. Soc. 289 (1985) 679-706, Section 2 (the entropy method).

View graph