Radon-Nikodym theorem

This file proves the Radon-Nikodym theorem. The Radon-Nikodym theorem states that, given measures μ, ν, if HaveLebesgueDecomposition μ ν, then μ is absolutely continuous with respect to ν if and only if there exists a measurable function f : α → ℝ≥0∞ such that μ = fν. In particular, we have f = rnDeriv μ ν.

The Radon-Nikodym theorem will allow us to define many important concepts in probability theory, most notably probability cumulative functions. It could also be used to define the conditional expectation of a real function, but we take a different approach (see the file MeasureTheory/Function/ConditionalExpectation).

Main results

• MeasureTheory.Measure.absolutelyContinuous_iff_withDensity_rnDeriv_eq : the Radon-Nikodym theorem
• MeasureTheory.SignedMeasure.absolutelyContinuous_iff_withDensityᵥ_rnDeriv_eq : the Radon-Nikodym theorem for signed measures

Tags

Radon-Nikodym theorem

theorem MeasureTheory.Measure.withDensity_rnDeriv_eq {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.Measure.HaveLebesgueDecomposition μ ν] (h : MeasureTheory.Measure.AbsolutelyContinuous μ ν) : MeasureTheory.Measure.withDensity ν (MeasureTheory.Measure.rnDeriv μ ν) = μ

theorem MeasureTheory.Measure.absolutelyContinuous_iff_withDensity_rnDeriv_eq {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.Measure.HaveLebesgueDecomposition μ ν] : MeasureTheory.Measure.AbsolutelyContinuous μ ν ↔ MeasureTheory.Measure.withDensity ν (MeasureTheory.Measure.rnDeriv μ ν) = μ

The Radon-Nikodym theorem: Given two measures μ and ν, if HaveLebesgueDecomposition μ ν, then μ is absolutely continuous to ν if and only if ν.withDensity (rnDeriv μ ν) = μ.

theorem MeasureTheory.Measure.withDensity_rnDeriv_toReal_eq {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.Measure.HaveLebesgueDecomposition μ ν] (h : MeasureTheory.Measure.AbsolutelyContinuous μ ν) {i : Set α} (hi : MeasurableSet i) : ∫ (x : α) in i, ENNReal.toReal (MeasureTheory.Measure.rnDeriv μ ν x) ∂ν = ENNReal.toReal (↑↑μ i)

theorem MeasureTheory.SignedMeasure.withDensityᵥ_rnDeriv_eq {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (h : MeasureTheory.VectorMeasure.AbsolutelyContinuous s (MeasureTheory.Measure.toENNRealVectorMeasure μ)) : MeasureTheory.Measure.withDensityᵥ μ (MeasureTheory.SignedMeasure.rnDeriv s μ) = s

theorem MeasureTheory.SignedMeasure.absolutelyContinuous_iff_withDensityᵥ_rnDeriv_eq {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : MeasureTheory.VectorMeasure.AbsolutelyContinuous s (MeasureTheory.Measure.toENNRealVectorMeasure μ) ↔ MeasureTheory.Measure.withDensityᵥ μ (MeasureTheory.SignedMeasure.rnDeriv s μ) = s

The Radon-Nikodym theorem for signed measures.