singularPart_restrict — Mathlib

English

Restricting μ and ν to a measurable set s preserves the singular part: (μ.restrict s).singularPart ν = (μ.singularPart ν).restrict s.

Русский

Ограничение μ и ν до измеримого множества s сохраняет сингулярную часть: (μ.restrict s).singularPart ν = (μ.singularPart ν).restrict s.

LaTeX

$$$ (μ.restrict s).singularPart ν = (μ.singularPart ν).restrict s $$$

Lean4

theorem singularPart_restrict (μ ν : Measure α) [HaveLebesgueDecomposition μ ν] {s : Set α} (hs : MeasurableSet s) :
    (μ.restrict s).singularPart ν = (μ.singularPart ν).restrict s :=
  by
  refine (Measure.eq_singularPart (f := s.indicator (μ.rnDeriv ν)) ?_ ?_ ?_).symm
  · exact (μ.measurable_rnDeriv ν).indicator hs
  · exact (Measure.mutuallySingular_singularPart μ ν).restrict s
  · ext t
    rw [withDensity_indicator hs, ← restrict_withDensity hs, ← Measure.restrict_add, ←
      μ.haveLebesgueDecomposition_add ν]

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