The Kullback–Leibler divergence of restrictions of measures

The Kullback–Leibler divergence of two finite measures is the sum of the divergences of their restrictions to a measurable set and to its complement, so that restricting both measures to a measurable set does not increase the divergence, and the divergence is the supremum of the divergences of the restrictions to an increasing sequence of measurable sets covering the space.

Main statements

• klDiv_restrict_add_restrict_compl: the divergence is the sum of the divergences of the restrictions to a measurable set and to its complement.
• klDiv_restrict_le: restricting both measures to a measurable set does not increase the divergence.
• klDiv_eq_iSup_restrict: the divergence is the supremum of the divergences of the restrictions to an increasing sequence of measurable sets covering the space.

theorem MeasureTheory.Measure.rnDeriv_restrict_restrict {α : Type u_1} {mα : MeasurableSpace α} (μ ν : Measure α) [μ.HaveLebesgueDecomposition ν] [SigmaFinite ν] {s : Set α} (hs : MeasurableSet s) : (μ.restrict s).rnDeriv (ν.restrict s) =ᵐ[ν.restrict s] μ.rnDeriv ν

The Radon–Nikodym derivative of μ.restrict s with respect to ν.restrict s is the Radon–Nikodym derivative of μ with respect to ν, ν.restrict s-almost everywhere.

theorem InformationTheory.klDiv_restrict_of_ac {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {s : Set α} (hμν : (μ.restrict s).AbsolutelyContinuous (ν.restrict s)) (hs : MeasurableSet s) : klDiv (μ.restrict s) (ν.restrict s) = ∫⁻ (x : α) in s, ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν

If the restrictions of μ and ν to a measurable set s satisfy μ.restrict s ≪ ν.restrict s, the divergence of those restrictions is the integral of klFun (∂μ/∂ν) over s.

theorem InformationTheory.klDiv_restrict_add_restrict_compl {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {s : Set α} (hs : MeasurableSet s) : klDiv (μ.restrict s) (ν.restrict s) + klDiv (μ.restrict sᶜ) (ν.restrict sᶜ) = klDiv μ ν

The divergence is the sum of the divergences of the restrictions to a measurable set and to its complement.

theorem InformationTheory.klDiv_restrict_le {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {s : Set α} (hs : MeasurableSet s) : klDiv (μ.restrict s) (ν.restrict s) ≤ klDiv μ ν

Restricting both measures to a measurable set does not increase the divergence.

theorem InformationTheory.klDiv_add_add_of_measure_eq_zero {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {s : Set α} {μ' ν' : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ'] [MeasureTheory.IsFiniteMeasure ν'] (hs : MeasurableSet s) (hμ : μ sᶜ = 0) (hν : ν sᶜ = 0) (hμ' : μ' s = 0) (hν' : ν' s = 0) : klDiv (μ + μ') (ν + ν') = klDiv μ ν + klDiv μ' ν'

The divergence of two finite measures supported on a measurable set s and its complement respectively is the sum of the divergences of the two parts.

theorem InformationTheory.klDiv_eq_iSup_restrict {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {s : ℕ → Set α} (hs : ∀ (n : ℕ), MeasurableSet (s n)) (h_mono : Monotone s) (h_univ : ⋃ (n : ℕ), s n = Set.univ) : klDiv μ ν = ⨆ (n : ℕ), klDiv (μ.restrict (s n)) (ν.restrict (s n))

Monotone convergence for the Kullback–Leibler divergence: the divergence is the supremum of the divergences of the restrictions to an increasing sequence of measurable sets covering the space.