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

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.setLIntegral_rnDeriv: ∫⁻ x in s, μ.rnDeriv ν x ∂ν = μ s if μ ≪ ν. 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 α) [μ.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 α} [ν.HaveLebesgueDecomposition μ] [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_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_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 α} [μ.HaveLebesgueDecomposition ν] [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.Measure α} [μ.HaveLebesgueDecomposition ν'] [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 α} [μ.HaveLebesgueDecomposition ν] [μ.HaveLebesgueDecomposition (ν + ν')] [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 α} [μ.HaveLebesgueDecomposition ν] [ν.HaveLebesgueDecomposition μ] [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.setLIntegral_rnDeriv_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (s : Set α) : ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≤ μ s

@[deprecated MeasureTheory.Measure.setLIntegral_rnDeriv_le]

theorem MeasureTheory.Measure.set_lintegral_rnDeriv_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (s : Set α) : ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≤ μ s

Alias of MeasureTheory.Measure.setLIntegral_rnDeriv_le.

theorem MeasureTheory.Measure.lintegral_rnDeriv_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} : ∫⁻ (x : α), μ.rnDeriv ν x ∂ν ≤ μ Set.univ

theorem MeasureTheory.Measure.setLIntegral_rnDeriv' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) {s : Set α} (hs : MeasurableSet s) : ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν = μ s

@[deprecated MeasureTheory.Measure.setLIntegral_rnDeriv']

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

Alias of MeasureTheory.Measure.setLIntegral_rnDeriv'.

theorem MeasureTheory.Measure.setLIntegral_rnDeriv {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν] [MeasureTheory.SFinite ν] (hμν : μ.AbsolutelyContinuous ν) (s : Set α) : ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν = μ s

@[deprecated MeasureTheory.Measure.setLIntegral_rnDeriv]

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

Alias of MeasureTheory.Measure.setLIntegral_rnDeriv.

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.integral_toReal_rnDeriv' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.SigmaFinite ν] : ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = (μ Set.univ).toReal - ((μ.singularPart ν) 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 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 MeasureTheory.Measure.rnDeriv_le_one_of_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (hμν : μ ≤ ν) [MeasureTheory.SigmaFinite ν] : μ.rnDeriv ν ≤ᵐ[ν] 1

theorem MeasureTheory.Measure.rnDeriv_le_one_iff_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν] [MeasureTheory.SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) : μ.rnDeriv ν ≤ᵐ[ν] 1 ↔ μ ≤ ν

theorem MeasureTheory.Measure.rnDeriv_eq_one_iff_eq {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν] [MeasureTheory.SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) : μ.rnDeriv ν =ᵐ[ν] 1 ↔ μ = ν

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 ν

theorem MeasurableEmbedding.map_withDensity_rnDeriv {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (hf : MeasurableEmbedding f) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] : MeasureTheory.Measure.map f (ν.withDensity (μ.rnDeriv ν)) = (MeasureTheory.Measure.map f ν).withDensity ((MeasureTheory.Measure.map f μ).rnDeriv (MeasureTheory.Measure.map f ν))

theorem MeasurableEmbedding.singularPart_map {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (hf : MeasurableEmbedding f) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] : (MeasureTheory.Measure.map f μ).singularPart (MeasureTheory.Measure.map f ν) = MeasureTheory.Measure.map f (μ.singularPart ν)

theorem MeasureTheory.SignedMeasure.withDensityᵥ_rnDeriv_eq {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (h : MeasureTheory.VectorMeasure.AbsolutelyContinuous s μ.toENNRealVectorMeasure) : μ.withDensityᵥ (s.rnDeriv μ) = 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 μ.toENNRealVectorMeasure ↔ μ.withDensityᵥ (s.rnDeriv μ) = s

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.setLIntegral_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 ∂μ

@[deprecated MeasureTheory.setLIntegral_rnDeriv_mul]

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 ∂μ

Alias of MeasureTheory.setLIntegral_rnDeriv_mul.

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 ∂μ

theorem MeasureTheory.setIntegral_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} {s : Set α} (hs : MeasurableSet s) : ∫ (x : α) in s, (μ.rnDeriv ν x).toReal • f x ∂ν = ∫ (x : α) in s, f x ∂μ