theorem radon_nikodym_withDensity {Ω : Type u_1} {𝓕 : MeasurableSpace Ω} (μ ν : MeasureTheory.Measure Ω) [ν.HaveLebesgueDecomposition μ] (hac : ν.AbsolutelyContinuous μ) : μ.withDensity (ν.rnDeriv μ) = ν

Radon–Nikodym theorem (density form). If ν ≪ μ (with ν having a Lebesgue decomposition w.r.t. μ), then ν is the measure with density dν/dμ w.r.t. μ, i.e. μ.withDensity (ν.rnDeriv μ) = ν.

theorem radon_nikodym_setLIntegral' {Ω : Type u_1} {𝓕 : MeasurableSpace Ω} (μ ν : MeasureTheory.Measure Ω) [ν.HaveLebesgueDecomposition μ] [MeasureTheory.SFinite μ] (hac : ν.AbsolutelyContinuous μ) (A : Set Ω) : ∫⁻ (x : Ω) in A, ν.rnDeriv μ x ∂μ = ν A

Radon–Nikodym theorem (integral form). If ν ≪ μ then for every measurable set A, ν(A) = ∫_A (dν/dμ) dμ, expressing ν as integration of its Radon–Nikodym derivative against μ.