Shannon entropy and Kullback–Leibler divergence

DefinitionShannon entropy#✓fully proved

The Shannon entropy in bits of a probability mass function \(p\) on a finite type \(\alpha\) is \(H(p) = -\sum_{a \in \alpha} p(a) \log_2 p(a)\), where a term with \(p(a) = 0\) contributes \(0\).

noncomputable def shannonEntropy {α : Type*} [Fintype α] (p : PMF α) : ℝ :=
  (∑ a, Real.negMulLog (p a).toReal) / Real.log 2

Sources

• the finite Shannon sum; Li, arXiv:2501.13736v4, entropy conventions.

Used by 36

Used byInformation content against the uniform background · Information content is at most the log of the alphabet size · Information gain of a split · Information gain in terms of entropies · No split has negative information gain · Information gain is mutual information · Mutual information between the input and the auxiliary · Conditional entropy of the output given the auxiliary · Conditional entropy vanishes for a one-letter output · Mutual information · Conditional entropy of the output given the input and the auxiliary · Zero output entropy given input and auxiliary for a one-letter output · The trivial extension has zero auxiliary information · Conditional entropy in the trivial extension · Chow–Liu identity · Chow–Liu optimality · Conditioning does not increase entropy · Mutual information of a finite joint law · Chain rule for entropy · Subadditivity of entropy · Divergence of a finite joint law from the product of its marginals · Conditional mutual information in terms of entropies · Chain rule for mutual information · Mutual information in terms of entropies · Data-processing inequality · Data-processing inequality · Entropy of a pushforward is invariant under relabeling · Shannon entropy as a p log p sum · Log-sum against a pushforward equals its negative entropy · Cross-entropy is entropy plus divergence · Equality in Gibbs' inequality · Gibbs' inequality · A constant observation has zero entropy · Entropy is invariant under relabeling · Appending a singleton coordinate preserves entropy · A point mass has zero entropy

TheoremA point mass has zero entropy#✓fully proved

For every outcome \(a\) of a finite alphabet, the point mass at \(a\) has Shannon entropy \(0\).

@[simp] theorem shannonEntropy_pure {α : Type*} [Fintype α] (a : α) :
    shannonEntropy (PMF.pure a) = 0

Uses 1 · Used by 1

Statement usesShannon entropy

Used byA constant observation has zero entropy

TheoremA constant observation has zero entropy#✓fully proved

For any probability mass function \(p\) on a type \(\alpha\) and any point \(b\) of a finite alphabet \(\beta\), the image of \(p\) under the constant map \(\alpha \to \beta\) with value \(b\) has Shannon entropy \(0\).

theorem shannonEntropy_map_const {α β : Type*} [Fintype β]
    (p : PMF α) (b : β) :
    shannonEntropy (p.map (Function.const α b)) = 0

Uses 2 · Used by 2

Statement usesShannon entropy

Proof usesA point mass has zero entropy

Used byThe trivial extension has zero auxiliary information · Conditional entropy in the trivial extension

TheoremEntropy is invariant under relabeling#✓fully proved

For a probability mass function \(p\) on a finite alphabet \(\alpha\) and a bijection \(e : \alpha \to \beta\) onto a finite alphabet \(\beta\), the image of \(p\) under \(e\) has the same Shannon entropy as \(p\).

theorem shannonEntropy_map_equiv {α β : Type*} [Fintype α] [Fintype β]
    (p : PMF α) (e : α ≃ β) : shannonEntropy (p.map e) = shannonEntropy p

Uses 1 · Used by 6

Statement usesShannon entropy

Used byConditional entropy vanishes for a one-letter output · Zero output entropy given input and auxiliary for a one-letter output · Data-processing inequality · Data-processing inequality · Entropy of a pushforward is invariant under relabeling · Appending a singleton coordinate preserves entropy

TheoremAppending a singleton coordinate preserves entropy#✓fully proved

For a probability mass function \(p\) on a finite alphabet \(\alpha\), the image of \(p\) under \(a \mapsto (a, 0)\) in \(\alpha \times \{0\}\) has the same Shannon entropy as \(p\).

