English
A composition-product of a measure with a kernel defined via withDensity equals the withDensity of the composition-product.
Русский
Произведение-композиция меры с ядром через withDensity равняется withDensity от композиции меры.
LaTeX
$$$\\mu \\otimes_{\\! m} (\\kappa \\text{ withDensity } f) = (\\mu \\otimes_{\\! m} \\kappa) \\text{ withDensity } (p \\mapsto f(p_1, p_2))$$$
Lean4
/-- A composition-product of a measure with a kernel defined with `withDensity` is equal to the
`withDensity` of the composition-product. -/
theorem compProd_withDensity [SFinite μ] [IsSFiniteKernel κ] [IsSFiniteKernel (κ.withDensity f)]
(hf : Measurable (Function.uncurry f)) : μ ⊗ₘ (κ.withDensity f) = (μ ⊗ₘ κ).withDensity (fun p ↦ f p.1 p.2) :=
by
ext s hs
rw [compProd_apply hs, withDensity_apply _ hs, ← lintegral_indicator hs, lintegral_compProd]
· congr with a
rw [Kernel.withDensity_apply' _ hf, ← lintegral_indicator (measurable_prodMk_left hs)]
rfl
· exact hf.indicator hs
