English
If μ ≪ ν and both measures are σ-finite, then (ν.rnDeriv μ)⁻¹ =ᵐ[μ] μ.rnDeriv ν.
Русский
Если μ ≪ ν и оба меры σ-конечны, то (dν/dμ)^{-1} = dμ/dν почти наверху μ.
LaTeX
$$$(ν.rnDeriv μ)^{-1} =_{μ}^{ae} μ.rnDeriv ν$$$
Lean4
/-- Auxiliary lemma for `inv_rnDeriv`. -/
theorem inv_rnDeriv_aux [HaveLebesgueDecomposition μ ν] [HaveLebesgueDecomposition ν μ] [SigmaFinite μ] (hμν : μ ≪ ν)
(hνμ : ν ≪ μ) : (μ.rnDeriv ν)⁻¹ =ᵐ[μ] ν.rnDeriv μ :=
by
suffices μ.withDensity (μ.rnDeriv ν)⁻¹ = μ.withDensity (ν.rnDeriv μ) by
calc
(μ.rnDeriv ν)⁻¹ =ᵐ[μ] (μ.withDensity (μ.rnDeriv ν)⁻¹).rnDeriv μ :=
(rnDeriv_withDensity _ (measurable_rnDeriv _ _).inv).symm
_ = (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ := by rw [this]
_ =ᵐ[μ] ν.rnDeriv μ := rnDeriv_withDensity _ (measurable_rnDeriv _ _)
rw [withDensity_rnDeriv_eq _ _ hνμ, ← withDensity_rnDeriv_eq _ _ hμν]
conv in ((ν.withDensity (μ.rnDeriv ν)).rnDeriv ν)⁻¹ => rw [withDensity_rnDeriv_eq _ _ hμν]
change (ν.withDensity (μ.rnDeriv ν)).withDensity (fun x ↦ (μ.rnDeriv ν x)⁻¹) = ν
rw [withDensity_inv_same (measurable_rnDeriv _ _)
(by filter_upwards [hνμ.ae_le (rnDeriv_pos hμν)] with x hx using hx.ne') (rnDeriv_ne_top _ _)]
