rnDeriv_restrict_self — Mathlib

English

The RN derivative of the restricted ν.restrict s with respect to itself is s.indicator 1 almost everywhere: (ν.restrict s).rnDer ν =ᵐ[ν] s.indicator 1.

Русский

РДР производной ν.restrict s по ν равна s.indicator 1 почти всюду: (ν.restrict s).rnDer ν =ᵐ[ν] s.indicator 1.

LaTeX

$$$ (ν.restrict s).rnDer ν =ᵐ[ν] s.indicator 1 $$$

Lean4

/-- The Radon-Nikodym derivative of the restriction of a measure to a measurable set is the
indicator function of this set. -/
theorem rnDeriv_restrict_self (ν : Measure α) [SigmaFinite ν] {s : Set α} (hs : MeasurableSet s) :
    (ν.restrict s).rnDeriv ν =ᵐ[ν] s.indicator 1 :=
  by
  rw [← withDensity_indicator_one hs]
  exact rnDeriv_withDensity _ (measurable_one.indicator hs)

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