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

theorem MeasureTheory.Measure.absolutelyContinuous_iff_withDensity_rnDeriv_eq {α : Type u_1} {m : MeasurableSpace α} {μ ν : 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 α} {μ ν : Measure α} [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) : ∀ᵐ (x : α) ∂μ, 0 < μ.rnDeriv ν x

theorem MeasureTheory.Measure.rnDeriv_pos' {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} [ν.HaveLebesgueDecomposition μ] [SigmaFinite μ] (hμν : μ.AbsolutelyContinuous ν) : ∀ᵐ (x : α) ∂μ, 0 < ν.rnDeriv μ x

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

Auxiliary lemma for rnDeriv_withDensity_right.

theorem MeasureTheory.Measure.rnDeriv_withDensity_left_of_absolutelyContinuous {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} {ν : Measure α} [SigmaFinite μ] [SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) (hf : AEMeasurable f ν) : (μ.withDensity f).rnDeriv ν =ᶠ[ae ν] fun (x : α) => f x * μ.rnDeriv ν x

theorem MeasureTheory.Measure.rnDeriv_withDensity_left {α : Type u_1} {m : MeasurableSpace α} {f : α → ENNReal} {μ ν : Measure α} [SigmaFinite μ] [SigmaFinite ν] (hfν : AEMeasurable f ν) (hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤) : (μ.withDensity f).rnDeriv ν =ᶠ[ae ν] fun (x : α) => f x * μ.rnDeriv ν x

theorem MeasureTheory.Measure.rnDeriv_withDensity_right_of_absolutelyContinuous {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} {ν : Measure α} [μ.HaveLebesgueDecomposition ν] [SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) (hf : AEMeasurable f ν) (hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0) (hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ⊤) : μ.rnDeriv (ν.withDensity f) =ᶠ[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} (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] (hf : AEMeasurable f ν) (hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0) (hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ⊤) : μ.rnDeriv (ν.withDensity f) =ᶠ[ae ν] fun (x : α) => (f x)⁻¹ * μ.rnDeriv ν x

