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.set_lintegral_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 α) [MeasureTheory.Measure.HaveLebesgueDecomposition μ ν] (h : MeasureTheory.Measure.AbsolutelyContinuous μ ν) : ν.withDensity (μ.rnDeriv ν) = μ

theorem MeasureTheory.Measure.absolutelyContinuous_iff_withDensity_rnDeriv_eq {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.Measure.HaveLebesgueDecomposition μ ν] : MeasureTheory.Measure.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 α} [MeasureTheory.Measure.HaveLebesgueDecomposition μ ν] (hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν) : ∀ᵐ (x : α) ∂μ, 0 < μ.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 < ν.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 ν =ᶠ[MeasureTheory.Measure.ae ν] (μ.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) =ᶠ[MeasureTheory.Measure.ae ν] μ.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μν : MeasureTheory.Measure.AbsolutelyContinuous μ ν) (hf : AEMeasurable f ν) : (μ.withDensity f).rnDeriv ν =ᶠ[MeasureTheory.Measure.ae ν] 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 ν =ᶠ[MeasureTheory.Measure.ae ν] 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μν : MeasureTheory.Measure.AbsolutelyContinuous μ ν) (hf : AEMeasurable f ν) (hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0) (hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ⊤) : μ.rnDeriv (ν.withDensity f) =ᶠ[MeasureTheory.Measure.ae ν] 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) =ᶠ[MeasureTheory.Measure.ae ν] 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 : MeasureTheory.Measure.MutuallySingular μ ν) (hνν' : MeasureTheory.Measure.AbsolutelyContinuous ν ν') : μ.rnDeriv ν' =ᶠ[MeasureTheory.Measure.ae ν] 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μν : MeasureTheory.Measure.AbsolutelyContinuous μ ν) (hνν' : MeasureTheory.Measure.MutuallySingular ν ν') : μ.rnDeriv (ν + ν') =ᶠ[MeasureTheory.Measure.ae ν] μ.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μν' : MeasureTheory.Measure.MutuallySingular μ ν') (hνν' : MeasureTheory.Measure.MutuallySingular ν ν') : μ.rnDeriv (ν + ν') =ᶠ[MeasureTheory.Measure.ae ν] μ.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νν' : MeasureTheory.Measure.MutuallySingular ν ν') : μ.rnDeriv (ν + ν') =ᶠ[MeasureTheory.Measure.ae ν] μ.rnDeriv ν

theorem MeasureTheory.Measure.rnDeriv_withDensity_rnDeriv {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν) : μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᶠ[MeasureTheory.Measure.ae μ] μ.rnDeriv ν

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 ν μ) : (μ.rnDeriv ν)⁻¹ =ᶠ[MeasureTheory.Measure.ae μ] ν.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μν : MeasureTheory.Measure.AbsolutelyContinuous μ ν) : (μ.rnDeriv ν)⁻¹ =ᶠ[MeasureTheory.Measure.ae μ] ν.rnDeriv μ

theorem MeasureTheory.Measure.inv_rnDeriv' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν) : (ν.rnDeriv μ)⁻¹ =ᶠ[MeasureTheory.Measure.ae μ] μ.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 α} [MeasureTheory.Measure.HaveLebesgueDecomposition μ ν] (hμν : MeasureTheory.Measure.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 α} [MeasureTheory.Measure.HaveLebesgueDecomposition μ ν] [MeasureTheory.SFinite ν] (hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν) (s : Set α) : ∫⁻ (x : α) in s, μ.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 : α), μ.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 μ] [MeasureTheory.Measure.HaveLebesgueDecomposition μ ν] (hμν : MeasureTheory.Measure.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 μ] [MeasureTheory.Measure.HaveLebesgueDecomposition μ ν] (hμν : MeasureTheory.Measure.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μν : MeasureTheory.Measure.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μν : MeasureTheory.Measure.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μν : MeasureTheory.Measure.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μν : MeasureTheory.Measure.AbsolutelyContinuous μ ν) : μ.rnDeriv ν * ν.rnDeriv κ =ᶠ[MeasureTheory.Measure.ae κ] μ.rnDeriv κ

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.

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 : α), μ.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, μ.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 : α) => (μ.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 : α) => (μ.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 : α), (μ.rnDeriv ν x).toReal • f x ∂ν = ∫ (x : α), f x ∂μ