Subadditivity of Shannon entropy for a finite family (independence bound)

Proved

shannonEntropy_pi_le

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

combinatoricsentropyinformation-theoryspencer

Let $\Omega$ be a finite, nonempty sample space with the uniform distribution, $\gamma$ a finite set, and $Z_1,\dots,Z_n : \Omega \to \gamma$ a finite family of $\gamma$ -valued random variables. Then the (base-2, empirical) Shannon entropy of the joint random variable $(Z_1,\dots,Z_n) : \Omega \to \gamma^n$ (encoded here as the function $\omega \mapsto (i \mapsto Z_i(\omega))$ ) is at most the sum of the individual entropies:

H(Z_1,\dots,Z_n) \le \sum_{i=1}^n H(Z_i).

This is the finite-family generalization of the pairwise subadditivity already established as shannonEntropy_prod_le, obtained by induction on $n$ : split off one coordinate at a time via the equivalence $(\mathrm{Fin}(n{+}1) \to \gamma) \simeq \gamma \times (\mathrm{Fin}\,n \to \gamma)$ , apply the two-variable bound, and use the inductive hypothesis on the rest. It is the standard 'independence bound on entropy' from information theory, and is the tool used to bound the entropy of a vector of independently-digitized coordinates (e.g. one bin index per linear form/row) by the sum of the per-coordinate entropies, a key step in entropy-compression arguments such as Spencer's partial-colouring method.

Preamble

import Definitions.Def_DiscreteEntropy
import Theorems.Thm_shannonEntropy_prod_le
import Mathlib
open Finset

Formal statement

theorem shannonEntropy_pi_le {Ω : Type*} [Fintype Ω] [Nonempty Ω]
    {n : ℕ} {γ : Type*} [Fintype γ] [DecidableEq γ]
    (Z : Fin n → Ω → γ) :
    shannonEntropy (fun ω i => Z i ω) ≤ ∑ i, shannonEntropy (Z i) := by sorry

Source

T. Cover, J. Thomas, Elements of Information Theory, 2nd ed. (Wiley, 2006), Theorem 2.6.6 ("Independence bound on entropy"): H(X_1,...,X_n) <= sum H(X_i). Standard finite-family generalization of the pairwise subadditivity proved as Prove2Me theorem shannonEntropy_prod_le, which is used as the inductive step here.

View graph