rnDeriv_restrict — Mathlib

English

The RN derivative of the restricted μ.restrict s with respect to ν equals s.indicator (μ.rnDer ν) almost everywhere.

Русский

РДР производной ограниченной меры μ.restrict s по ν равна s.indicator (μ.rnDer ν) почти везде по ν.

LaTeX

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

Lean4

theorem rnDeriv_restrict (μ ν : Measure α) [HaveLebesgueDecomposition μ ν] [SigmaFinite ν] {s : Set α}
    (hs : MeasurableSet s) : (μ.restrict s).rnDeriv ν =ᵐ[ν] s.indicator (μ.rnDeriv ν) :=
  by
  refine
    (eq_rnDeriv (s := (μ.restrict s).singularPart ν) ((measurable_rnDeriv _ _).indicator hs)
        (mutuallySingular_singularPart _ _) ?_).symm
  rw [singularPart_restrict _ _ hs, withDensity_indicator hs, ← restrict_withDensity hs, ← Measure.restrict_add, ←
    μ.haveLebesgueDecomposition_add ν]

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