Conditional Kullback-Leibler divergence, integral form #

This file fills the explicit Mathlib TODO of Mathlib/InformationTheory/KullbackLeibler/ChainRule.lean:

Add a version of the chain rule for the integral form of the conditional KL divergence, i.e. μ[fun x ↦ klDiv (κ x) (η x)].

The main theorem klDiv_compProd_toReal_integral states that, when the two joint measures μ ⊗ₘ κ and μ ⊗ₘ η share the same first marginal μ, the toReal Kullback-Leibler divergence between them equals the μ-average of the fibrewise divergences:

(klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)).toReal = ∫ z, (klDiv (κ z) (η z)).toReal ∂μ.

The Mathlib chain rule klDiv_compProd_eq_add keeps the conditional KL term in the composition-product form klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η) precisely to avoid the measurability of z ↦ klDiv (κ z) (η z). Here we resolve that measurability and the integral identity.

Main statements #

• rnDeriv_compProd_eq_kernel_rnDeriv: the slice identity ∂(μ ⊗ₘ κ)/∂(μ ⊗ₘ η) (z, y) =ᵐ Kernel.rnDeriv κ η z y.
• klDiv_compProd_toReal_integral: the conditional KL integral form.

Proof strategy #

The slice identity is the linchpin. We use Measure.compProd_withDensity (μ ⊗ₘ (η.withDensity f) = (μ ⊗ₘ η).withDensity (fun p ↦ f p.1 p.2)) together with the kernel Radon-Nikodym facts Kernel.withDensity_rnDeriv_eq (η.withDensity (κ.rnDeriv η) a = κ a when κ a ≪ η a) and Measure.absolutelyContinuous_compProd_right_iff (μ ⊗ₘ κ ≪ μ ⊗ₘ η ↔ ∀ᵐ a ∂μ, κ a ≪ η a) to rewrite μ ⊗ₘ κ as (μ ⊗ₘ η).withDensity (fun p ↦ Kernel.rnDeriv κ η p.1 p.2), whence Measure.rnDeriv_withDensity reads off the joint Radon-Nikodym derivative.

For the integral, toReal_klDiv_eq_integral_klFun expresses both sides through klFun integrated against the dominating measure (μ ⊗ₘ η on the left, η z per fibre), and Measure.integral_compProd opens the joint klFun integral into the outer μ-integral.