English
A density-compatibility statement for measure maps and densities under a measurable embedding, showing the density of pushforwards equals the pushforward density.
Русский
Совместимость плотностей между мерами и их образами через измеримое вложение: плотность перехода соответствует образу плотности.
LaTeX
$$$$ (\nu.withDensity (\mu.rnDeriv ν)).map f = (\nu.map f).withDensity ((\mu.map f).rnDeriv (\nu.map f)) $$$$
Lean4
theorem _root_.MeasurableEmbedding.map_withDensity_rnDeriv (hf : MeasurableEmbedding f) (μ ν : Measure α)
[SigmaFinite μ] [SigmaFinite ν] :
(ν.withDensity (μ.rnDeriv ν)).map f = (ν.map f).withDensity ((μ.map f).rnDeriv (ν.map f)) :=
by
ext s hs
rw [hf.map_apply, withDensity_apply _ (hf.measurable hs), withDensity_apply _ hs,
setLIntegral_map hs (Measure.measurable_rnDeriv _ _) hf.measurable]
refine setLIntegral_congr_fun_ae (hf.measurable hs) ?_
filter_upwards [hf.rnDeriv_map μ ν] with a ha _ using ha.symm
