English
If ν ≪ κ and μ ≪ ν with σ-finiteness, then the product μ.rnDeriv ν · ν.rnDeriv κ equals μ.rnDeriv κ almost everywhere with respect to ν.
Русский
Если ν ≪ κ и μ ≪ ν с σ–конечностью, то произведение μ.rnDeriv ν и ν.rnDeriv κ равно μ.rnDeriv κ почти по ν.
LaTeX
$$$$ μ.rnDeriv ν · ν.rnDeriv κ =^\mathrm{ae}_{ν} μ.rnDeriv κ $$$$
Lean4
theorem rnDeriv_mul_rnDeriv' {κ : Measure α} [SigmaFinite μ] [SigmaFinite ν] [SigmaFinite κ] (hνκ : ν ≪ κ) :
μ.rnDeriv ν * ν.rnDeriv κ =ᵐ[ν] μ.rnDeriv κ :=
by
obtain ⟨h_meas, h_sing, hμν⟩ := Measure.haveLebesgueDecomposition_spec μ ν
filter_upwards [hνκ <| Measure.rnDeriv_add' (μ.singularPart ν) (ν.withDensity (μ.rnDeriv ν)) κ,
hνκ <| Measure.rnDeriv_withDensity_left_of_absolutelyContinuous hνκ h_meas.aemeasurable,
Measure.rnDeriv_eq_zero_of_mutuallySingular h_sing hνκ] with x hx1 hx2 hx3
nth_rw 2 [hμν]
rw [hx1, Pi.add_apply, hx2, Pi.mul_apply, hx3, Pi.zero_apply, zero_add]
