Kullback-Leibler divergence of a conditional measure

The conditioning identity: for a probability measure μ and an event s of nonzero mass, klDiv (μ[|s]) μ = −log μ(s) — Bayesian update by pure restriction costs exactly the information content of the event.

[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 (μ s).toReal)

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.