KL Divergence

This file imports Mathlib's Kullback-Leibler divergence development for use in the project.

theorem CommunicationComplexity.FiniteMeasureSpace.klDiv_eq_sum_llr {Ω : Type u_1} [MeasurableSpace Ω] [FiniteMeasureSpace Ω] (μ ν : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : InformationTheory.klDiv μ ν = if ∃ (ω : Ω), ν {ω} = 0 ∧ μ {ω} ≠ 0 then ⊤ else ENNReal.ofReal (∑ ω : Ω, μ.real {ω} * MeasureTheory.llr μ ν ω + ν.real Set.univ - μ.real Set.univ)

On a finite measurable space, the Kullback-Leibler divergence between finite measures is ∞ exactly in the displayed formula when some singleton has zero ν-mass and nonzero μ-mass; otherwise it is the finite sum of the log-likelihood ratio against the singleton masses, with Mathlib's finite-measure correction term.

theorem CommunicationComplexity.FiniteMeasureSpace.probabilityMeasure_klDiv_eq_sum_llr {Ω : Type u_1} [MeasurableSpace Ω] [FiniteMeasureSpace Ω] (μ ν : MeasureTheory.ProbabilityMeasure Ω) : InformationTheory.klDiv ↑μ ↑ν = if ∃ (ω : Ω), (↑ν).toPMF ω = 0 ∧ (↑μ).toPMF ω ≠ 0 then ⊤ else ENNReal.ofReal (∑ ω : Ω, ((↑μ).toPMF ω).toReal * MeasureTheory.llr (↑μ) (↑ν) ω)

On a finite measurable space, the Kullback-Leibler divergence between probability measures is ∞ if some singleton has zero ν-mass and nonzero μ-mass; otherwise it is a finite sum over the PMFs.

theorem CommunicationComplexity.FiniteMeasureSpace.pmf_klDiv_eq_sum_llr {Ω : Type u_1} [MeasurableSpace Ω] [FiniteMeasureSpace Ω] (p q : PMF Ω) : InformationTheory.klDiv p.toMeasure q.toMeasure = if ∃ (ω : Ω), q ω = 0 ∧ p ω ≠ 0 then ⊤ else ENNReal.ofReal (∑ ω : Ω, (p ω).toReal * MeasureTheory.llr p.toMeasure q.toMeasure ω)

On a finite measurable space, the Kullback-Leibler divergence between PMFs is ∞ if some point has zero q-mass and nonzero p-mass; otherwise it is a finite sum over the PMFs.

theorem CommunicationComplexity.FiniteMeasureSpace.klDiv_eq_sum_log {Ω : Type u_1} [MeasurableSpace Ω] [FiniteMeasureSpace Ω] (μ ν : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : InformationTheory.klDiv μ ν = if ∃ (ω : Ω), ν {ω} = 0 ∧ μ {ω} ≠ 0 then ⊤ else ENNReal.ofReal (∑ ω : Ω, μ.real {ω} * Real.log (μ.real {ω} / ν.real {ω}) + ν.real Set.univ - μ.real Set.univ)

On a finite measurable space, the Kullback-Leibler divergence between finite measures is ∞ if some singleton has zero ν-mass and nonzero μ-mass; otherwise it is the finite sum of μ {ω} * log (μ {ω} / ν {ω}), with Mathlib's finite-measure correction term.

theorem CommunicationComplexity.FiniteMeasureSpace.probabilityMeasure_klDiv_eq_sum_log {Ω : Type u_1} [MeasurableSpace Ω] [FiniteMeasureSpace Ω] (μ ν : MeasureTheory.ProbabilityMeasure Ω) : InformationTheory.klDiv ↑μ ↑ν = if ∃ (ω : Ω), (↑ν).toPMF ω = 0 ∧ (↑μ).toPMF ω ≠ 0 then ⊤ else ENNReal.ofReal (∑ ω : Ω, ((↑μ).toPMF ω).toReal * Real.log (((↑μ).toPMF ω).toReal / ((↑ν).toPMF ω).toReal))

On a finite measurable space, the Kullback-Leibler divergence between probability measures is ∞ if some singleton has zero ν-mass and nonzero μ-mass; otherwise it is the finite sum of p ω * log (p ω / q ω), where p and q are the PMFs of the two measures.

theorem CommunicationComplexity.FiniteMeasureSpace.probabilityMeasure_klDiv_ne_top_of_forall_toPMF_ne_zero {Ω : Type u_1} [MeasurableSpace Ω] [FiniteMeasureSpace Ω] (μ ν : MeasureTheory.ProbabilityMeasure Ω) (hν : ∀ (ω : Ω), (↑ν).toPMF ω ≠ 0) : InformationTheory.klDiv ↑μ ↑ν ≠ ⊤

On a finite space, KL divergence from μ to a probability measure with full support is finite.

theorem CommunicationComplexity.FiniteMeasureSpace.pmf_klDiv_eq_sum_log {Ω : Type u_1} [MeasurableSpace Ω] [FiniteMeasureSpace Ω] (p q : PMF Ω) : InformationTheory.klDiv p.toMeasure q.toMeasure = if ∃ (ω : Ω), q ω = 0 ∧ p ω ≠ 0 then ⊤ else ENNReal.ofReal (∑ ω : Ω, (p ω).toReal * Real.log ((p ω).toReal / (q ω).toReal))

On a finite measurable space, the Kullback-Leibler divergence between PMFs is ∞ if some point has zero q-mass and nonzero p-mass; otherwise it is ∑ ω, p ω * log (p ω / q ω).