Kullback-Leibler divergence of conditional measures

The conditioning identity: for a probability measure μ and an event s of nonzero mass, klDiv μ[|s] μ = −log μ(s), so Bayesian update by pure restriction costs exactly the information content of the event. More generally the divergence between two conditionings of one finite measure is the log of the ratio of the events' masses when the first event is almost contained in the second (klDiv_cond_cond), and infinite otherwise (klDiv_cond_cond_eq_top_iff).

[UPSTREAM] candidate for Mathlib/InformationTheory/KullbackLeibler/ (placement and namespace mirror ChainRule.lean, the directory's other file combining klDiv with probability constructions).

theorem InformationTheory.klDiv_cond_self {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {s : Set Ω} (hs : MeasurableSet s) (hs0 : μ s ≠ 0) : klDiv μ[|s] μ = ENNReal.ofReal (-Real.log (μ.real s))

The Kullback-Leibler divergence of the conditional measure μ[|s] from μ is the information content of the event: −log μ(s). The core of [Lev08]'s equivalence of relative-entropy difficulty and surprisal.

theorem InformationTheory.klDiv_cond_cond {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s t : Set Ω} (hs : MeasurableSet s) (ht : MeasurableSet t) (hs0 : μ s ≠ 0) (hst : s ≤ᵐ[μ] t) : klDiv μ[|s] μ[|t] = ENNReal.ofReal (Real.log (μ.real t / μ.real s))

The divergence between two conditionings of one measure, the first on an event almost contained in the second, is the log of the ratio of the events' masses.

theorem InformationTheory.klDiv_cond_cond_lt_iff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s t t' : Set Ω} (hs : MeasurableSet s) (ht : MeasurableSet t) (ht' : MeasurableSet t') (hs0 : μ s ≠ 0) (hst : s ≤ᵐ[μ] t) (hst' : s ≤ᵐ[μ] t') : klDiv μ[|s] μ[|t] < klDiv μ[|s] μ[|t'] ↔ μ t < μ t'

Among the events almost containing s, the one of smaller mass has its conditional closer to μ[|s].

theorem InformationTheory.klDiv_cond_cond_eq_top_iff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s t : Set Ω} (hs : MeasurableSet s) (ht : MeasurableSet t) : klDiv μ[|s] μ[|t] = ⊤ ↔ ¬s ≤ᵐ[μ] t

The divergence between two conditionings of one measure is infinite exactly when the first event is not almost contained in the second.