singularPart_eq_restrict — Mathlib

English

If a set s separates the ν-absolutely continuous part from the ν-singular part, then μ.singularPart ν = μ.restrict s.

Русский

Если множество s разделяет абсолютно непрерывную часть ν от сингулярной части ν, то μ.singularPart ν = μ.restrict s.

LaTeX

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

Lean4

/-- If a set `s` separates `ν` from the singular part of `μ` with respect to `ν`,
then the singular part equals the restriction of `μ` to `s`. -/
theorem singularPart_eq_restrict {s : Set α} [μ.HaveLebesgueDecomposition ν] (hμs : μ.singularPart ν sᶜ = 0)
    (hνs : ν s = 0) : μ.singularPart ν = μ.restrict s :=
  singularPart_eq_restrict' hμs <| withDensity_absolutelyContinuous _ _ hνs

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