Theorems · Theorem · measure theory

MeasureTheory.SignedMeasure.eq_rnDeriv

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

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 f = rnDeriv s μ, i.e. f is the Radon-Nikodym derivative of s and μ.

Defined in

Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Cited by

0 results in Mathlib

Foundations

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