theorem MeasureTheory.Measure.rnDeriv_eq_zero_of_mutuallySingular {α : Type u_1} {m : MeasurableSpace α} {μ ν ν' : Measure α} [μ.HaveLebesgueDecomposition ν'] [SigmaFinite ν'] (h : μ.MutuallySingular ν) (hνν' : ν.AbsolutelyContinuous ν') : μ.rnDeriv ν' =ᶠ[ae ν] 0

theorem MeasureTheory.Measure.rnDeriv_add_right_of_absolutelyContinuous_of_mutuallySingular {α : Type u_1} {m : MeasurableSpace α} {μ ν ν' : Measure α} [μ.HaveLebesgueDecomposition ν] [μ.HaveLebesgueDecomposition (ν + ν')] [SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) (hνν' : ν.MutuallySingular ν') : μ.rnDeriv (ν + ν') =ᶠ[ae ν] μ.rnDeriv ν

Auxiliary lemma for rnDeriv_add_right_of_mutuallySingular.

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

Auxiliary lemma for rnDeriv_add_right_of_mutuallySingular.

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

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

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

Auxiliary lemma for inv_rnDeriv.

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

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

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

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

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

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

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

theorem MeasureTheory.Measure.integrableOn_toReal_rnDeriv {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} {s : Set α} (hμs : μ s ≠ ⊤) : IntegrableOn (fun (x : α) => (μ.rnDeriv ν x).toReal) s ν

theorem MeasureTheory.Measure.setIntegral_toReal_rnDeriv_eq_withDensity' {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} [SigmaFinite μ] {s : Set α} (hs : MeasurableSet s) : ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = (ν.withDensity (μ.rnDeriv ν)).real s

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

theorem MeasureTheory.Measure.setIntegral_toReal_rnDeriv_le {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} [SigmaFinite μ] {s : Set α} (hμs : μ s ≠ ⊤) : ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν ≤ μ.real s

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

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

theorem MeasureTheory.Measure.integral_toReal_rnDeriv {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} [SigmaFinite μ] [SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) : ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = μ.real Set.univ

theorem MeasureTheory.Measure.integral_toReal_rnDeriv' {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} [IsFiniteMeasure μ] [SigmaFinite ν] : ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = μ.real Set.univ - (μ.singularPart ν).real Set.univ

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

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

theorem MeasureTheory.Measure.rnDeriv_le_one_of_le {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} (hμν : μ ≤ ν) [SigmaFinite ν] : μ.rnDeriv ν ≤ᶠ[ae ν] 1

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

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

theorem MeasurableEmbedding.rnDeriv_map_aux {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ ν : 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.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.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.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] : (MeasureTheory.Measure.map f μ).singularPart (MeasureTheory.Measure.map f ν) = MeasureTheory.Measure.map f (μ.singularPart ν)

theorem MeasureTheory.lintegral_rnDeriv_mul {α : Type u_3} {m : MeasurableSpace α} {μ ν : 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 α} {μ ν : 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 α} {μ ν : Measure α} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [μ.HaveLebesgueDecomposition ν] [SigmaFinite μ] {f : α → E} (hμν : μ.AbsolutelyContinuous ν) : Integrable (fun (x : α) => (μ.rnDeriv ν x).toReal • f x) ν ↔ Integrable f μ

theorem MeasureTheory.integral_rnDeriv_smul {α : Type u_3} {m : MeasurableSpace α} {μ ν : Measure α} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [μ.HaveLebesgueDecomposition ν] [SigmaFinite μ] {f : α → E} (hμν : μ.AbsolutelyContinuous ν) : ∫ (x : α), (μ.rnDeriv ν x).toReal • f x ∂ν = ∫ (x : α), f x ∂μ

theorem MeasureTheory.setIntegral_rnDeriv_smul {α : Type u_3} {m : MeasurableSpace α} {μ ν : Measure α} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [μ.HaveLebesgueDecomposition ν] [SigmaFinite μ] {f : α → E} (hμν : μ.AbsolutelyContinuous ν) {s : Set α} (hs : MeasurableSet s) : ∫ (x : α) in s, (μ.rnDeriv ν x).toReal • f x ∂ν = ∫ (x : α) in s, f x ∂μ

See also setIntegral_rnDeriv_smul' for a version that requires both measures to be σ-finite, but doesn't require s to be a measurable set.

theorem MeasureTheory.setIntegral_rnDeriv_smul' {α : Type u_3} {m : MeasurableSpace α} {μ ν : Measure α} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [SigmaFinite μ] {f : α → E} [SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) (s : Set α) : ∫ (x : α) in s, (μ.rnDeriv ν x).toReal • f x ∂ν = ∫ (x : α) in s, f x ∂μ

A version of setIntegral_rnDeriv_smul that requires both measures to be σ-finite, but doesn't require s to be a measurable set.

theorem MeasureTheory.mconv_eq_withDensity_mlconvolution_rnDeriv {G : Type u_3} [Group G] {mG : MeasurableSpace G} [MeasurableMul₂ G] [MeasurableInv G] {μ : Measure G} [μ.IsMulLeftInvariant] [SFinite μ] {ν₁ ν₂ : Measure G} [ν₁.HaveLebesgueDecomposition μ] [ν₂.HaveLebesgueDecomposition μ] (hν₁ : ν₁.AbsolutelyContinuous μ) (hν₂ : ν₂.AbsolutelyContinuous μ) : ν₁.mconv ν₂ = μ.withDensity (mlconvolution (ν₁.rnDeriv μ) (ν₂.rnDeriv μ) μ)

theorem MeasureTheory.conv_eq_withDensity_lconvolution_rnDeriv {G : Type u_3} [AddGroup G] {mG : MeasurableSpace G} [MeasurableAdd₂ G] [MeasurableNeg G] {μ : Measure G} [μ.IsAddLeftInvariant] [SFinite μ] {ν₁ ν₂ : Measure G} [ν₁.HaveLebesgueDecomposition μ] [ν₂.HaveLebesgueDecomposition μ] (hν₁ : ν₁.AbsolutelyContinuous μ) (hν₂ : ν₂.AbsolutelyContinuous μ) : ν₁.conv ν₂ = μ.withDensity (lconvolution (ν₁.rnDeriv μ) (ν₂.rnDeriv μ) μ)

theorem MeasureTheory.HaveLebesgueDecomposition.mconv {G : Type u_3} [Group G] {mG : MeasurableSpace G} [MeasurableMul₂ G] [MeasurableInv G] {μ : Measure G} [μ.IsMulLeftInvariant] [SFinite μ] {ν₁ ν₂ : Measure G} [ν₁.HaveLebesgueDecomposition μ] [ν₂.HaveLebesgueDecomposition μ] (hν₁ : ν₁.AbsolutelyContinuous μ) (hν₂ : ν₂.AbsolutelyContinuous μ) : (ν₁.mconv ν₂).HaveLebesgueDecomposition μ

theorem MeasureTheory.HaveLebesgueDecomposition.conv {G : Type u_3} [AddGroup G] {mG : MeasurableSpace G} [MeasurableAdd₂ G] [MeasurableNeg G] {μ : Measure G} [μ.IsAddLeftInvariant] [SFinite μ] {ν₁ ν₂ : Measure G} [ν₁.HaveLebesgueDecomposition μ] [ν₂.HaveLebesgueDecomposition μ] (hν₁ : ν₁.AbsolutelyContinuous μ) (hν₂ : ν₂.AbsolutelyContinuous μ) : (ν₁.conv ν₂).HaveLebesgueDecomposition μ

theorem MeasureTheory.rnDeriv_mconv {G : Type u_3} [Group G] {mG : MeasurableSpace G} [MeasurableMul₂ G] [MeasurableInv G] {μ : Measure G} [μ.IsMulLeftInvariant] [SFinite μ] {ν₁ ν₂ : Measure G} [IsFiniteMeasure ν₁] [IsFiniteMeasure ν₂] [ν₁.HaveLebesgueDecomposition μ] [ν₂.HaveLebesgueDecomposition μ] (hν₁ : ν₁.AbsolutelyContinuous μ) (hν₂ : ν₂.AbsolutelyContinuous μ) : (ν₁.mconv ν₂).rnDeriv μ =ᶠ[ae μ] mlconvolution (ν₁.rnDeriv μ) (ν₂.rnDeriv μ) μ

theorem MeasureTheory.rnDeriv_conv {G : Type u_3} [AddGroup G] {mG : MeasurableSpace G} [MeasurableAdd₂ G] [MeasurableNeg G] {μ : Measure G} [μ.IsAddLeftInvariant] [SFinite μ] {ν₁ ν₂ : Measure G} [IsFiniteMeasure ν₁] [IsFiniteMeasure ν₂] [ν₁.HaveLebesgueDecomposition μ] [ν₂.HaveLebesgueDecomposition μ] (hν₁ : ν₁.AbsolutelyContinuous μ) (hν₂ : ν₂.AbsolutelyContinuous μ) : (ν₁.conv ν₂).rnDeriv μ =ᶠ[ae μ] lconvolution (ν₁.rnDeriv μ) (ν₂.rnDeriv μ) μ

theorem MeasureTheory.rnDeriv_mconv' {G : Type u_3} [Group G] {mG : MeasurableSpace G} [MeasurableMul₂ G] [MeasurableInv G] {μ : Measure G} [μ.IsMulLeftInvariant] [SigmaFinite μ] {ν₁ ν₂ : Measure G} [SigmaFinite ν₁] [SigmaFinite ν₂] (hν₁ : ν₁.AbsolutelyContinuous μ) (hν₂ : ν₂.AbsolutelyContinuous μ) : (ν₁.mconv ν₂).rnDeriv μ =ᶠ[ae μ] mlconvolution (ν₁.rnDeriv μ) (ν₂.rnDeriv μ) μ

theorem MeasureTheory.rnDeriv_conv' {G : Type u_3} [AddGroup G] {mG : MeasurableSpace G} [MeasurableAdd₂ G] [MeasurableNeg G] {μ : Measure G} [μ.IsAddLeftInvariant] [SigmaFinite μ] {ν₁ ν₂ : Measure G} [SigmaFinite ν₁] [SigmaFinite ν₂] (hν₁ : ν₁.AbsolutelyContinuous μ) (hν₂ : ν₂.AbsolutelyContinuous μ) : (ν₁.conv ν₂).rnDeriv μ =ᶠ[ae μ] lconvolution (ν₁.rnDeriv μ) (ν₂.rnDeriv μ) μ