Kullback-Leibler divergence: probability-measure forms

Extensions to mathlib's InformationTheory/KullbackLeibler/Basic.lean, its [UPSTREAM] home. For probability measures the finite-measure correction term in klDiv cancels, giving the textbook integral form; a distribution whose density is a.e. constant has KL divergence log c.

theorem InformationTheory.klDiv_eq_ofReal_integral_llr {Ω : Type u_1} [MeasurableSpace Ω] {μ ν : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hμν : μ.AbsolutelyContinuous ν) (hint : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) : klDiv μ ν = ENNReal.ofReal (∫ (x : Ω), MeasureTheory.llr μ ν x ∂μ)

For probability measures, klDiv is the integral of the log-likelihood ratio: the finite-measure correction term cancels.

theorem InformationTheory.klDiv_of_llr_ae_const {Ω : Type u_1} [MeasurableSpace Ω] {μ ν : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hμν : μ.AbsolutelyContinuous ν) {r : ℝ} (h : MeasureTheory.llr μ ν =ᵐ[μ] fun (x : Ω) => r) : klDiv μ ν = ENNReal.ofReal r

A distribution whose log-likelihood ratio to ν is a.e. the constant r has KL divergence r from it.

theorem InformationTheory.klDiv_of_rnDeriv_ae_const {Ω : Type u_1} [MeasurableSpace Ω] {μ ν : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hμν : μ.AbsolutelyContinuous ν) {c : ENNReal} (h : μ.rnDeriv ν =ᵐ[μ] fun (x : Ω) => c) : klDiv μ ν = ENNReal.ofReal (Real.log c.toReal)

A distribution whose density with respect to ν is a.e. the constant c has KL divergence log c from it.