Theorems · Theorem · measure theory

MeasureTheory.SignedMeasure.eq_singularPart

∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : MeasureTheory.SignedMeasure α}
  (t : MeasureTheory.SignedMeasure α) (f : α → ℝ),
  MeasureTheory.VectorMeasure.MutuallySingular t μ.toENNRealVectorMeasure →
    s = t + μ.withDensityᵥ f → t = s.singularPart μ

Given a measure μ, signed measures s and t, and a function f such that t is mutually singular with respect to μ and s = t + μ.withDensityᵥ f, we have t = singularPart s μ, i.e. t is the singular part of the Lebesgue decomposition between s and μ.

Defined in

Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Cited by

3 results in Mathlib

Foundations

Depth 264 from the axioms · uses propext, Classical.choice, Quot.sound