singularPart — Mathlib

English

For a complex measure c and μ, the singular part of c plus μ with density equals c, i.e., the Lebesgue decomposition recovers c from its singular part and RN-density components.

Русский

Для комплексной меры c и μ разложение Лебега восстанавливает c через сингулярную часть и плотность RN.

LaTeX

$$$ c.singularPart \\mu + μ.withDensityᵥ (c.rnDeriv \\mu) = c $$$

Lean4

/-- The singular part between a complex measure `c` and a positive measure `μ` is the complex
measure satisfying `c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ) = c`. This property is given
by `MeasureTheory.ComplexMeasure.singularPart_add_withDensity_rnDeriv_eq`. -/
def singularPart (c : ComplexMeasure α) (μ : Measure α) : ComplexMeasure α :=
  (c.re.singularPart μ).toComplexMeasure (c.im.singularPart μ)

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