Kullback–Leibler divergence of finite distributions

The library has one divergence notion, Mathlib's InformationTheory.klDiv, and one entropy notion, Cslib.Probability.PMF.entropy. This file bridges them. For PMFs on a finite type with a discrete measurable structure, klDiv p.toMeasure q.toMeasure is finite exactly when the support of p is contained in that of q, and is then the finite sum ∑ a, p a * log (p a / q a) in nats. Consequences:

• Gibbs' inequality: the sum is nonnegative and vanishes only at p = q. Equivalently, the entropy of p is at most its cross-entropy ∑ a, p a * surprisal q a.
• Entropy is the logarithm of the alphabet size minus the divergence from uniform.
• Mutual information, H(X) + H(Y) - H(X, Y), is the divergence of the joint law from the product of its marginals. Entropy is subadditive and conditioning cannot increase it; by the equality case of Gibbs' inequality, subadditivity is an equality exactly for independent pairs.
• Pinsker's inequality 2 δ(p, q)² ≤ D(p ‖ q) for the statistical distance δ, from the form for arbitrary probability measures and events in Probability/Pinsker. Statistical distance is half of Mathlib's total variation distance tvDist.

Divergences are in nats and entropies in bits, so the bridges divide by log 2.

Main results

• Cslib.Probability.PMF.toReal_klDiv_toMeasure: the finite-sum formula.
• Cslib.Probability.PMF.klDiv_toMeasure_ne_top_iff: finiteness is support inclusion.
• Cslib.Probability.PMF.klDiv_toMeasure_map_le: data processing for deterministic maps.
• Cslib.Probability.PMF.sum_mul_log_div_nonneg, .sum_mul_log_div_eq_zero_iff: Gibbs.
• Cslib.Probability.PMF.entropy_le_sum_mul_surprisal: entropy is at most cross-entropy.
• Cslib.Probability.PMF.entropy_le_logb_card_of_support_subset: entropy is at most the logarithm of the support size.
• Cslib.Probability.PMF.entropy_eq_logb_card_sub_klDiv: entropy and divergence from uniform.
• Cslib.Probability.PMF.entropy_map_fst_add_entropy_map_snd_sub_entropy: mutual information.
• Cslib.Probability.PMF.entropy_le_entropy_map_fst_add_entropy_map_snd: subadditivity, with equality exactly for independent pairs (Cslib.Probability.PMF.entropy_eq_entropy_map_fst_add_entropy_map_snd_iff).
• Cslib.Probability.PMF.conditionalEntropy_le_entropy_map_snd: conditioning reduces entropy.
• Cslib.Probability.PMF.ofReal_two_mul_dist_sq_le_klDiv, Cslib.Probability.PMF.dist_le_sqrt_toReal_klDiv_div_two: Pinsker's inequality.

References

• T. M. Cover, J. A. Thomas, Elements of Information Theory, Theorems 2.6.3 (Gibbs), 2.6.4 (uniform maximizes entropy), 2.6.5 (conditioning reduces entropy), 2.6.6 (independence bound on entropy, here for two variables), Section 2.3 and Theorem 2.4.1 (mutual information) and Lemma 11.6.1 (Pinsker).

The finite-sum formula

theorem Cslib.Probability.PMF.toMeasure_absolutelyContinuous_iff {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Countable α] {p q : PMF α} : p.toMeasure.AbsolutelyContinuous q.toMeasure ↔ p.support ⊆ q.support

A PMF measure on a countable type is absolutely continuous with respect to another exactly when its support is contained in the other's support.

theorem Cslib.Probability.PMF.toReal_klDiv_toMeasure {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype α] {p q : PMF α} (h : p.support ⊆ q.support) : (InformationTheory.klDiv p.toMeasure q.toMeasure).toReal = ∑ a : α, (p a).toReal * Real.log ((p a).toReal / (q a).toReal)

The finite-sum formula for the Kullback–Leibler divergence of finite distributions, in nats. Null outcomes of p contribute zero.

theorem Cslib.Probability.PMF.klDiv_toMeasure_ne_top_iff {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Finite α] {p q : PMF α} : InformationTheory.klDiv p.toMeasure q.toMeasure ≠ ⊤ ↔ p.support ⊆ q.support

The divergence of finite distributions is finite exactly when the support of the first is contained in the support of the second.

theorem Cslib.Probability.PMF.klDiv_toMeasure_eq_ofReal {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype α] {p q : PMF α} (h : p.support ⊆ q.support) : InformationTheory.klDiv p.toMeasure q.toMeasure = ENNReal.ofReal (∑ a : α, (p a).toReal * Real.log ((p a).toReal / (q a).toReal))

The divergence of finite distributions with nested supports, as an extended real.

theorem Cslib.Probability.PMF.klDiv_toMeasure_map_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSingletonClass α] [Countable α] [MeasurableSpace β] (p q : PMF α) (f : α → β) : InformationTheory.klDiv (PMF.map f p).toMeasure (PMF.map f q).toMeasure ≤ InformationTheory.klDiv p.toMeasure q.toMeasure

Data processing: a deterministic map cannot increase the divergence of distributions on a countable type.

Gibbs' inequality

