English
If μ ≪ ν and both measures are σ-finite, then the reciprocal RN-derivative satisfies (μ.rnDeriv ν)^{-1} = ν.rnDeriv μ almost everywhere with respect to μ.
Русский
Если μ ⪯ ν и оба меры σ-конечны, то (dμ/dν)^{-1} = dν/dμ почти наверху μ.
LaTeX
$$$(μ.rnDeriv ν)^{-1} =_{μ}^{ae} ν.rnDeriv μ$$$
Lean4
theorem inv_rnDeriv [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) : (μ.rnDeriv ν)⁻¹ =ᵐ[μ] ν.rnDeriv μ :=
by
suffices
(μ.rnDeriv ν)⁻¹ =ᵐ[μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ ∧
ν.rnDeriv μ =ᵐ[μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
by
refine (this.1.trans (Filter.EventuallyEq.trans ?_ this.2.symm))
exact Measure.inv_rnDeriv_aux (absolutelyContinuous_withDensity_rnDeriv hμν) (withDensity_absolutelyContinuous _ _)
constructor
· filter_upwards [rnDeriv_withDensity_rnDeriv hμν] with x hx
simp only [Pi.inv_apply, inv_inj]
exact hx.symm
· exact (Measure.rnDeriv_withDensity μ (Measure.measurable_rnDeriv ν μ)).symm
