absolutelyContinuous_iff_withDensity_rnDeriv_eq

English

For HaveLebesgueDecomposition μ ν, μ ≪ ν if and only if ν.withDensity (rnDeriv μ ν) = μ.

Русский

Для HaveLebesgueDecomposition μ ν верно: μ ≪ ν тогда и только тогда, когда ν.withDensity (rnDeriv μ ν) = μ.

LaTeX

$$$$ \\mu \\ll \\nu \\;\\;\\text{iff}\\;\\; \\nu.withDensity(\\mathrm{rnDeriv}(\\mu, \\nu)) = \\mu. $$$$

Lean4

/-- **The Radon-Nikodym theorem**: Given two measures `μ` and `ν`, if
`HaveLebesgueDecomposition μ ν`, then `μ` is absolutely continuous to `ν` if and only if
`ν.withDensity (rnDeriv μ ν) = μ`. -/
theorem absolutelyContinuous_iff_withDensity_rnDeriv_eq [HaveLebesgueDecomposition μ ν] :
    μ ≪ ν ↔ ν.withDensity (rnDeriv μ ν) = μ :=
  ⟨withDensity_rnDeriv_eq μ ν, fun h => h ▸ withDensity_absolutelyContinuous _ _⟩

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