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 \\text{ if } hμs \\text{ and } hνs$ (precise hypotheses omitted here for brevity)$$

Lean4

/-- If a set `s` separates the absolutely continuous part of `μ` with respect to `ν`
from the singular part, then the singular part equals the restriction of `μ` to `s`. -/
theorem singularPart_eq_restrict' {s : Set α} [μ.HaveLebesgueDecomposition ν] (hμs : μ.singularPart ν sᶜ = 0)
    (hνs : ν.withDensity (μ.rnDeriv ν) s = 0) : μ.singularPart ν = μ.restrict s :=
  by
  conv_rhs => rw [← singularPart_add_rnDeriv μ ν]
  rwa [restrict_add, restrict_eq_self_of_ae_mem, restrict_eq_zero.2 hνs, add_zero]

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