Kullback–Leibler divergence on a finite type #
On a finite type with measurable singletons the Radon–Nikodym derivative is the ratio of atom
masses, so klDiv is a finite sum, and for probability measures its real part is the textbook
relative entropy ∑ a, μ {a} * log (μ {a} / ν {a}) ([CT06], chapter 2).
[UPSTREAM] candidate for Mathlib/InformationTheory/KullbackLeibler/.
theorem
InformationTheory.klDiv_eq_top_iff_not_ac
{α : Type u_1}
[MeasurableSpace α]
[MeasurableSingletonClass α]
[Fintype α]
{μ ν : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
:
klDiv μ ν = ⊤ ↔ ¬μ.AbsolutelyContinuous ν
On a finite type the log-likelihood ratio is integrable, so the divergence is infinite exactly when the first measure is not absolutely continuous with respect to the second.
theorem
InformationTheory.klDiv_eq_sum_klFun
{α : Type u_1}
[MeasurableSpace α]
[MeasurableSingletonClass α]
[Fintype α]
{μ ν : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hμν : μ.AbsolutelyContinuous ν)
:
klDiv μ ν = ∑ a : α, ν {a} * ENNReal.ofReal (klFun (μ {a} / ν {a}).toReal)
theorem
InformationTheory.toReal_klDiv_eq_sum_log_div
{α : Type u_1}
[MeasurableSpace α]
[MeasurableSingletonClass α]
[Fintype α]
{μ ν : MeasureTheory.Measure α}
[MeasureTheory.IsProbabilityMeasure μ]
[MeasureTheory.IsProbabilityMeasure ν]
(hμν : μ.AbsolutelyContinuous ν)
:
(klDiv μ ν).toReal = ∑ a : α, μ.real {a} * Real.log (μ.real {a} / ν.real {a})