Theorems · Definition · measure theory

MeasureTheory.SignedMeasure.singularPart

{α : Type u_1} →
  {m : MeasurableSpace α} → MeasureTheory.SignedMeasure α → MeasureTheory.Measure α → MeasureTheory.SignedMeasure α

Given a signed measure s and a measure μ, s.singularPart μ is the signed measure such that s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) = s and s.singularPart μ is mutually singular with respect to μ.

Defined in

Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Cited by

13 results in Mathlib

Foundations

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