theorem Cslib.Probability.PMF.sum_mul_log_div_nonneg {α : Type u_1} [Fintype α] {p q : PMF α} (h : p.support ⊆ q.support) : 0 ≤ ∑ a : α, (p a).toReal * Real.log ((p a).toReal / (q a).toReal)

Gibbs' inequality: the divergence sum of finite distributions is nonnegative.

theorem Cslib.Probability.PMF.sum_mul_log_div_eq_zero_iff {α : Type u_1} [Fintype α] {p q : PMF α} (h : p.support ⊆ q.support) : ∑ a : α, (p a).toReal * Real.log ((p a).toReal / (q a).toReal) = 0 ↔ p = q

The equality case of Gibbs' inequality: the divergence sum vanishes only for equal distributions.

theorem Cslib.Probability.PMF.entropy_le_sum_mul_surprisal {α : Type u_1} [Fintype α] {p q : PMF α} (h : p.support ⊆ q.support) : entropy p ≤ ∑ a : α, (p a).toReal * surprisal q a

Gibbs' inequality in entropy form: the entropy of p is at most its cross-entropy relative to any q whose support contains that of p.

theorem Cslib.Probability.PMF.entropy_uniformOfFinset {α : Type u_1} [Finite α] (s : Finset α) (hs : s.Nonempty) : entropy (uniformOfFinset s hs) = Real.logb 2 ↑s.card

The uniform distribution on a nonempty finite set has the logarithm of its size as entropy.

theorem Cslib.Probability.PMF.entropy_le_logb_card_of_support_subset {α : Type u_1} [Finite α] (p : PMF α) {s : Finset α} (h : p.support ⊆ ↑s) : entropy p ≤ Real.logb 2 ↑s.card

A distribution supported on a finite set s has entropy at most log₂ |s|. This is Gibbs' inequality against the uniform distribution on s.

theorem Cslib.Probability.PMF.entropy_eq_logb_card_sub_klDiv {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (p : PMF α) : entropy p = Real.logb 2 ↑(Fintype.card α) - (InformationTheory.klDiv p.toMeasure (uniformOfFintype α).toMeasure).toReal / Real.log 2

Entropy is the logarithm of the alphabet size minus the divergence from the uniform distribution, converted to bits.

Mutual information and subadditivity

theorem Cslib.Probability.PMF.entropy_map_fst_add_entropy_map_snd_sub_entropy {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] [MeasurableSpace α] [MeasurableSingletonClass α] [MeasurableSpace β] [MeasurableSingletonClass β] (joint : PMF (α × β)) : entropy (PMF.map Prod.fst joint) + entropy (PMF.map Prod.snd joint) - entropy joint = (InformationTheory.klDiv joint.toMeasure ((PMF.map Prod.fst joint).toMeasure.prod (PMF.map Prod.snd joint).toMeasure)).toReal / Real.log 2

Mutual information I(X; Y) = H(X) + H(Y) - H(X, Y), in bits, is the divergence of the joint law from the product of its marginals.

theorem Cslib.Probability.PMF.conditionalEntropy_le_entropy_map_snd {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] (joint : PMF (α × β)) : conditionalEntropy joint ≤ entropy (PMF.map Prod.snd joint)

Conditioning reduces entropy: the entropy of the second component given the first is at most its unconditional entropy.

theorem Cslib.Probability.PMF.entropy_le_entropy_map_fst_add_entropy_map_snd {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] (joint : PMF (α × β)) : entropy joint ≤ entropy (PMF.map Prod.fst joint) + entropy (PMF.map Prod.snd joint)

Subadditivity of entropy: the joint entropy is at most the sum of the marginal entropies ([CT06], Theorem 2.6.6 for two variables).

theorem Cslib.Probability.PMF.entropy_eq_entropy_map_fst_add_entropy_map_snd_iff {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] (joint : PMF (α × β)) : entropy joint = entropy (PMF.map Prod.fst joint) + entropy (PMF.map Prod.snd joint) ↔ joint = (PMF.map Prod.fst joint).bind fun (a : α) => PMF.map (fun (x : β) => (a, x)) (PMF.map Prod.snd joint)

Subadditivity of entropy is an equality exactly for independent pairs, whose joint law is the product of its marginals.

Pinsker's inequality

theorem Cslib.Probability.PMF.ofReal_two_mul_dist_sq_le_klDiv {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (p q : PMF α) : ENNReal.ofReal (2 * dist p q ^ 2) ≤ InformationTheory.klDiv p.toMeasure q.toMeasure

Pinsker's inequality for finite distributions: twice the squared statistical distance is at most the Kullback–Leibler divergence, in nats.

theorem Cslib.Probability.PMF.two_mul_dist_sq_le_sum_mul_log_div {α : Type u_1} [Fintype α] {p q : PMF α} (h : p.support ⊆ q.support) : 2 * dist p q ^ 2 ≤ ∑ a : α, (p a).toReal * Real.log ((p a).toReal / (q a).toReal)

Pinsker's inequality with a finite-sum divergence.

theorem Cslib.Probability.PMF.dist_le_sqrt_toReal_klDiv_div_two {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] {p q : PMF α} (h : p.support ⊆ q.support) : dist p q ≤ √((InformationTheory.klDiv p.toMeasure q.toMeasure).toReal / 2)

Pinsker's inequality in its usual form: statistical distance is at most sqrt (D(p ‖ q) / 2), the divergence in nats.