Kullback-Leibler divergence

The Kullback-Leibler divergence is a measure of the difference between two measures.

Main definitions

• klDiv μ ν: Kullback-Leibler divergence between two measures, with value in ℝ≥0∞, defined as ∞ if μ is not absolutely continuous with respect to ν or if the log-likelihood ratio llr μ ν is not integrable with respect to μ, and by ENNReal.ofReal (∫ x, llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal) otherwise.

Note that our Kullback-Leibler divergence is nonnegative by definition (it takes value in ℝ≥0∞). However ∫ x, llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal is nonnegative for all finite measures μ ≪ ν, as proved in the lemma integral_llr_add_sub_measure_univ_nonneg. That lemma is our version of Gibbs' inequality ("the Kullback-Leibler divergence is nonnegative").

Main statements

• klDiv_eq_zero_iff : the Kullback-Leibler divergence between two finite measures is zero if and only if the two measures are equal.

Implementation details

The Kullback-Leibler divergence on probability measures is ∫ x, llr μ ν x ∂μ if μ ≪ ν (and the log-likelihood ratio is integrable) and ∞ otherwise. The definition we use extends this to finite measures by introducing a correction term (ν univ).toReal - (μ univ).toReal. The definition of the divergence thus uses the formula ∫ x, llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal, which is nonnegative for all finite measures μ ≪ ν. This also makes klDiv μ ν equal to an f-divergence: it equals the integral ∫ x, klFun (μ.rnDeriv ν x).toReal ∂ν, in which klFun x = x * log x + 1 - x.

theorem InformationTheory.klDiv_def {α : Type u_2} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) : klDiv μ ν = if μ.AbsolutelyContinuous ν ∧ MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ then ENNReal.ofReal (∫ (x : α), MeasureTheory.llr μ ν x ∂μ + (ν Set.univ).toReal - (μ Set.univ).toReal) else ⊤

@[irreducible]

noncomputable def InformationTheory.klDiv {α : Type u_2} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) : ENNReal

Kullback-Leibler divergence between two measures.

Equations

• One or more equations did not get rendered due to their size.

theorem InformationTheory.klDiv_of_ac_of_integrable {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (h1 : μ.AbsolutelyContinuous ν) (h2 : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) : klDiv μ ν = ENNReal.ofReal (∫ (x : α), MeasureTheory.llr μ ν x ∂μ + (ν Set.univ).toReal - (μ Set.univ).toReal)

@[simp]

theorem InformationTheory.klDiv_of_not_ac {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (h : ¬μ.AbsolutelyContinuous ν) : klDiv μ ν = ⊤

@[simp]

theorem InformationTheory.klDiv_of_not_integrable {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (h : ¬MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) : klDiv μ ν = ⊤

@[simp]

theorem InformationTheory.klDiv_self {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : klDiv μ μ = 0

@[simp]

theorem InformationTheory.klDiv_zero_left {α : Type u_1} {mα : MeasurableSpace α} {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure ν] : klDiv 0 ν = ν Set.univ

@[simp]

theorem InformationTheory.klDiv_zero_right {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NeZero μ] : klDiv μ 0 = ⊤

theorem InformationTheory.klDiv_eq_top_iff {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} : klDiv μ ν = ⊤ ↔ μ.AbsolutelyContinuous ν → ¬MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ

theorem InformationTheory.klDiv_ne_top_iff {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} : klDiv μ ν ≠ ⊤ ↔ μ.AbsolutelyContinuous ν ∧ MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ

theorem InformationTheory.klDiv_eq_integral_klFun {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : klDiv μ ν = if μ.AbsolutelyContinuous ν ∧ MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ⊤

theorem InformationTheory.klDiv_eq_lintegral_klFun {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : klDiv μ ν = if μ.AbsolutelyContinuous ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ⊤

theorem InformationTheory.integral_llr_add_sub_measure_univ_nonneg {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hμν : μ.AbsolutelyContinuous ν) (h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) : 0 ≤ ∫ (x : α), MeasureTheory.llr μ ν x ∂μ + (ν Set.univ).toReal - (μ Set.univ).toReal

Gibbs' inequality: the Kullback-Leibler divergence is nonnegative. Note that since klDiv takes value in ℝ≥0∞ (defined when it is finite as ENNReal.ofReal (...)), it is nonnegative by definition. This lemma proves that the argument of ENNReal.ofReal is also nonnegative.

theorem InformationTheory.toReal_klDiv {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : μ.AbsolutelyContinuous ν) (h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) : (klDiv μ ν).toReal = ∫ (a : α), MeasureTheory.llr μ ν a ∂μ + (ν Set.univ).toReal - (μ Set.univ).toReal

theorem InformationTheory.toReal_klDiv_of_measure_eq {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : μ.AbsolutelyContinuous ν) (h_eq : μ Set.univ = ν Set.univ) : (klDiv μ ν).toReal = ∫ (a : α), MeasureTheory.llr μ ν a ∂μ

If μ ≪ ν and μ univ = ν univ, then toReal of the Kullback-Leibler divergence is equal to an integral, without any integrability condition.

theorem InformationTheory.toReal_klDiv_eq_integral_klFun {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : μ.AbsolutelyContinuous ν) : (klDiv μ ν).toReal = ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν

theorem InformationTheory.integral_llr_add_mul_log_nonneg {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hμν : μ.AbsolutelyContinuous ν) (h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) : 0 ≤ ∫ (x : α), MeasureTheory.llr μ ν x ∂μ + (μ Set.univ).toReal * Real.log (ν Set.univ).toReal + 1 - (μ Set.univ).toReal

theorem InformationTheory.mul_klFun_le_toReal_klDiv {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hμν : μ.AbsolutelyContinuous ν) (h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) : (ν Set.univ).toReal * klFun ((μ Set.univ).toReal / (ν Set.univ).toReal) ≤ (klDiv μ ν).toReal

theorem InformationTheory.mul_log_le_toReal_klDiv {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hμν : μ.AbsolutelyContinuous ν) (h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) : (μ Set.univ).toReal * Real.log ((μ Set.univ).toReal / (ν Set.univ).toReal) + (ν Set.univ).toReal - (μ Set.univ).toReal ≤ (klDiv μ ν).toReal

theorem InformationTheory.mul_log_le_klDiv {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : ENNReal.ofReal ((μ Set.univ).toReal * Real.log ((μ Set.univ).toReal / (ν Set.univ).toReal) + (ν Set.univ).toReal - (μ Set.univ).toReal) ≤ klDiv μ ν

theorem InformationTheory.klDiv_eq_zero_iff {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : klDiv μ ν = 0 ↔ μ = ν

Converse Gibbs' inequality: the Kullback-Leibler divergence between two finite measures is zero if and only if the two measures are equal.