English
If μ ≪ ν and f is ν-a.e. measurable, then the RN-derivative of μ with density f equals f·(RN-deriv of μ with respect to ν) almost everywhere.
Русский
Если μ ⪯ ν и f ν-при почти всякой измеримости, то производная μ по ν после взятия плотности f равна f умножить на RN-дерив μ по ν почти всюду.
LaTeX
$$$(μ.withDensity f).rnDeriv ν =_{ν}^{ae} f \\cdot (μ.rnDeriv ν)$$$
Lean4
theorem rnDeriv_withDensity_left_of_absolutelyContinuous {ν : Measure α} [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν)
(hf : AEMeasurable f ν) : (μ.withDensity f).rnDeriv ν =ᵐ[ν] fun x ↦ f x * μ.rnDeriv ν x :=
by
refine (Measure.eq_rnDeriv₀ ?_ Measure.MutuallySingular.zero_left ?_).symm
· exact hf.mul (Measure.measurable_rnDeriv _ _).aemeasurable
· ext1 s hs
rw [zero_add, withDensity_apply _ hs, withDensity_apply _ hs]
conv_lhs => rw [← Measure.withDensity_rnDeriv_eq _ _ hμν]
rw [setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ _ _ _ hs]
· congr with x
rw [mul_comm]
simp only [Pi.mul_apply]
· refine ae_restrict_of_ae ?_
exact Measure.rnDeriv_lt_top _ _
· exact (Measure.measurable_rnDeriv _ _).aemeasurable
