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 theoremMeasureTheory.SignedMeasure.absolutelyContinuous_iff_withDensityᵥ_rnDeriv_eq: the Radon-Nikodym theorem for signed measures
The file also contains properties of rnDeriv that use the Radon-Nikodym theorem, notably
MeasureTheory.Measure.rnDeriv_withDensity_left: the Radon-Nikodym derivative ofμ.withDensity fwith respect toνisf * μ.rnDeriv ν.MeasureTheory.Measure.rnDeriv_withDensity_right: the Radon-Nikodym derivative ofμwith respect toν.withDensity fisf⁻¹ * μ.rnDeriv ν.MeasureTheory.Measure.inv_rnDeriv:(μ.rnDeriv ν)⁻¹ =ᵐ[μ] ν.rnDeriv μ.MeasureTheory.Measure.set_lintegral_rnDeriv:∫⁻ x in s, μ.rnDeriv ν x ∂ν = μ sifμ ≪ ν. There is also a version of this result for the Bochner integral.
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 μ ν)
:
theorem
MeasureTheory.Measure.absolutelyContinuous_iff_withDensity_rnDeriv_eq
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.Measure.HaveLebesgueDecomposition μ ν]
:
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 α}
[MeasureTheory.Measure.HaveLebesgueDecomposition μ ν]
(hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν)
:
∀ᵐ (x : α) ∂μ, 0 < MeasureTheory.Measure.rnDeriv μ ν x
theorem
MeasureTheory.Measure.rnDeriv_pos'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
(hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν)
:
∀ᵐ (x : α) ∂μ, 0 < MeasureTheory.Measure.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 ≠ ⊤)
:
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 ≠ ⊤)
:
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μν : MeasureTheory.Measure.AbsolutelyContinuous μ ν)
(hf : AEMeasurable f ν)
:
MeasureTheory.Measure.rnDeriv (MeasureTheory.Measure.withDensity μ f) ν =ᶠ[MeasureTheory.Measure.ae ν] fun (x : α) =>
f x * MeasureTheory.Measure.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 ≠ ⊤)
:
MeasureTheory.Measure.rnDeriv (MeasureTheory.Measure.withDensity μ f) ν =ᶠ[MeasureTheory.Measure.ae ν] fun (x : α) =>
f x * MeasureTheory.Measure.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μν : MeasureTheory.Measure.AbsolutelyContinuous μ ν)
(hf : AEMeasurable f ν)
(hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0)
(hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ⊤)
:
MeasureTheory.Measure.rnDeriv μ (MeasureTheory.Measure.withDensity ν f) =ᶠ[MeasureTheory.Measure.ae ν] fun (x : α) =>
(f x)⁻¹ * MeasureTheory.Measure.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 ≠ ⊤)
:
MeasureTheory.Measure.rnDeriv μ (MeasureTheory.Measure.withDensity ν f) =ᶠ[MeasureTheory.Measure.ae ν] fun (x : α) =>
(f x)⁻¹ * MeasureTheory.Measure.rnDeriv μ ν x
theorem
MeasureTheory.Measure.rnDeriv_restrict
{α : Type u_1}
{m : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
{s : Set α}
(hs : MeasurableSet s)
:
theorem
MeasureTheory.Measure.rnDeriv_eq_zero_of_mutuallySingular
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
{ν' : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite ν']
(h : MeasureTheory.Measure.MutuallySingular μ ν)
(hνν' : MeasureTheory.Measure.AbsolutelyContinuous ν ν')
:
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μν : MeasureTheory.Measure.AbsolutelyContinuous μ ν)
(hνν' : MeasureTheory.Measure.MutuallySingular ν ν')
:
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μν' : MeasureTheory.Measure.MutuallySingular μ ν')
(hνν' : MeasureTheory.Measure.MutuallySingular ν ν')
:
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νν' : MeasureTheory.Measure.MutuallySingular ν ν')
:
theorem
MeasureTheory.Measure.rnDeriv_withDensity_rnDeriv
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
(hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν)
:
theorem
MeasureTheory.Measure.inv_rnDeriv_aux
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
(hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν)
(hνμ : MeasureTheory.Measure.AbsolutelyContinuous ν μ)
:
Auxiliary lemma for inv_rnDeriv.
theorem
MeasureTheory.Measure.inv_rnDeriv
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
(hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν)
:
theorem
MeasureTheory.Measure.inv_rnDeriv'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
(hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν)
:
theorem
MeasureTheory.Measure.set_lintegral_rnDeriv_le
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(s : Set α)
:
∫⁻ (x : α) in s, MeasureTheory.Measure.rnDeriv μ ν x ∂ν ≤ ↑↑μ s
theorem
MeasureTheory.Measure.set_lintegral_rnDeriv'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.Measure.HaveLebesgueDecomposition μ ν]
(hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν)
{s : Set α}
(hs : MeasurableSet s)
:
∫⁻ (x : α) in s, MeasureTheory.Measure.rnDeriv μ ν x ∂ν = ↑↑μ s
theorem
MeasureTheory.Measure.set_lintegral_rnDeriv
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.Measure.HaveLebesgueDecomposition μ ν]
[MeasureTheory.SFinite ν]
(hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν)
(s : Set α)
:
∫⁻ (x : α) in s, MeasureTheory.Measure.rnDeriv μ ν x ∂ν = ↑↑μ s
theorem
MeasureTheory.Measure.lintegral_rnDeriv
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.Measure.HaveLebesgueDecomposition μ ν]
(hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν)
:
∫⁻ (x : α), MeasureTheory.Measure.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 : α) => (MeasureTheory.Measure.rnDeriv μ ν x).toReal) s ν
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, (MeasureTheory.Measure.rnDeriv μ ν x).toReal ∂ν = (↑↑(MeasureTheory.Measure.withDensity ν (MeasureTheory.Measure.rnDeriv μ ν)) s).toReal
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, (MeasureTheory.Measure.rnDeriv μ ν x).toReal ∂ν = (↑↑(MeasureTheory.Measure.withDensity ν (MeasureTheory.Measure.rnDeriv μ ν)) s).toReal
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, (MeasureTheory.Measure.rnDeriv μ ν x).toReal ∂ν ≤ (↑↑μ s).toReal
theorem
MeasureTheory.Measure.set_integral_toReal_rnDeriv'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.Measure.HaveLebesgueDecomposition μ ν]
(hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν)
{s : Set α}
(hs : MeasurableSet s)
:
∫ (x : α) in s, (MeasureTheory.Measure.rnDeriv μ ν x).toReal ∂ν = (↑↑μ s).toReal
theorem
MeasureTheory.Measure.set_integral_toReal_rnDeriv
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
(hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν)
(s : Set α)
:
∫ (x : α) in s, (MeasureTheory.Measure.rnDeriv μ ν x).toReal ∂ν = (↑↑μ s).toReal
theorem
MeasureTheory.Measure.integral_toReal_rnDeriv
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
(hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν)
:
∫ (x : α), (MeasureTheory.Measure.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μν : MeasureTheory.Measure.AbsolutelyContinuous μ ν)
:
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 μ))
:
theorem
MeasureTheory.SignedMeasure.absolutelyContinuous_iff_withDensityᵥ_rnDeriv_eq
{α : Type u_1}
{m : MeasurableSpace α}
(s : MeasureTheory.SignedMeasure α)
(μ : MeasureTheory.Measure α)
[MeasureTheory.SigmaFinite μ]
:
The Radon-Nikodym theorem for signed measures.
theorem
MeasureTheory.lintegral_rnDeriv_mul
{α : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.Measure.HaveLebesgueDecomposition μ ν]
(hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν)
{f : α → ENNReal}
(hf : AEMeasurable f ν)
:
∫⁻ (x : α), MeasureTheory.Measure.rnDeriv μ ν x * f x ∂ν = ∫⁻ (x : α), f x ∂μ
theorem
MeasureTheory.set_lintegral_rnDeriv_mul
{α : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.Measure.HaveLebesgueDecomposition μ ν]
(hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν)
{f : α → ENNReal}
(hf : AEMeasurable f ν)
{s : Set α}
(hs : MeasurableSet s)
:
∫⁻ (x : α) in s, MeasureTheory.Measure.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]
[MeasureTheory.Measure.HaveLebesgueDecomposition μ ν]
(hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν)
[MeasureTheory.SigmaFinite μ]
{f : α → E}
:
MeasureTheory.Integrable (fun (x : α) => (MeasureTheory.Measure.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]
[MeasureTheory.Measure.HaveLebesgueDecomposition μ ν]
(hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν)
[MeasureTheory.SigmaFinite μ]
{f : α → E}
(hf : MeasureTheory.Integrable f μ)
:
(MeasureTheory.Measure.withDensityᵥ ν fun (x : α) => (MeasureTheory.Measure.rnDeriv μ ν x).toReal • f x) = MeasureTheory.Measure.withDensityᵥ μ f
theorem
MeasureTheory.integral_rnDeriv_smul
{α : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasureTheory.Measure.HaveLebesgueDecomposition μ ν]
(hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν)
[MeasureTheory.SigmaFinite μ]
{f : α → E}
:
∫ (x : α), (MeasureTheory.Measure.rnDeriv μ ν x).toReal • f x ∂ν = ∫ (x : α), f x ∂μ