Subadditivity of Shannon entropy

Proved

shannonEntropy_prod_le

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

combinatoricsdiscrepancy-theoryentropyinformation-theory

Subadditivity of Shannon entropy. Let $Z_1 : \Omega \to \beta_1$ and $Z_2 : \Omega \to \beta_2$ be two random variables on the same finite, nonempty sample space $\Omega$ (uniformly distributed, as throughout Definitions.DiscreteEntropy). Then the entropy of the pair $(Z_1, Z_2)$ is at most the sum of the individual entropies:

H(Z_1, Z_2) \;\le\; H(Z_1) + H(Z_2).

Equality holds exactly when $Z_1$ and $Z_2$ are independent under the uniform measure on $\Omega$ ; the inequality in general reflects that correlation between $Z_1$ and $Z_2$ can only decrease the joint entropy relative to the independent case.

This is one of the two basic structural facts about entropy (alongside non-negativity) used throughout information theory and its combinatorial applications. In particular, it is the tool that lets the entropy method in combinatorics (Spencer's partial coloring lemma, and Beck-Fiala type arguments) bound the entropy of a vector of many "row" statistics of a random coloring by the sum of each row's individual entropy, one row at a time, rather than having to reason about their joint distribution directly.

The proof reduces to Gibbs' inequality (gibbs_inequality) applied to the joint distribution $p(a,b) = \Pr[Z_1 = a, Z_2 = b]$ against the product-of-marginals distribution $q(a,b) = \Pr[Z_1=a]\Pr[Z_2=b]$ : the resulting bound $\sum_{(a,b)} p(a,b)\log(q(a,b)/p(a,b)) \le 0$ unwinds, after taking marginals, to exactly $H(Z_1,Z_2) \le H(Z_1)+H(Z_2)$ (up to the constant base-2-versus-natural-log rescaling factor $\log 2$ , which is positive and so preserves the inequality's direction).

Formalization Note The joint variable is represented as fun ω => (Z1 ω, Z2 ω) : Ω → β1 × β2, and its entropy shannonEntropy uses the same base-2 convention as Definitions.DiscreteEntropy.

Preamble

import Definitions.Def_DiscreteEntropy
import Theorems.Thm_gibbs_inequality
import Mathlib

open Finset

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

Formal statement

theorem shannonEntropy_prod_le (Z1 : Ω → β1) (Z2 : Ω → β2) :
    shannonEntropy (fun ω => (Z1 ω, Z2 ω)) ≤ shannonEntropy Z1 + shannonEntropy Z2 := by sorry

Source

T. M. Cover and J. A. Thomas, Elements of Information Theory, 2nd ed., Wiley, 2006, Chapter 2, Theorem 2.6.6 (H(X,Y) <= H(X)+H(Y)); as applied in J. Spencer, Six standard deviations suffice, Trans. Amer. Math. Soc. 289 (1985) 679-706, Section 2 (the entropy method).

View graph