setIntegral_toReal_rnDeriv — Mathlib

English

For any set s, the ν-integral of μ.rnDeriv ν over s is bounded above by μ(s).

Русский

Для любого множества s ν-интеграл μ.rnDeriv ν по s не превосходит μ(s).

LaTeX

$$$\\int_{s} μ.rnDeriv ν(x) \\, dν(x) \\le μ(s)$$$

Lean4

theorem setIntegral_toReal_rnDeriv [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) (s : Set α) :
    ∫ x in s, (μ.rnDeriv ν x).toReal ∂ν = μ.real s := by
  rw [setIntegral_toReal_rnDeriv_eq_withDensity s, Measure.withDensity_rnDeriv_eq _ _ hμν]

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