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 ∂μ + ν.real - μ.real univ) otherwise.

Note that our Kullback-Leibler divergence is nonnegative by definition (it takes value in ℝ≥0∞). However ∫ x, llr μ ν x ∂μ + ν.real univ - μ.real univ 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 ν.real univ - μ.real univ. The definition of the divergence thus uses the formula ∫ x, llr μ ν x ∂μ + ν.real univ - μ.real univ, 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 ∂μ + ν.real Set.univ - μ.real Set.univ) else ⊤

@[irreducible]

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

Kullback-Leibler divergence between two measures.

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 ∂μ + ν.real Set.univ - μ.real Set.univ)

@[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_ne_top {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (hμν : μ.AbsolutelyContinuous ν) (h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) : klDiv μ ν ≠ ⊤

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.klDiv_eq_lintegral_klFun_of_ac {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h_ac : μ.AbsolutelyContinuous ν) : klDiv μ ν = ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν

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 ∂μ + ν.real Set.univ - μ.real Set.univ

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 ∂μ + ν.real Set.univ - μ.real Set.univ

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.toReal_klDiv_smul_left {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hμν : μ.AbsolutelyContinuous ν) (h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) (c : NNReal) : (klDiv (c • μ) ν).toReal = ↑c * (klDiv μ ν).toReal + (1 - ↑c) * ν.real Set.univ + ↑c * Real.log ↑c * μ.real Set.univ

theorem InformationTheory.toReal_klDiv_smul_right_eq_smul_left {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hμν : μ.AbsolutelyContinuous ν) (h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) (c : NNReal) : (klDiv μ (c • ν)).toReal = ↑c * (klDiv (c⁻¹ • μ) ν).toReal

theorem InformationTheory.toReal_klDiv_smul_right {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hμν : μ.AbsolutelyContinuous ν) (h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) {c : NNReal} (hc : c ≠ 0) : (klDiv μ (c • ν)).toReal = (klDiv μ ν).toReal + (↑c - 1) * ν.real Set.univ - Real.log ↑c * μ.real Set.univ

theorem InformationTheory.toReal_klDiv_smul_same {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hμν : μ.AbsolutelyContinuous ν) (h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) (c : NNReal) : (klDiv (c • μ) (c • ν)).toReal = ↑c * (klDiv μ ν).toReal

theorem InformationTheory.klDiv_smul_right_eq_smul_left {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {c : NNReal} (hc : c ≠ 0) : klDiv μ (c • ν) = ↑c * klDiv (c⁻¹ • μ) ν

theorem InformationTheory.klDiv_smul_same {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (c : NNReal) : klDiv (c • μ) (c • ν) = ↑c * klDiv μ ν

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 ∂μ + μ.real Set.univ * Real.log (ν.real Set.univ) + 1 - μ.real Set.univ

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 μ ν) μ) : ν.real Set.univ * klFun (μ.real Set.univ / ν.real Set.univ) ≤ (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 μ ν) μ) : μ.real Set.univ * Real.log (μ.real Set.univ / ν.real Set.univ) + ν.real Set.univ - μ.real Set.univ ≤ (klDiv μ ν).toReal

theorem InformationTheory.mul_log_le_klDiv {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : ENNReal.ofReal (μ.real Set.univ * Real.log (μ.real Set.univ / ν.real Set.univ) + ν.real Set.univ - μ.real Set.univ) ≤ 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.