singularPart_withDensity — Mathlib

English

The singular part of a density-modified measure vanishes: (ν.withDensity f).singularPart ν = 0 for any f ≥ 0.

Русский

Сингулярная часть меры после модификации плотностью исчезает: (ν.withDensity f).singularPart ν = 0 для любой f ≥ 0.

LaTeX

$$$$ (ν.withDensity f).singularPart ν = 0 $$$$

Lean4

@[simp]
theorem singularPart_withDensity (ν : Measure α) (f : α → ℝ≥0∞) : (ν.withDensity f).singularPart ν = 0 :=
  singularPart_eq_zero_of_ac (withDensity_absolutelyContinuous _ _)

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