rnDeriv_eq_one_iff_eq — Mathlib

English

If HaveLebesgueDecomposition μ ν and μ ≪ ν, then μ.rnDeriv ν equals 1 almost everywhere with respect to ν if and only if μ = ν.

Русский

Если имеется разложение Лебега μ по ν и μ ≪ ν, то μ.rnDeriv ν = 1 почти по ν тогда же, когда μ = ν.

LaTeX

$$$$ μ.rnDeriv ν =^\mathrm{ae}_{ν} 1 \iff μ = ν $$$$

Lean4

theorem rnDeriv_eq_one_iff_eq [HaveLebesgueDecomposition μ ν] [SigmaFinite ν] (hμν : μ ≪ ν) :
    μ.rnDeriv ν =ᵐ[ν] 1 ↔ μ = ν := by
  refine ⟨fun h ↦ ?_, fun h ↦ h ▸ ν.rnDeriv_self⟩
  rw [← withDensity_rnDeriv_eq _ _ hμν, withDensity_congr_ae h, withDensity_one]

Похожие утверждения