withDensity_rnDeriv_eq — Mathlib

English

If μ ≪ ν and μ has a Lebesgue decomposition w.r.t. ν, then ν.withDensity (rnDeriv μ ν) = μ.

Русский

Если μ абсолютно непрерывна по ν и имеет разложение Лебеса, то ν.withDensity (rnDeriv μ ν) = μ.

LaTeX

$$$$ \\nu.withDensity(\\mathrm{rnDeriv}(\\mu, \\nu)) = \\mu. $$$$

Lean4

theorem withDensity_rnDeriv_eq (μ ν : Measure α) [HaveLebesgueDecomposition μ ν] (h : μ ≪ ν) :
    ν.withDensity (rnDeriv μ ν) = μ :=
  by
  suffices μ.singularPart ν = 0 by conv_rhs => rw [haveLebesgueDecomposition_add μ ν, this, zero_add]
  exact (singularPart_eq_zero μ ν).mpr h

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