Kullback-Leibler divergence on FintypePMF

FintypePMF.klDiv Q P = ∑ h, Q.prob h · log (Q.prob h / P.prob h) with the convention 0 · log(0 / anything) = 0. An ℝ-valued, Finset.sum- based specialization of Mathlib.InformationTheory.klDiv to the Fintype-indexed setting, admitted under the proof-engineering specialization clause of CHARTER.md for the same reason as FintypePMF itself.

noncomputable def ProbabilityTheory.FintypePMF.klDiv {α : Type u_1} [Fintype α] (Q P : FintypePMF α) : ℝ

Kullback-Leibler divergence between two FintypePMFs (ℝ-valued, discrete).

klDiv Q P = ∑ h, Q.prob h · log (Q.prob h / P.prob h), with the convention 0 · log(0 / anything) = 0.

Equations

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