setLIntegral_rnDeriv' — Mathlib

English

For HaveLebesgueDecomposition μ ν and μ ≪ ν, and s measurable, the ν-weighted real-valued integral over s matches μ.real(s).

Русский

ДляHaveLebesgueDecomposition μ ν и μ ≪ ν и множества s измеримо, интеграл по ν плотности μ.rnDeriv ν на s равен μ.real(s).

LaTeX

$$$\\int_{s} μ.rnDeriv ν(x) \\; dν(x) = μ.real(s)$$$

Lean4

theorem setLIntegral_rnDeriv' [HaveLebesgueDecomposition μ ν] (hμν : μ ≪ ν) {s : Set α} (hs : MeasurableSet s) :
    ∫⁻ x in s, μ.rnDeriv ν x ∂ν = μ s := by rw [← withDensity_apply _ hs, Measure.withDensity_rnDeriv_eq _ _ hμν]

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