integral_toReal_rnDeriv — Mathlib

English

Let μ and ν be σ-finite measures with μ absolutely continuous with respect to ν. Then the total mass of μ is recovered by integrating the real-valued Radon–Nikodym derivative of μ with respect to ν over the whole space.

Русский

Пусть μ и ν — конечные по мере μ σ–конечные, причем μ абсолютно непрерывна по ν. Тогда общая масса μ восстанавливается путем интегрирования вещественно-значного Radon–Nikodym производного μ по ν по всему пространству.

LaTeX

$$$$ \int x\, (\mu.rnDeriv \nu\; x)^{\mathrm{toReal}} \, d\nu = \mu.\mathrm{real}({\mathrm Set.univ}) $$$$

Lean4

theorem integral_toReal_rnDeriv [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) :
    ∫ x, (μ.rnDeriv ν x).toReal ∂ν = μ.real Set.univ := by
  rw [← setIntegral_univ, setIntegral_toReal_rnDeriv hμν Set.univ]

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