The Radon–Nikodym derivative on null sets and at atoms

On a μ-null set s, the Radon–Nikodym derivative μ.rnDeriv ν vanishes ν-almost everywhere (MeasureTheory.Measure.ae_rnDeriv_eq_zero_of_measure_eq_zero): its integral over a measurable hull of s is at most μ s = 0.

The Radon–Nikodym derivative μ.rnDeriv ν is a fixed representative of an almost-everywhere defined density, so in general its value at a single point carries no information. At a point x with measurable singleton and ν {x} ≠ 0, it does: the singular part of μ with respect to ν cannot charge {x}, and so μ.rnDeriv ν x * ν {x} = μ {x}. On a countable space with measurable singletons every point of positive ν-mass is such an atom, and the derivative is the ratio of the masses there.

theorem MeasureTheory.Measure.ae_rnDeriv_eq_zero_of_measure_eq_zero {α : Type u_1} [MeasurableSpace α] {μ ν : Measure α} {s : Set α} (hs : μ s = 0) : ∀ᵐ (x : α) ∂ν, x ∈ s → μ.rnDeriv ν x = 0

The Radon–Nikodym derivative of μ with respect to ν vanishes ν-almost everywhere on a μ-null set.

theorem MeasureTheory.Measure.toENNReal_mul_measure_eq_setLIntegral_ofReal_mul_rnDeriv {α : Type u_1} [MeasurableSpace α] {μ ν : Measure α} [SigmaFinite μ] [μ.HaveLebesgueDecomposition ν] (hμ : μ.AbsolutelyContinuous ν) {Z : Set α} (hZ : MeasurableSet Z) {c : EReal} {L : ℝ} (hL : c = ↑L ∨ μ Z = 0) (ε : ℝ) : (↑ε * c).toENNReal * μ Z = ∫⁻ (x : α) in Z, ENNReal.ofReal (ε * (L * (μ.rnDeriv ν x).toReal)) ∂ν

For μ ≪ ν with μ σ-finite, a measurable set Z and a real L which is the extended real c unless μ Z = 0, the term (ε c)⁺ μ(Z) is the integral over Z of the positive part of ε L dμ/dν.

theorem MeasureTheory.Measure.rnDeriv_mul_measure_singleton {α : Type u_1} [MeasurableSpace α] {μ ν : Measure α} [MeasurableSingletonClass α] {x : α} [μ.HaveLebesgueDecomposition ν] (hx : ν {x} ≠ 0) : μ.rnDeriv ν x * ν {x} = μ {x}

At an atom x of ν, the Radon–Nikodym derivative of μ with respect to ν, weighted by the mass of the atom, is the μ-mass of x: the singular part of μ does not charge {x}.

theorem MeasureTheory.Measure.rnDeriv_eq_measure_singleton_div {α : Type u_1} [MeasurableSpace α] {μ ν : Measure α} [MeasurableSingletonClass α] {x : α} [μ.HaveLebesgueDecomposition ν] (hx : ν {x} ≠ 0) (hx' : ν {x} ≠ ⊤) : μ.rnDeriv ν x = μ {x} / ν {x}

At an atom x of finite positive ν-mass, the Radon–Nikodym derivative of μ with respect to ν is the ratio μ {x} / ν {x} of the masses.