English
Under a measurable embedding f, the RN-derivative of pushforwards matches the original RN-derivative almost everywhere along the map.
Русский
При измеримо вложении f плотности переводятся через отображение так, что RN-деривив μ по ν сохраняется почти всюду вдоль f.
LaTeX
$$$$ (\mu.map f).rnDeriv (\nu.map f) (f x) =^\mathrm{ae}_{\nu} \mu.rnDeriv ν x $$$$
Lean4
theorem _root_.MeasurableEmbedding.rnDeriv_map (hf : MeasurableEmbedding f) (μ ν : Measure α) [SigmaFinite μ]
[SigmaFinite ν] : (fun x ↦ (μ.map f).rnDeriv (ν.map f) (f x)) =ᵐ[ν] μ.rnDeriv ν :=
by
rw [μ.haveLebesgueDecomposition_add ν, Measure.map_add _ _ hf.measurable]
have : SigmaFinite (map f ν) := hf.sigmaFinite_map
have : SigmaFinite (map f (μ.singularPart ν)) := hf.sigmaFinite_map
have : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν))) := hf.sigmaFinite_map
have h_add := Measure.rnDeriv_add' ((μ.singularPart ν).map f) ((ν.withDensity (μ.rnDeriv ν)).map f) (ν.map f)
rw [Filter.EventuallyEq, hf.ae_map_iff, ← Filter.EventuallyEq] at h_add
refine h_add.trans ((Measure.rnDeriv_add' _ _ _).trans ?_).symm
refine Filter.EventuallyEq.add ?_ ?_
· refine (Measure.rnDeriv_singularPart μ ν).trans ?_
symm
suffices (fun x ↦ ((μ.singularPart ν).map f).rnDeriv (ν.map f) x) =ᵐ[ν.map f] 0
by
rw [Filter.EventuallyEq, hf.ae_map_iff] at this
exact this
refine Measure.rnDeriv_eq_zero_of_mutuallySingular ?_ Measure.AbsolutelyContinuous.rfl
exact hf.mutuallySingular_map (μ.mutuallySingular_singularPart ν)
· exact (hf.rnDeriv_map_aux (withDensity_absolutelyContinuous _ _)).symm
