singularPart_eq_zero_of_ac — Mathlib

English

If μ is absolutely continuous with respect to ν, then the singular part of μ with respect to ν vanishes: μ.singularPart ν = 0.

Русский

Если μ абсолютно непрерывна относительно ν, то μ.singularPart ν = 0.

LaTeX

$$$$ μ \ll ν \Rightarrow μ.singularPart ν = 0 $$$$

Lean4

theorem singularPart_eq_zero_of_ac (h : μ ≪ ν) : μ.singularPart ν = 0 :=
  by
  rw [← MutuallySingular.self_iff]
  exact
    MutuallySingular.mono_ac (mutuallySingular_singularPart _ _) AbsolutelyContinuous.rfl
      ((absolutelyContinuous_of_le (singularPart_le _ _)).trans h)

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