English
If f is ν-a.e. measurable and f is finite ν-a.e., the RN-derivative of μ with density f equals f times the RN-derivative already present.
Русский
Если f ν-при почти любой измеримости и конечна почти всюду, то RN-дерив μ по ν с плотностью f равен f умножить на существующую RN-дерив μ по ν.
LaTeX
$$$(μ.withDensity f).rnDeriv ν =_{ν}^{ae} f \\cdot (μ.rnDeriv ν)$$$
Lean4
theorem rnDeriv_withDensity_left {μ ν : Measure α} [SigmaFinite μ] [SigmaFinite ν] (hfν : AEMeasurable f ν)
(hf_ne_top : ∀ᵐ x ∂μ, f x ≠ ∞) : (μ.withDensity f).rnDeriv ν =ᵐ[ν] fun x ↦ f x * μ.rnDeriv ν x :=
by
let μ' := ν.withDensity (μ.rnDeriv ν)
have hμ'ν : μ' ≪ ν := withDensity_absolutelyContinuous _ _
have h := rnDeriv_withDensity_left_of_absolutelyContinuous hμ'ν hfν
have h1 : μ'.rnDeriv ν =ᵐ[ν] μ.rnDeriv ν := Measure.rnDeriv_withDensity _ (Measure.measurable_rnDeriv _ _)
have h2 : (μ'.withDensity f).rnDeriv ν =ᵐ[ν] (μ.withDensity f).rnDeriv ν := by
exact rnDeriv_withDensity_withDensity_rnDeriv_left μ ν hf_ne_top
filter_upwards [h, h1, h2] with x hx hx1 hx2
rw [← hx2, hx, hx1]
