# Documentation

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

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 f with respect to ν is f * μ.rnDeriv ν.
• MeasureTheory.Measure.rnDeriv_withDensity_right: the Radon-Nikodym derivative of μ with respect to ν.withDensity f is f⁻¹ * μ.rnDeriv ν.
• MeasureTheory.Measure.inv_rnDeriv: (μ.rnDeriv ν)⁻¹ =ᵐ[μ] ν.rnDeriv μ.
• MeasureTheory.Measure.set_lintegral_rnDeriv: ∫⁻ x in s, μ.rnDeriv ν x ∂ν = μ s if μ ≪ ν. There is also a version of this result for the Bochner integral.

## Tags #

theorem MeasureTheory.Measure.withDensity_rnDeriv_eq {α : Type u_1} {m : } (μ : ) (ν : ) [μ.HaveLebesgueDecomposition ν] (h : μ.AbsolutelyContinuous ν) :
ν.withDensity (μ.rnDeriv ν) = μ
theorem MeasureTheory.Measure.absolutelyContinuous_iff_withDensity_rnDeriv_eq {α : Type u_1} {m : } {μ : } {ν : } [μ.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 : } {μ : } {ν : } [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) :
∀ᵐ (x : α) ∂μ, 0 < μ.rnDeriv ν x
theorem MeasureTheory.Measure.rnDeriv_pos' {α : Type u_1} {m : } {μ : } {ν : } (hμν : μ.AbsolutelyContinuous ν) :
∀ᵐ (x : α) ∂μ, 0 < ν.rnDeriv μ x
theorem MeasureTheory.Measure.rnDeriv_withDensity_withDensity_rnDeriv_left {α : Type u_1} {m : } {f : αENNReal} (μ : ) (ν : ) (hf : ) (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 : } {f : αENNReal} (μ : ) (ν : ) (hf : ) (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 : } {μ : } {f : αENNReal} {ν : } (hμν : μ.AbsolutelyContinuous ν) (hf : ) :
(μ.withDensity f).rnDeriv ν =ᵐ[ν] fun (x : α) => f x * μ.rnDeriv ν x
theorem MeasureTheory.Measure.rnDeriv_withDensity_left {α : Type u_1} {m : } {f : αENNReal} {μ : } {ν : } (hfμ : ) (hfν : ) (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 : } {μ : } {f : αENNReal} {ν : } (hμν : μ.AbsolutelyContinuous ν) (hf : ) (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 : } {f : αENNReal} (μ : ) (ν : ) (hf : ) (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 : } {μ : } {ν : } {ν' : } (h : μ.MutuallySingular ν) (hνν' : ν.AbsolutelyContinuous ν') :
μ.rnDeriv ν' =ᵐ[ν] 0
theorem MeasureTheory.Measure.rnDeriv_add_right_of_absolutelyContinuous_of_mutuallySingular {α : Type u_1} {m : } {μ : } {ν : } {ν' : } (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 : } {μ : } {ν : } {ν' : } (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 : } {μ : } {ν : } {ν' : } (hνν' : ν.MutuallySingular ν') :
μ.rnDeriv (ν + ν') =ᵐ[ν] μ.rnDeriv ν
theorem MeasureTheory.Measure.rnDeriv_withDensity_rnDeriv {α : Type u_1} {m : } {μ : } {ν : } (hμν : μ.AbsolutelyContinuous ν) :
μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᵐ[μ] μ.rnDeriv ν
theorem MeasureTheory.Measure.inv_rnDeriv_aux {α : Type u_1} {m : } {μ : } {ν : } (hμν : μ.AbsolutelyContinuous ν) (hνμ : ν.AbsolutelyContinuous μ) :
(μ.rnDeriv ν)⁻¹ =ᵐ[μ] ν.rnDeriv μ

Auxiliary lemma for inv_rnDeriv.

theorem MeasureTheory.Measure.inv_rnDeriv {α : Type u_1} {m : } {μ : } {ν : } (hμν : μ.AbsolutelyContinuous ν) :
(μ.rnDeriv ν)⁻¹ =ᵐ[μ] ν.rnDeriv μ
theorem MeasureTheory.Measure.inv_rnDeriv' {α : Type u_1} {m : } {μ : } {ν : } (hμν : μ.AbsolutelyContinuous ν) :
(ν.rnDeriv μ)⁻¹ =ᵐ[μ] μ.rnDeriv ν
theorem MeasureTheory.Measure.set_lintegral_rnDeriv_le {α : Type u_1} {m : } {μ : } {ν : } (s : Set α) :
∫⁻ (x : α) in s, μ.rnDeriv ν xν μ s
theorem MeasureTheory.Measure.set_lintegral_rnDeriv' {α : Type u_1} {m : } {μ : } {ν : } [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) {s : Set α} (hs : ) :
∫⁻ (x : α) in s, μ.rnDeriv ν xν = μ s
theorem MeasureTheory.Measure.set_lintegral_rnDeriv {α : Type u_1} {m : } {μ : } {ν : } [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) (s : Set α) :
∫⁻ (x : α) in s, μ.rnDeriv ν xν = μ s
theorem MeasureTheory.Measure.lintegral_rnDeriv {α : Type u_1} {m : } {μ : } {ν : } [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) :
∫⁻ (x : α), μ.rnDeriv ν xν = μ Set.univ
theorem MeasureTheory.Measure.integrableOn_toReal_rnDeriv {α : Type u_1} {m : } {μ : } {ν : } {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 : } {μ : } {ν : } {s : Set α} (hs : ) :
∫ (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 : } {μ : } {ν : } {s : Set α} (hs : ) :
∫ (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 : } {μ : } {ν : } (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 : } {μ : } {ν : } (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 : } {μ : } {ν : } {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 : } {μ : } {ν : } {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 : } {μ : } {ν : } [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) {s : Set α} (hs : ) :
∫ (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 : } {μ : } {ν : } [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) {s : Set α} (hs : ) :
∫ (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 : } {μ : } {ν : } (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 : } {μ : } {ν : } (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 : } {μ : } {ν : } (hμν : μ.AbsolutelyContinuous ν) :
∫ (x : α), (μ.rnDeriv ν x).toRealν = (μ Set.univ).toReal
theorem MeasureTheory.Measure.rnDeriv_mul_rnDeriv {α : Type u_1} {m : } {μ : } {ν : } {κ : } (hμν : μ.AbsolutelyContinuous ν) :
μ.rnDeriv ν * ν.rnDeriv κ =ᵐ[κ] μ.rnDeriv κ
theorem MeasureTheory.Measure.rnDeriv_le_one_of_le {α : Type u_1} {m : } {μ : } {ν : } (hμν : μ ν) :
μ.rnDeriv ν ≤ᵐ[ν] 1
theorem MeasurableEmbedding.rnDeriv_map_aux {α : Type u_1} {β : Type u_2} {m : } {μ : } {ν : } {mβ : } {f : αβ} (hf : ) (hμν : μ.AbsolutelyContinuous ν) :
(fun (x : α) => .rnDeriv (f x)) =ᵐ[ν] μ.rnDeriv ν
theorem MeasurableEmbedding.rnDeriv_map {α : Type u_1} {β : Type u_2} {m : } {mβ : } {f : αβ} (hf : ) (μ : ) (ν : ) :
(fun (x : α) => .rnDeriv (f x)) =ᵐ[ν] μ.rnDeriv ν
theorem MeasurableEmbedding.map_withDensity_rnDeriv {α : Type u_1} {β : Type u_2} {m : } {mβ : } {f : αβ} (hf : ) (μ : ) (ν : ) :
MeasureTheory.Measure.map f (ν.withDensity (μ.rnDeriv ν)) = .withDensity (.rnDeriv )
theorem MeasurableEmbedding.singularPart_map {α : Type u_1} {β : Type u_2} {m : } {mβ : } {f : αβ} (hf : ) (μ : ) (ν : ) :
.singularPart = MeasureTheory.Measure.map f (μ.singularPart ν)
theorem MeasureTheory.SignedMeasure.withDensityᵥ_rnDeriv_eq {α : Type u_1} {m : } (s : ) (μ : ) (h : MeasureTheory.VectorMeasure.AbsolutelyContinuous s μ.toENNRealVectorMeasure) :
μ.withDensityᵥ (s.rnDeriv μ) = s
theorem MeasureTheory.SignedMeasure.absolutelyContinuous_iff_withDensityᵥ_rnDeriv_eq {α : Type u_1} {m : } (s : ) (μ : ) :
MeasureTheory.VectorMeasure.AbsolutelyContinuous s μ.toENNRealVectorMeasure μ.withDensityᵥ (s.rnDeriv μ) = s

The Radon-Nikodym theorem for signed measures.

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