theorem shannonEntropy_map_prod_singleton {α : Type*} [Fintype α] (p : PMF α) :
    shannonEntropy (p.map (fun a => (a, (0 : Fin 1)))) = shannonEntropy p

Uses 2 · Used by 2

Statement usesShannon entropy

Proof usesEntropy is invariant under relabeling

Used byThe trivial extension has zero auxiliary information · Conditional entropy in the trivial extension

TheoremKullback–Leibler divergence on a finite space#✓fully proved

Let \(\mu\) and \(\nu\) be finite measures on a finite type \(\alpha\) in which every singleton is measurable, with \(\mu \ll \nu\) and \(\mu(\alpha) = \nu(\alpha)\). Then the Kullback–Leibler divergence \(\mathrm{KL}(\mu \parallel \nu)\), taken as a real number, equals \(\sum_{a \in \alpha} \mu(\{a\}) \log (\mu(\{a\}) / \nu(\{a\}))\), where \(\log\) is the natural logarithm and a term with \(\mu(\{a\}) = 0\) is \(0\).

theorem toReal_klDiv_eq_sum [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α]
    {μ ν : Measure α} [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hμν : μ ≪ ν)
    (huniv : μ Set.univ = ν Set.univ) :
    (klDiv μ ν).toReal = ∑ a, μ.real {a} * log (μ.real {a} / ν.real {a})

Used by 2

Used byDivergence of a finite joint law from the product of its marginals · Kullback–Leibler divergence of finite probability laws

TheoremKullback–Leibler divergence of finite probability laws#✓fully proved

Let \(p\) and \(q\) be probability mass functions on a finite type \(\alpha\) in which every singleton is measurable, such that \(p(a) = 0\) whenever \(q(a) = 0\), and let \(P\) and \(Q\) be the measures they define. Then the Kullback–Leibler divergence \(\mathrm{KL}(P \parallel Q)\), taken as a real number, equals \(\sum_{a \in \alpha} p(a) \log (p(a) / q(a))\), where \(\log\) is the natural logarithm and a term with \(p(a) = 0\) is \(0\).

theorem toReal_klDiv_toMeasure [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α]
    {p q : PMF α} (hpq : ∀ a, q a = 0 → p a = 0) :
    (klDiv p.toMeasure q.toMeasure).toReal =
      ∑ a, (p a).toReal * log ((p a).toReal / (q a).toReal)

Uses 1 · Used by 5

Proof usesKullback–Leibler divergence on a finite space

Used byInformation content is a Kullback–Leibler divergence · Chow–Liu divergence as a Kullback–Leibler divergence · Vanishing conditional mutual information iff conditional independence · Nonnegativity of conditional mutual information · Cross-entropy is entropy plus divergence

DefinitionSurprisal#✓fully proved

The surprisal (information content) in bits of an outcome of probability \(q\) is \(-\log_2 q\), with value \(\infty\) when \(q = 0\). Formally \(q\) ranges over the extended nonnegative reals \([0, \infty]\): the surprisal of \(0\) is \(\infty\), the surprisal of \(q \in (0, \infty)\) is \(\max(0, -\log_2 q)\), and the surprisal of \(\infty\) is \(0\).

noncomputable def surprisal (q : ℝ≥0∞) : ℝ≥0∞ :=
  if q = 0 then ∞ else ENNReal.ofReal (-logb 2 q.toReal)

Used by 7

Used byThe cross-entropy loss is the average negative log-likelihood · Cross-entropy loss via the likelihood · The cross-entropy loss is infinite exactly when a label is ruled out · Cross-entropy · Cross-entropy is entropy plus divergence · Cross-entropy of a point mass · Cross-entropy is expected surprisal

DefinitionCross-entropy#✓fully proved

For probability mass functions \(p\) and \(q\) on a finite alphabet, the cross-entropy of \(q\) relative to \(p\) is \(H(p, q) = \sum_a p(a) \cdot (-\log_2 q(a))\) in bits, a value in \([0, \infty]\). Here \(-\log_2 q(a)\) is the surprisal of \(a\) under \(q\), which is \(\infty\) when \(q(a) = 0\), and a term with \(p(a) = 0\) contributes \(0\). So \(H(p, q)\) is \(\infty\) exactly when \(p\) charges an outcome that \(q\) rules out.

