Lemmas related to the data-processing inequality for the Kullback–Leibler divergence

theorem InformationTheory.klDiv_map_eq_lintegral_klFun_condExp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hμν : μ.AbsolutelyContinuous ν) {g : α → β} (hg : Measurable g) : klDiv (MeasureTheory.Measure.map g μ) (MeasureTheory.Measure.map g ν) = ∫⁻ (x : α), ENNReal.ofReal (klFun (ν[fun (x : α) => (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g mβ] x)) ∂ν

The divergence of the images of μ ≪ ν by a measurable map g, as the integral of klFun of the conditional expectation of the density ∂μ/∂ν given g.

See klDiv_map_of_ac for a version of this lemma with a Bochner integral.