KL Divergence and Finite PMFs

Pure mathematical infrastructure for probability mass functions over finite types, KL divergence, cross-entropy, and expected values. No learning-theory types.

Main definitions

• FinitePMF : a probability mass function over a finite type
• klDivFinitePMF : KL divergence between two FinitePMFs
• crossEntropyFinitePMF : cross-entropy H(Q, P)
• expectFinitePMF : expected value E_{h~Q}[f(h)]
• HasPositivePrior : typeclass for PMFs with strictly positive weights

References

• Cover & Thomas, "Elements of Information Theory", Chapter 2

structure FinitePMF (H : Type u_1) [Fintype H] : Type u_1

A probability mass function over a finite type. Named FinitePMF to avoid conflict with Mathlib's PMF.

• prob : H → ℝ
• prob_nonneg (h : H) : 0 ≤ self.prob h
• prob_sum_one : ∑ h : H, self.prob h = 1

noncomputable def klDivFinitePMF {H : Type u_1} [Fintype H] (Q P : FinitePMF H) : ℝ

KL divergence between two FinitePMFs over a finite type. KL(Q‖P) = ∑_h Q(h) · log(Q(h)/P(h)). Convention: 0 · log(0/p) = 0.

Equations

• klDivFinitePMF Q P = ∑ h : H, if Q.prob h = 0 then 0 else Q.prob h * Real.log (Q.prob h / P.prob h)

noncomputable def crossEntropyFinitePMF {H : Type u_1} [Fintype H] (Q P : FinitePMF H) : ℝ

Cross-entropy: ∑_h Q(h) · log(1/P(h)). Equals KL(Q‖P) + H(Q) where H(Q) is Shannon entropy.

Equations

• crossEntropyFinitePMF Q P = ∑ h : H, if Q.prob h = 0 then 0 else Q.prob h * Real.log (1 / P.prob h)

noncomputable def expectFinitePMF {H : Type u_1} [Fintype H] (Q : FinitePMF H) (f : H → ℝ) : ℝ

Expected value of a real-valued function under a FinitePMF.

Equations

• expectFinitePMF Q f = ∑ h : H, Q.prob h * f h

class HasPositivePrior {H : Type u_1} [Fintype H] (P : FinitePMF H) : Prop

Typeclass asserting that a FinitePMF has strictly positive weights.

• pos (h : H) : 0 < P.prob h