English
If μ ≪ ν and ν ⟂ ν' with Lebesgue decompositions present, the RN-derivative with respect to ν+ν' equals the RN-derivative with respect to ν, almost everywhere on ν.
Русский
Если μ ≪ ν и ν ⟂ ν' и существуют разложения Лебега, то RN-дерив μ по ν+ν' равен RN-дериву μ по ν почти всюду на ν.
LaTeX
$$$μ.rnDeriv(ν+ν') =_{ν}^{ae} μ.rnDeriv ν$$$
Lean4
theorem rnDeriv_withDensity_right (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] (hf : AEMeasurable f ν)
(hf_ne_zero : ∀ᵐ x ∂ν, f x ≠ 0) (hf_ne_top : ∀ᵐ x ∂ν, f x ≠ ∞) :
μ.rnDeriv (ν.withDensity f) =ᵐ[ν] fun x ↦ (f x)⁻¹ * μ.rnDeriv ν x :=
by
let μ' := ν.withDensity (μ.rnDeriv ν)
have h₁ : μ'.rnDeriv (ν.withDensity f) =ᵐ[ν] μ.rnDeriv (ν.withDensity f) :=
rnDeriv_withDensity_withDensity_rnDeriv_right μ ν hf hf_ne_zero hf_ne_top
have h₂ : μ.rnDeriv ν =ᵐ[ν] μ'.rnDeriv ν := (Measure.rnDeriv_withDensity _ (Measure.measurable_rnDeriv _ _)).symm
have hμ' :=
rnDeriv_withDensity_right_of_absolutelyContinuous (withDensity_absolutelyContinuous ν (μ.rnDeriv ν)) hf hf_ne_zero
hf_ne_top
filter_upwards [h₁, h₂, hμ'] with x hx₁ hx₂ hx_eq
rw [← hx₁, hx₂, hx_eq]
