Theorems · Theorem · measure theory

MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eq

∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : MeasureTheory.SignedMeasure α)
  [s.HaveLebesgueDecomposition μ], s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) = s

The Lebesgue Decomposition theorem between a signed measure and a measure: Given a signed measure s and a σ-finite measure μ, there exist a signed measure t and a measurable and integrable function f, such that t is mutually singular with respect to μ and s = t + μ.withDensityᵥ f. In this case t = s.singularPart μ and f = s.rnDeriv μ.

Defined in

Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Cited by

6 results in Mathlib

Foundations

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

Assumes

MeasureTheory.SignedMeasure.HaveLebesgueDecomposition