Documentation

Mathlib.MeasureTheory.Decomposition.RadonNikodym

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 #

The file also contains properties of rnDeriv that use the Radon-Nikodym theorem, notably

Tags #

Radon-Nikodym theorem

theorem MeasureTheory.Measure.withDensity_rnDeriv_eq {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [μ.HaveLebesgueDecomposition ν] (h : μ.AbsolutelyContinuous ν) :
ν.withDensity (μ.rnDeriv ν) = μ
theorem MeasureTheory.Measure.absolutelyContinuous_iff_withDensity_rnDeriv_eq {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν] :
μ.AbsolutelyContinuous ν ν.withDensity (μ.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.rnDeriv_pos {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) :
∀ᵐ (x : α) ∂μ, 0 < μ.rnDeriv ν x
theorem MeasureTheory.Measure.rnDeriv_pos' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) :
∀ᵐ (x : α) ∂μ, 0 < ν.rnDeriv μ x
theorem MeasureTheory.Measure.rnDeriv_withDensity_withDensity_rnDeriv_left {α : Type u_1} {m : MeasurableSpace α} {f : αENNReal} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hf : AEMeasurable f μ) (hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ) :
((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᵐ[ν] (μ.withDensity f).rnDeriv ν

Auxiliary lemma for rnDeriv_withDensity_left.

theorem MeasureTheory.Measure.rnDeriv_withDensity_withDensity_rnDeriv_right {α : Type u_1} {m : MeasurableSpace α} {f : αENNReal} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hf : AEMeasurable f ν) (hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x 0) (hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ) :
(ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᵐ[ν] μ.rnDeriv (ν.withDensity f)

Auxiliary lemma for rnDeriv_withDensity_right.

theorem MeasureTheory.Measure.rnDeriv_withDensity_left_of_absolutelyContinuous {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) (hf : AEMeasurable f ν) :
(μ.withDensity f).rnDeriv ν =ᵐ[ν] fun (x : α) => f x * μ.rnDeriv ν x
theorem MeasureTheory.Measure.rnDeriv_withDensity_left {α : Type u_1} {m : MeasurableSpace α} {f : αENNReal} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hfμ : AEMeasurable f μ) (hfν : AEMeasurable f ν) (hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ) :
(μ.withDensity f).rnDeriv ν =ᵐ[ν] fun (x : α) => f x * μ.rnDeriv ν x
theorem MeasureTheory.Measure.rnDeriv_withDensity_right_of_absolutelyContinuous {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) (hf : AEMeasurable f ν) (hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x 0) (hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ) :
μ.rnDeriv (ν.withDensity f) =ᵐ[ν] fun (x : α) => (f x)⁻¹ * μ.rnDeriv ν x

Auxiliary lemma for rnDeriv_withDensity_right.

theorem MeasureTheory.Measure.rnDeriv_withDensity_right {α : Type u_1} {m : MeasurableSpace α} {f : αENNReal} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hf : AEMeasurable f ν) (hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x 0) (hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ) :
μ.rnDeriv (ν.withDensity f) =ᵐ[ν] fun (x : α) => (f x)⁻¹ * μ.rnDeriv ν x
theorem MeasureTheory.Measure.rnDeriv_eq_zero_of_mutuallySingular {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {ν' : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite ν'] (h : μ.MutuallySingular ν) (hνν' : ν.AbsolutelyContinuous ν') :
μ.rnDeriv ν' =ᵐ[ν] 0
theorem MeasureTheory.Measure.rnDeriv_add_right_of_absolutelyContinuous_of_mutuallySingular {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {ν' : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] [MeasureTheory.SigmaFinite ν'] (hμν : μ.AbsolutelyContinuous ν) (hνν' : ν.MutuallySingular ν') :
μ.rnDeriv (ν + ν') =ᵐ[ν] μ.rnDeriv ν

Auxiliary lemma for rnDeriv_add_right_of_mutuallySingular.

theorem MeasureTheory.Measure.rnDeriv_add_right_of_mutuallySingular' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {ν' : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] [MeasureTheory.SigmaFinite ν'] (hμν' : μ.MutuallySingular ν') (hνν' : ν.MutuallySingular ν') :
μ.rnDeriv (ν + ν') =ᵐ[ν] μ.rnDeriv ν

Auxiliary lemma for rnDeriv_add_right_of_mutuallySingular.

theorem MeasureTheory.Measure.rnDeriv_add_right_of_mutuallySingular {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {ν' : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] [MeasureTheory.SigmaFinite ν'] (hνν' : ν.MutuallySingular ν') :
μ.rnDeriv (ν + ν') =ᵐ[ν] μ.rnDeriv ν
theorem MeasureTheory.Measure.rnDeriv_withDensity_rnDeriv {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) :
μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᵐ[μ] μ.rnDeriv ν
theorem MeasureTheory.Measure.inv_rnDeriv_aux {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) (hνμ : ν.AbsolutelyContinuous μ) :
(μ.rnDeriv ν)⁻¹ =ᵐ[μ] ν.rnDeriv μ

Auxiliary lemma for inv_rnDeriv.

theorem MeasureTheory.Measure.inv_rnDeriv {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) :
(μ.rnDeriv ν)⁻¹ =ᵐ[μ] ν.rnDeriv μ
theorem MeasureTheory.Measure.inv_rnDeriv' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) :
(ν.rnDeriv μ)⁻¹ =ᵐ[μ] μ.rnDeriv ν
theorem MeasureTheory.Measure.set_lintegral_rnDeriv_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (s : Set α) :
∫⁻ (x : α) in s, μ.rnDeriv ν xν μ s
theorem MeasureTheory.Measure.set_lintegral_rnDeriv' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) {s : Set α} (hs : MeasurableSet s) :
∫⁻ (x : α) in s, μ.rnDeriv ν xν = μ s
theorem MeasureTheory.Measure.set_lintegral_rnDeriv {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν] [MeasureTheory.SFinite ν] (hμν : μ.AbsolutelyContinuous ν) (s : Set α) :
∫⁻ (x : α) in s, μ.rnDeriv ν xν = μ s
theorem MeasureTheory.Measure.lintegral_rnDeriv {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) :
∫⁻ (x : α), μ.rnDeriv ν xν = μ Set.univ
theorem MeasureTheory.Measure.integrableOn_toReal_rnDeriv {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {s : Set α} (hμs : μ s ) :
MeasureTheory.IntegrableOn (fun (x : α) => (μ.rnDeriv ν x).toReal) s ν
theorem MeasureTheory.Measure.setIntegral_toReal_rnDeriv_eq_withDensity' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {s : Set α} (hs : MeasurableSet s) :
∫ (x : α) in s, (μ.rnDeriv ν x).toRealν = ((ν.withDensity (μ.rnDeriv ν)) s).toReal
@[deprecated MeasureTheory.Measure.setIntegral_toReal_rnDeriv_eq_withDensity']
theorem MeasureTheory.Measure.set_integral_toReal_rnDeriv_eq_withDensity' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {s : Set α} (hs : MeasurableSet s) :
∫ (x : α) in s, (μ.rnDeriv ν x).toRealν = ((ν.withDensity (μ.rnDeriv ν)) s).toReal

Alias of MeasureTheory.Measure.setIntegral_toReal_rnDeriv_eq_withDensity'.

theorem MeasureTheory.Measure.setIntegral_toReal_rnDeriv_eq_withDensity {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SFinite ν] (s : Set α) :
∫ (x : α) in s, (μ.rnDeriv ν x).toRealν = ((ν.withDensity (μ.rnDeriv ν)) s).toReal
@[deprecated MeasureTheory.Measure.setIntegral_toReal_rnDeriv_eq_withDensity]
theorem MeasureTheory.Measure.set_integral_toReal_rnDeriv_eq_withDensity {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SFinite ν] (s : Set α) :
∫ (x : α) in s, (μ.rnDeriv ν x).toRealν = ((ν.withDensity (μ.rnDeriv ν)) s).toReal

Alias of MeasureTheory.Measure.setIntegral_toReal_rnDeriv_eq_withDensity.

theorem MeasureTheory.Measure.setIntegral_toReal_rnDeriv_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {s : Set α} (hμs : μ s ) :
∫ (x : α) in s, (μ.rnDeriv ν x).toRealν (μ s).toReal
@[deprecated MeasureTheory.Measure.setIntegral_toReal_rnDeriv_le]
theorem MeasureTheory.Measure.set_integral_toReal_rnDeriv_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {s : Set α} (hμs : μ s ) :
∫ (x : α) in s, (μ.rnDeriv ν x).toRealν (μ s).toReal

Alias of MeasureTheory.Measure.setIntegral_toReal_rnDeriv_le.

theorem MeasureTheory.Measure.setIntegral_toReal_rnDeriv' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) {s : Set α} (hs : MeasurableSet s) :
∫ (x : α) in s, (μ.rnDeriv ν x).toRealν = (μ s).toReal
@[deprecated MeasureTheory.Measure.setIntegral_toReal_rnDeriv']
theorem MeasureTheory.Measure.set_integral_toReal_rnDeriv' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) {s : Set α} (hs : MeasurableSet s) :
∫ (x : α) in s, (μ.rnDeriv ν x).toRealν = (μ s).toReal

Alias of MeasureTheory.Measure.setIntegral_toReal_rnDeriv'.

theorem MeasureTheory.Measure.setIntegral_toReal_rnDeriv {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) (s : Set α) :
∫ (x : α) in s, (μ.rnDeriv ν x).toRealν = (μ s).toReal
@[deprecated MeasureTheory.Measure.setIntegral_toReal_rnDeriv]
theorem MeasureTheory.Measure.set_integral_toReal_rnDeriv {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) (s : Set α) :
∫ (x : α) in s, (μ.rnDeriv ν x).toRealν = (μ s).toReal

Alias of MeasureTheory.Measure.setIntegral_toReal_rnDeriv.

theorem MeasureTheory.Measure.integral_toReal_rnDeriv {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) :
∫ (x : α), (μ.rnDeriv ν x).toRealν = (μ Set.univ).toReal
theorem MeasureTheory.Measure.rnDeriv_mul_rnDeriv {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {κ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] [MeasureTheory.SigmaFinite κ] (hμν : μ.AbsolutelyContinuous ν) :
μ.rnDeriv ν * ν.rnDeriv κ =ᵐ[κ] μ.rnDeriv κ
theorem MeasurableEmbedding.rnDeriv_map_aux {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {mβ : MeasurableSpace β} {f : αβ} (hf : MeasurableEmbedding f) (hμν : μ.AbsolutelyContinuous ν) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] :
(fun (x : α) => (MeasureTheory.Measure.map f μ).rnDeriv (MeasureTheory.Measure.map f ν) (f x)) =ᵐ[ν] μ.rnDeriv ν
theorem MeasurableEmbedding.rnDeriv_map {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : αβ} (hf : MeasurableEmbedding f) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] :
(fun (x : α) => (MeasureTheory.Measure.map f μ).rnDeriv (MeasureTheory.Measure.map f ν) (f x)) =ᵐ[ν] μ.rnDeriv ν

The Radon-Nikodym theorem for signed measures.

theorem MeasureTheory.lintegral_rnDeriv_mul {α : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) {f : αENNReal} (hf : AEMeasurable f ν) :
∫⁻ (x : α), μ.rnDeriv ν x * f xν = ∫⁻ (x : α), f xμ
theorem MeasureTheory.set_lintegral_rnDeriv_mul {α : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) {f : αENNReal} (hf : AEMeasurable f ν) {s : Set α} (hs : MeasurableSet s) :
∫⁻ (x : α) in s, μ.rnDeriv ν x * f xν = ∫⁻ (x : α) in s, f xμ
theorem MeasureTheory.integrable_rnDeriv_smul_iff {α : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace E] [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) [MeasureTheory.SigmaFinite μ] {f : αE} :
MeasureTheory.Integrable (fun (x : α) => (μ.rnDeriv ν x).toReal f x) ν MeasureTheory.Integrable f μ
theorem MeasureTheory.withDensityᵥ_rnDeriv_smul {α : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace E] [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) [MeasureTheory.SigmaFinite μ] {f : αE} (hf : MeasureTheory.Integrable f μ) :
(ν.withDensityᵥ fun (x : α) => (μ.rnDeriv ν x).toReal f x) = μ.withDensityᵥ f
theorem MeasureTheory.integral_rnDeriv_smul {α : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace E] [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) [MeasureTheory.SigmaFinite μ] {f : αE} :
∫ (x : α), (μ.rnDeriv ν x).toReal f xν = ∫ (x : α), f xμ