noncomputable def crossEntropy [Fintype α] (p q : PMF α) : ℝ≥0∞ := ∑ a, p a * surprisal (q a)

Uses 1 · Used by 7

Statement usesSurprisal

Used byCross-entropy loss · The cross-entropy loss is the average negative log-likelihood · Cross-entropy is entropy plus divergence · Equality in Gibbs' inequality · Cross-entropy of a point mass · Cross-entropy is expected surprisal · Gibbs' inequality

TheoremCross-entropy of a point mass#✓fully proved

For an outcome \(y\) of a finite alphabet and a probability mass function \(q\) on it, the cross-entropy \(H(\delta_y, q)\) of \(q\) relative to the point mass \(\delta_y\) at \(y\) equals the surprisal \(-\log_2 q(y)\) of \(y\) under \(q\), which is \(\infty\) when \(q(y) = 0\).

theorem crossEntropy_pure [Fintype α] (y : α) (q : PMF α) :
    crossEntropy (PMF.pure y) q = surprisal (q y)

Uses 2 · Used by 1

Statement usesCross-entropy · Surprisal

Used byThe cross-entropy loss is the average negative log-likelihood

TheoremCross-entropy is expected surprisal#✓fully proved

For probability mass functions \(p\) and \(q\) on a finite alphabet, the expected surprisal \(\mathbb{E}_{a \sim p}[-\log_2 q(a)]\) (with \(-\log_2 0 = \infty\)), taken as the integral of a \([0, \infty]\)-valued function with respect to the law \(p\), equals the cross-entropy \(H(p, q)\).

theorem lintegral_surprisal [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α]
    (p q : PMF α) : ∫⁻ a, surprisal (q a) ∂p.toMeasure = crossEntropy p q

Uses 2

Statement usesCross-entropy · Surprisal

TheoremCross-entropy is entropy plus divergence#✓fully proved

For probability mass functions \(p\) and \(q\) on a finite alphabet, the cross-entropy \(H(p, q)\) in bits equals \(H(p) + D(p \parallel q) / \ln 2\), where \(H(p)\) is the Shannon entropy of \(p\) in bits and \(D(p \parallel q)\) is the Kullback–Leibler divergence of \(p\) from \(q\) with the natural logarithm. The identity holds in \([0, \infty]\) with no support hypothesis: when \(p\) charges an outcome that \(q\) rules out, both sides are \(\infty\).

theorem crossEntropy_eq_shannonEntropy_add_klDiv [Fintype α] [MeasurableSpace α]
    [MeasurableSingletonClass α] (p q : PMF α) :
    crossEntropy p q = ENNReal.ofReal (shannonEntropy p) +
      klDiv p.toMeasure q.toMeasure / ENNReal.ofReal (log 2)

Uses 4 · Used by 2

Statement usesCross-entropy · Shannon entropy

Proof usesSurprisal · Kullback–Leibler divergence of finite probability laws

Used byEquality in Gibbs' inequality · Gibbs' inequality

TheoremGibbs' inequality#✓fully proved

The cross-entropy of any prediction q is at least the entropy of the truth p.

theorem shannonEntropy_le_crossEntropy [Fintype α] [MeasurableSpace α]
    [MeasurableSingletonClass α] (p q : PMF α) :
    ENNReal.ofReal (shannonEntropy p) ≤ crossEntropy p q

Uses 3

Statement usesCross-entropy · Shannon entropy

Proof usesCross-entropy is entropy plus divergence

TheoremEquality in Gibbs' inequality#✓fully proved

For probability mass functions \(p\) and \(q\) on a finite alphabet, the cross-entropy \(H(p, q)\) in bits equals the Shannon entropy \(H(p)\) in bits if and only if \(q = p\). Thus log loss is a strictly proper scoring rule.

theorem crossEntropy_eq_shannonEntropy_iff [Fintype α] [MeasurableSpace α]
    [MeasurableSingletonClass α] (p q : PMF α) :
    crossEntropy p q = ENNReal.ofReal (shannonEntropy p) ↔ q = p

Uses 3

Statement usesCross-entropy · Shannon entropy

Proof usesCross-entropy is entropy plus divergence

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.