English
The singular part of μ with respect to ν, after mapping by f, equals the map by f of the singular part of μ with respect to ν.
Русский
Сингулярная часть меры после отображения равна отображению сингулярной части по отображению.
LaTeX
$$$$ (\mu.map f).singularPart (\nu.map f) = (\mu.singularPart ν).map f $$$$
Lean4
theorem _root_.MeasurableEmbedding.singularPart_map (hf : MeasurableEmbedding f) (μ ν : Measure α) [SigmaFinite μ]
[SigmaFinite ν] : (μ.map f).singularPart (ν.map f) = (μ.singularPart ν).map f :=
by
have h_add : μ.map f = (μ.singularPart ν).map f + (ν.map f).withDensity ((μ.map f).rnDeriv (ν.map f)) :=
by
conv_lhs => rw [μ.haveLebesgueDecomposition_add ν]
rw [Measure.map_add _ _ hf.measurable, ← hf.map_withDensity_rnDeriv μ ν]
refine (Measure.eq_singularPart (Measure.measurable_rnDeriv _ _) ?_ h_add).symm
exact hf.mutuallySingular_map (μ.mutuallySingular_singularPart ν)
