Pushing the base of a composition-product along a map the kernel factors through

Mathlib's MeasureTheory.Measure.compProd records how μ ⊗ₘ κ reacts to operations on the kernel, but not what happens when the base measure is pushed forward. In general nothing does: (μ ⊗ₘ κ).map (Prod.map f id) cannot be read off μ.map f, because κ still sees the finer information carried by the points of the source. The one case in which it can is exactly the case in which κ itself factors through f, and that case is the content of this file.

Main statements

• TauCeti.Measure.map_prodMap_compProd_comap — for f : W → Y measurable and κ : Kernel Y Z, (μ ⊗ₘ κ.comap f hf).map (Prod.map f id) = μ.map f ⊗ₘ κ.

theorem TauCeti.Measure.map_prodMap_compProd_comap {W : Type u_1} {Y : Type u_2} {Z : Type u_3} [MeasurableSpace W] [MeasurableSpace Y] [MeasurableSpace Z] (μ : MeasureTheory.Measure W) [MeasureTheory.SFinite μ] (κ : ProbabilityTheory.Kernel Y Z) [ProbabilityTheory.IsSFiniteKernel κ] {f : W → Y} (hf : Measurable f) : MeasureTheory.Measure.map (Prod.map f id) (μ.compProd (κ.comap f hf)) = (MeasureTheory.Measure.map f μ).compProd κ

If a kernel factors through a measurable map f : W → Y, then pushing the base of the composition-product forward along f gives back the composition-product over the pushed-forward base: (μ ⊗ₘ κ.comap f hf).map (Prod.map f id) = μ.map f ⊗ₘ κ.

Without the factorization hypothesis the left-hand side genuinely depends on more than μ.map f, so the comap on the left is not decoration.