singularPart_add_rnDeriv — Mathlib

English

The sum of ν.withDensity(μ.rnDeriv ν) and μ.singularPart ν equals μ.

Русский

Сумма ν.withDensity(μ.rnDeriv ν) и μ.singularPart ν равна μ.

LaTeX

$$ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν = μ$$

Lean4

/-- For the versions of this lemma where `ν.withDensity (μ.rnDeriv ν)` or `μ.singularPart ν` are
isolated, see `MeasureTheory.Measure.measure_sub_singularPart` and
`MeasureTheory.Measure.measure_sub_rnDeriv`. -/
theorem singularPart_add_rnDeriv (μ ν : Measure α) [HaveLebesgueDecomposition μ ν] :
    μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = μ :=
  (haveLebesgueDecomposition_add μ ν).symm

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