Theorems · Definition · measure theory

MeasureTheory.SignedMeasure.rnDeriv

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

The Radon-Nikodym derivative between a signed measure and a positive measure. rnDeriv s μ satisfies μ.withDensityᵥ (s.rnDeriv μ) = s if and only if s is absolutely continuous with respect to μ and this fact is known as MeasureTheory.SignedMeasure.absolutelyContinuous_iff_withDensity_rnDeriv_eq and can be found in Mathlib/MeasureTheory/Measure/Decomposition/RadonNikodym.lean.

Defined in

Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Cited by

13 results in Mathlib

Foundations

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