Change of variables in the source of a composition-product

Pulling a kernel back along a measurable map in its source, and pushing the resulting composition-product forward by that same map, is the same as moving the map onto the measure:

(μ ⊗ₘ κ.comap e he).map (Prod.map e id) = μ.map e ⊗ₘ κ

with the composition-level corollary (κ.comap e he) ∘ₘ μ = κ ∘ₘ μ.map e obtained by taking the second marginal.

Mathlib has Kernel.comap and Measure.compProd but not their interaction. The statement is proved on measurable rectangles, where both sides are the same integral after a change of variables.

e need only be measurable

An earlier private version of the first identity in Graphon.RelStepKernel asked for a measurable equivalence. Nothing in the argument uses an inverse: the preimage step is definitional for Prod.map e id, and setLIntegral_map needs only measurability. Consumers that want to cancel the pushforward — to conclude equality of the arguments rather than of the images — need MeasurableEmbedding e, but that is their hypothesis to carry, not this one's; surjectivity is never used on either side.

theorem MeasureTheory.Measure.map_prodMap_compProd_comap {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (μ : Measure α) [IsFiniteMeasure μ] {e : α → β} (he : Measurable e) (κ : ProbabilityTheory.Kernel β γ) [ProbabilityTheory.IsFiniteKernel κ] : map (Prod.map e id) (μ.compProd (κ.comap e he)) = (map e μ).compProd κ

Change of variables for ⊗ₘ in the source. Pushing μ ⊗ₘ κ.comap e forward by e × id is μ.map e ⊗ₘ κ.

theorem MeasureTheory.Measure.comp_comap {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (μ : Measure α) [IsFiniteMeasure μ] {e : α → β} (he : Measurable e) (κ : ProbabilityTheory.Kernel β γ) [ProbabilityTheory.IsFiniteKernel κ] : μ.bind ⇑(κ.comap e he) = (map e μ).bind ⇑κ

Change of variables for ∘ₘ in the source, the second marginal of Measure.map_prodMap_compProd_comap.