Kullback-Leibler divergence and kernel composition products

This file contains generic lemmas about Kullback-Leibler divergence and Radon-Nikodym derivatives for composition products of measures and kernels.

It is designed to sit next to Mathlib/Probability/Kernel/Composition/RadonNikodym.lean and Mathlib/InformationTheory/KullbackLeibler/ChainRule.lean. The theorem rnDeriv_compProd_right supplies the kernel-only Radon-Nikodym description that is left as a TODO in the former file, while klDiv_compProd_right packages the corresponding pointwise-integral formula for Kullback-Leibler divergence.

Main statements

• InformationTheory.klDiv_map_measurableEquiv: Kullback-Leibler divergence is invariant under a measurable equivalence.
• ProbabilityTheory.rnDeriv_compProd_right: the Radon-Nikodym derivative ∂(μ ⊗ₘ κ)/∂(μ ⊗ₘ η) is given by the Radon-Nikodym derivative of the kernels.
• ProbabilityTheory.klDiv_compProd_right: the Kullback-Leibler divergence klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η) is the integral of the pointwise kernel divergences.

The last two lemmas complement the existing composition-product Radon-Nikodym and KL chain-rule infrastructure in Mathlib, where the mixed-left-measure and additive chain-rule statements are already available.

theorem InformationTheory.klDiv_map_measurableEquiv {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : klDiv (MeasureTheory.Measure.map (⇑e) μ) (MeasureTheory.Measure.map (⇑e) ν) = klDiv μ ν

Kullback-Leibler divergence is invariant under a measurable equivalence.

theorem ProbabilityTheory.rnDeriv_compProd_right {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace.CountableOrCountablyGenerated α β] {μ : MeasureTheory.Measure α} {κ η : Kernel α β} [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η] : (μ.compProd κ).rnDeriv (μ.compProd η) =ᵐ[μ.compProd η] fun (p : α × β) => κ.rnDeriv η p.1 p.2

The Radon-Nikodym derivative of μ ⊗ₘ κ with respect to μ ⊗ₘ η is the pointwise Radon-Nikodym derivative of the kernels.

theorem ProbabilityTheory.klDiv_compProd_right {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace.CountableOrCountablyGenerated α β] {μ : MeasureTheory.Measure α} {κ η : Kernel α β} [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η] (h_ac : (μ.compProd κ).AbsolutelyContinuous (μ.compProd η)) : InformationTheory.klDiv (μ.compProd κ) (μ.compProd η) = ∫⁻ (a : α), InformationTheory.klDiv (κ a) (η a) ∂μ

The Kullback-Leibler divergence of μ ⊗ₘ κ with respect to μ ⊗ₘ η is the integral of the pointwise kernel divergences.