# Lebesgue decomposition #

This file proves the Lebesgue decomposition theorem. The Lebesgue decomposition theorem states that, given two σ-finite measures μ and ν, there exists a σ-finite measure ξ and a measurable function f such that μ = ξ + fν and ξ is mutually singular with respect to ν.

## Tags #

Lebesgue decomposition theorem

class MeasureTheory.Measure.HaveLebesgueDecomposition {α : Type u_1} {m : } (μ : ) (ν : ) :

A pair of measures μ and ν is said to HaveLebesgueDecomposition if there exists a measure ξ and a measurable function f, such that ξ is mutually singular with respect to ν and μ = ξ + ν.withDensity f.

Instances
theorem MeasureTheory.Measure.HaveLebesgueDecomposition.lebesgue_decomposition {α : Type u_1} {m : } {μ : } {ν : } [self : μ.HaveLebesgueDecomposition ν] :
∃ (p : × (αENNReal)), Measurable p.2 p.1.MutuallySingular ν μ = p.1 + ν.withDensity p.2
theorem MeasureTheory.Measure.singularPart_def {α : Type u_3} {m : } (μ : ) (ν : ) :
μ.singularPart ν = if h : μ.HaveLebesgueDecomposition ν then ().1 else 0
@[irreducible]
noncomputable def MeasureTheory.Measure.singularPart {α : Type u_3} {m : } (μ : ) (ν : ) :

If a pair of measures HaveLebesgueDecomposition, then singularPart chooses the measure from HaveLebesgueDecomposition, otherwise it returns the zero measure. For sigma-finite measures, μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν).

Equations
Instances For
@[irreducible]
noncomputable def MeasureTheory.Measure.rnDeriv {α : Type u_3} {m : } (μ : ) (ν : ) :
αENNReal

If a pair of measures HaveLebesgueDecomposition, then rnDeriv chooses the measurable function from HaveLebesgueDecomposition, otherwise it returns the zero function. For sigma-finite measures, μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν).

Equations
Instances For
theorem MeasureTheory.Measure.rnDeriv_def {α : Type u_3} {m : } (μ : ) (ν : ) :
μ.rnDeriv ν = if h : μ.HaveLebesgueDecomposition ν then ().2 else 0
theorem MeasureTheory.Measure.haveLebesgueDecomposition_spec {α : Type u_1} {m : } (μ : ) (ν : ) [h : μ.HaveLebesgueDecomposition ν] :
Measurable (μ.rnDeriv ν) (μ.singularPart ν).MutuallySingular ν μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
theorem MeasureTheory.Measure.rnDeriv_of_not_haveLebesgueDecomposition {α : Type u_1} {m : } {μ : } {ν : } (h : ¬μ.HaveLebesgueDecomposition ν) :
μ.rnDeriv ν = 0
theorem MeasureTheory.Measure.singularPart_of_not_haveLebesgueDecomposition {α : Type u_1} {m : } {μ : } {ν : } (h : ¬μ.HaveLebesgueDecomposition ν) :
μ.singularPart ν = 0
theorem MeasureTheory.Measure.measurable_rnDeriv {α : Type u_1} {m : } (μ : ) (ν : ) :
Measurable (μ.rnDeriv ν)
theorem MeasureTheory.Measure.mutuallySingular_singularPart {α : Type u_1} {m : } (μ : ) (ν : ) :
(μ.singularPart ν).MutuallySingular ν
theorem MeasureTheory.Measure.haveLebesgueDecomposition_add {α : Type u_1} {m : } (μ : ) (ν : ) [μ.HaveLebesgueDecomposition ν] :
μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
theorem MeasureTheory.Measure.singularPart_add_rnDeriv {α : Type u_1} {m : } (μ : ) (ν : ) [μ.HaveLebesgueDecomposition ν] :
μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = μ
theorem MeasureTheory.Measure.rnDeriv_add_singularPart {α : Type u_1} {m : } (μ : ) (ν : ) [μ.HaveLebesgueDecomposition ν] :
ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν = μ
Equations
• =
instance MeasureTheory.Measure.instHaveLebesgueDecompositionZeroRight {α : Type u_1} {m : } {μ : } :
μ.HaveLebesgueDecomposition 0
Equations
• =
instance MeasureTheory.Measure.instHaveLebesgueDecompositionSelf {α : Type u_1} {m : } {μ : } :
μ.HaveLebesgueDecomposition μ
Equations
• =
instance MeasureTheory.Measure.HaveLebesgueDecomposition.sum_left {α : Type u_1} {m : } {ν : } {ι : Type u_3} [] (μ : ) [∀ (i : ι), (μ i).HaveLebesgueDecomposition ν] :
.HaveLebesgueDecomposition ν
Equations
• =
instance MeasureTheory.Measure.HaveLebesgueDecomposition.add_left {α : Type u_1} {m : } {μ : } {ν : } {μ' : } [μ.HaveLebesgueDecomposition ν] [μ'.HaveLebesgueDecomposition ν] :
(μ + μ').HaveLebesgueDecomposition ν
Equations
• =
instance MeasureTheory.Measure.haveLebesgueDecompositionSMul' {α : Type u_1} {m : } (μ : ) (ν : ) [μ.HaveLebesgueDecomposition ν] (r : ENNReal) :
(r μ).HaveLebesgueDecomposition ν
Equations
• =
instance MeasureTheory.Measure.haveLebesgueDecompositionSMul {α : Type u_1} {m : } (μ : ) (ν : ) [μ.HaveLebesgueDecomposition ν] (r : NNReal) :
(r μ).HaveLebesgueDecomposition ν
Equations
• =
instance MeasureTheory.Measure.haveLebesgueDecompositionSMulRight {α : Type u_1} {m : } (μ : ) (ν : ) [μ.HaveLebesgueDecomposition ν] (r : NNReal) :
μ.HaveLebesgueDecomposition (r ν)
Equations
• =
theorem MeasureTheory.Measure.haveLebesgueDecomposition_withDensity {α : Type u_1} {m : } (μ : ) {f : αENNReal} (hf : ) :
(μ.withDensity f).HaveLebesgueDecomposition μ
instance MeasureTheory.Measure.haveLebesgueDecompositionRnDeriv {α : Type u_1} {m : } (μ : ) (ν : ) :
(ν.withDensity (μ.rnDeriv ν)).HaveLebesgueDecomposition ν
Equations
• =
instance MeasureTheory.Measure.instHaveLebesgueDecompositionSingularPart {α : Type u_1} {m : } {μ : } {ν : } :
(μ.singularPart ν).HaveLebesgueDecomposition ν
Equations
• =
theorem MeasureTheory.Measure.singularPart_le {α : Type u_1} {m : } (μ : ) (ν : ) :
μ.singularPart ν μ
theorem MeasureTheory.Measure.withDensity_rnDeriv_le {α : Type u_1} {m : } (μ : ) (ν : ) :
ν.withDensity (μ.rnDeriv ν) μ
theorem AEMeasurable.singularPart {α : Type u_1} {m : } {μ : } {β : Type u_3} :
∀ {x : } {f : αβ}, ∀ (ν : ), AEMeasurable f (μ.singularPart ν)
theorem AEMeasurable.withDensity_rnDeriv {α : Type u_1} {m : } {μ : } {β : Type u_3} :
∀ {x : } {f : αβ}, ∀ (ν : ), AEMeasurable f (ν.withDensity (μ.rnDeriv ν))
theorem MeasureTheory.Measure.MutuallySingular.singularPart {α : Type u_1} {m : } {μ : } {ν : } (h : μ.MutuallySingular ν) (ν' : ) :
(μ.singularPart ν').MutuallySingular ν
theorem MeasureTheory.Measure.absolutelyContinuous_withDensity_rnDeriv {α : Type u_1} {m : } {μ : } {ν : } [ν.HaveLebesgueDecomposition μ] (hμν : μ.AbsolutelyContinuous ν) :
μ.AbsolutelyContinuous (μ.withDensity (ν.rnDeriv μ))
theorem MeasureTheory.Measure.singularPart_eq_zero_of_ac {α : Type u_1} {m : } {μ : } {ν : } (h : μ.AbsolutelyContinuous ν) :
μ.singularPart ν = 0
@[simp]
theorem MeasureTheory.Measure.singularPart_zero {α : Type u_1} {m : } (ν : ) :
@[simp]
theorem MeasureTheory.Measure.singularPart_zero_right {α : Type u_1} {m : } (μ : ) :
μ.singularPart 0 = μ
theorem MeasureTheory.Measure.singularPart_eq_zero {α : Type u_1} {m : } (μ : ) (ν : ) [μ.HaveLebesgueDecomposition ν] :
μ.singularPart ν = 0 μ.AbsolutelyContinuous ν
@[simp]
theorem MeasureTheory.Measure.withDensity_rnDeriv_eq_zero {α : Type u_1} {m : } (μ : ) (ν : ) [μ.HaveLebesgueDecomposition ν] :
ν.withDensity (μ.rnDeriv ν) = 0 μ.MutuallySingular ν
@[simp]
theorem MeasureTheory.Measure.rnDeriv_eq_zero {α : Type u_1} {m : } (μ : ) (ν : ) [μ.HaveLebesgueDecomposition ν] :
μ.rnDeriv ν =ᵐ[ν] 0 μ.MutuallySingular ν
theorem MeasureTheory.Measure.rnDeriv_zero {α : Type u_1} {m : } (ν : ) :
theorem MeasureTheory.Measure.MutuallySingular.rnDeriv_ae_eq_zero {α : Type u_1} {m : } {μ : } {ν : } (hμν : μ.MutuallySingular ν) :
μ.rnDeriv ν =ᵐ[ν] 0
@[simp]
theorem MeasureTheory.Measure.singularPart_withDensity {α : Type u_1} {m : } (ν : ) (f : αENNReal) :
(ν.withDensity f).singularPart ν = 0
theorem MeasureTheory.Measure.rnDeriv_singularPart {α : Type u_1} {m : } (μ : ) (ν : ) :
(μ.singularPart ν).rnDeriv ν =ᵐ[ν] 0
@[simp]
theorem MeasureTheory.Measure.singularPart_self {α : Type u_1} {m : } (μ : ) :
μ.singularPart μ = 0
theorem MeasureTheory.Measure.rnDeriv_self {α : Type u_1} {m : } (μ : ) :
μ.rnDeriv μ =ᵐ[μ] fun (x : α) => 1
theorem MeasureTheory.Measure.singularPart_eq_self {α : Type u_1} {m : } {μ : } {ν : } [μ.HaveLebesgueDecomposition ν] :
μ.singularPart ν = μ μ.MutuallySingular ν
@[simp]
theorem MeasureTheory.Measure.singularPart_singularPart {α : Type u_1} {m : } (μ : ) (ν : ) :
(μ.singularPart ν).singularPart ν = μ.singularPart ν
instance MeasureTheory.Measure.singularPart.instIsFiniteMeasure {α : Type u_1} {m : } {μ : } {ν : } :
MeasureTheory.IsFiniteMeasure (μ.singularPart ν)
Equations
• =
instance MeasureTheory.Measure.singularPart.instSigmaFinite {α : Type u_1} {m : } {μ : } {ν : } :
MeasureTheory.SigmaFinite (μ.singularPart ν)
Equations
• =
instance MeasureTheory.Measure.singularPart.instIsLocallyFiniteMeasure {α : Type u_1} {m : } {μ : } {ν : } [] :
Equations
• =
instance MeasureTheory.Measure.withDensity.instIsFiniteMeasure {α : Type u_1} {m : } {μ : } {ν : } :
MeasureTheory.IsFiniteMeasure (ν.withDensity (μ.rnDeriv ν))
Equations
• =
instance MeasureTheory.Measure.withDensity.instSigmaFinite {α : Type u_1} {m : } {μ : } {ν : } :
MeasureTheory.SigmaFinite (ν.withDensity (μ.rnDeriv ν))
Equations
• =
instance MeasureTheory.Measure.withDensity.instIsLocallyFiniteMeasure {α : Type u_1} {m : } {μ : } {ν : } [] :
MeasureTheory.IsLocallyFiniteMeasure (ν.withDensity (μ.rnDeriv ν))
Equations
• =
theorem MeasureTheory.Measure.lintegral_rnDeriv_lt_top_of_measure_ne_top {α : Type u_1} {m : } {μ : } (ν : ) {s : Set α} (hs : μ s ) :
∫⁻ (x : α) in s, μ.rnDeriv ν xν <
theorem MeasureTheory.Measure.lintegral_rnDeriv_lt_top {α : Type u_1} {m : } (μ : ) (ν : ) :
∫⁻ (x : α), μ.rnDeriv ν xν <
theorem MeasureTheory.Measure.integrable_toReal_rnDeriv {α : Type u_1} {m : } {μ : } {ν : } :
MeasureTheory.Integrable (fun (x : α) => (μ.rnDeriv ν x).toReal) ν
theorem MeasureTheory.Measure.rnDeriv_lt_top {α : Type u_1} {m : } (μ : ) (ν : ) :
∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x <

The Radon-Nikodym derivative of a sigma-finite measure μ with respect to another measure ν is ν-almost everywhere finite.

theorem MeasureTheory.Measure.rnDeriv_ne_top {α : Type u_1} {m : } (μ : ) (ν : ) :
∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x
theorem MeasureTheory.Measure.eq_singularPart {α : Type u_1} {m : } {μ : } {ν : } {s : } {f : αENNReal} (hf : ) (hs : s.MutuallySingular ν) (hadd : μ = s + ν.withDensity f) :
s = μ.singularPart ν

Given measures μ and ν, if s is a measure mutually singular to ν and f is a measurable function such that μ = s + fν, then s = μ.singularPart μ.

This theorem provides the uniqueness of the singularPart in the Lebesgue decomposition theorem, while MeasureTheory.Measure.eq_rnDeriv provides the uniqueness of the rnDeriv.

theorem MeasureTheory.Measure.singularPart_smul {α : Type u_1} {m : } (μ : ) (ν : ) (r : NNReal) :
(r μ).singularPart ν = r μ.singularPart ν
theorem MeasureTheory.Measure.singularPart_smul_right {α : Type u_1} {m : } (μ : ) (ν : ) (r : NNReal) (hr : r 0) :
μ.singularPart (r ν) = μ.singularPart ν
theorem MeasureTheory.Measure.singularPart_add {α : Type u_1} {m : } (μ₁ : ) (μ₂ : ) (ν : ) [μ₁.HaveLebesgueDecomposition ν] [μ₂.HaveLebesgueDecomposition ν] :
(μ₁ + μ₂).singularPart ν = μ₁.singularPart ν + μ₂.singularPart ν
theorem MeasureTheory.Measure.singularPart_restrict {α : Type u_1} {m : } (μ : ) (ν : ) [μ.HaveLebesgueDecomposition ν] {s : Set α} (hs : ) :
(μ.restrict s).singularPart ν = (μ.singularPart ν).restrict s
theorem MeasureTheory.Measure.eq_withDensity_rnDeriv {α : Type u_1} {m : } {μ : } {ν : } {s : } {f : αENNReal} (hf : ) (hs : s.MutuallySingular ν) (hadd : μ = s + ν.withDensity f) :
ν.withDensity f = ν.withDensity (μ.rnDeriv ν)

Given measures μ and ν, if s is a measure mutually singular to ν and f is a measurable function such that μ = s + fν, then f = μ.rnDeriv ν.

This theorem provides the uniqueness of the rnDeriv in the Lebesgue decomposition theorem, while MeasureTheory.Measure.eq_singularPart provides the uniqueness of the singularPart. Here, the uniqueness is given in terms of the measures, while the uniqueness in terms of the functions is given in eq_rnDeriv.

theorem MeasureTheory.Measure.eq_withDensity_rnDeriv₀ {α : Type u_1} {m : } {μ : } {ν : } {s : } {f : αENNReal} (hf : ) (hs : s.MutuallySingular ν) (hadd : μ = s + ν.withDensity f) :
ν.withDensity f = ν.withDensity (μ.rnDeriv ν)
theorem MeasureTheory.Measure.eq_rnDeriv₀ {α : Type u_1} {m : } {μ : } {ν : } {s : } {f : αENNReal} (hf : ) (hs : s.MutuallySingular ν) (hadd : μ = s + ν.withDensity f) :
f =ᵐ[ν] μ.rnDeriv ν
theorem MeasureTheory.Measure.eq_rnDeriv {α : Type u_1} {m : } {μ : } {ν : } {s : } {f : αENNReal} (hf : ) (hs : s.MutuallySingular ν) (hadd : μ = s + ν.withDensity f) :
f =ᵐ[ν] μ.rnDeriv ν

Given measures μ and ν, if s is a measure mutually singular to ν and f is a measurable function such that μ = s + fν, then f = μ.rnDeriv ν.

This theorem provides the uniqueness of the rnDeriv in the Lebesgue decomposition theorem, while MeasureTheory.Measure.eq_singularPart provides the uniqueness of the singularPart. Here, the uniqueness is given in terms of the functions, while the uniqueness in terms of the functions is given in eq_withDensity_rnDeriv.

theorem MeasureTheory.Measure.rnDeriv_withDensity₀ {α : Type u_1} {m : } (ν : ) {f : αENNReal} (hf : ) :
(ν.withDensity f).rnDeriv ν =ᵐ[ν] f

The Radon-Nikodym derivative of f ν with respect to ν is f.

theorem MeasureTheory.Measure.rnDeriv_withDensity {α : Type u_1} {m : } (ν : ) {f : αENNReal} (hf : ) :
(ν.withDensity f).rnDeriv ν =ᵐ[ν] f

The Radon-Nikodym derivative of f ν with respect to ν is f.

theorem MeasureTheory.Measure.rnDeriv_restrict {α : Type u_1} {m : } (μ : ) (ν : ) [μ.HaveLebesgueDecomposition ν] {s : Set α} (hs : ) :
(μ.restrict s).rnDeriv ν =ᵐ[ν] s.indicator (μ.rnDeriv ν)
theorem MeasureTheory.Measure.rnDeriv_restrict_self {α : Type u_1} {m : } (ν : ) {s : Set α} (hs : ) :
(ν.restrict s).rnDeriv ν =ᵐ[ν] s.indicator 1

The Radon-Nikodym derivative of the restriction of a measure to a measurable set is the indicator function of this set.

theorem MeasureTheory.Measure.rnDeriv_smul_left {α : Type u_1} {m : } (ν : ) (μ : ) [ν.HaveLebesgueDecomposition μ] (r : NNReal) :
(r ν).rnDeriv μ =ᵐ[μ] r ν.rnDeriv μ

Radon-Nikodym derivative of the scalar multiple of a measure. See also rnDeriv_smul_left', which requires sigma-finite ν and μ.

theorem MeasureTheory.Measure.rnDeriv_smul_left_of_ne_top {α : Type u_1} {m : } (ν : ) (μ : ) [ν.HaveLebesgueDecomposition μ] {r : ENNReal} (hr : r ) :
(r ν).rnDeriv μ =ᵐ[μ] r ν.rnDeriv μ

Radon-Nikodym derivative of the scalar multiple of a measure. See also rnDeriv_smul_left_of_ne_top', which requires sigma-finite ν and μ.

theorem MeasureTheory.Measure.rnDeriv_smul_right {α : Type u_1} {m : } (ν : ) (μ : ) [ν.HaveLebesgueDecomposition μ] {r : NNReal} (hr : r 0) :
ν.rnDeriv (r μ) =ᵐ[μ] r⁻¹ ν.rnDeriv μ

Radon-Nikodym derivative with respect to the scalar multiple of a measure. See also rnDeriv_smul_right', which requires sigma-finite ν and μ.

theorem MeasureTheory.Measure.rnDeriv_smul_right_of_ne_top {α : Type u_1} {m : } (ν : ) (μ : ) [ν.HaveLebesgueDecomposition μ] {r : ENNReal} (hr : r 0) (hr_ne_top : r ) :
ν.rnDeriv (r μ) =ᵐ[μ] r⁻¹ ν.rnDeriv μ

Radon-Nikodym derivative with respect to the scalar multiple of a measure. See also rnDeriv_smul_right_of_ne_top', which requires sigma-finite ν and μ.

theorem MeasureTheory.Measure.rnDeriv_add {α : Type u_1} {m : } (ν₁ : ) (ν₂ : ) (μ : ) [ν₁.HaveLebesgueDecomposition μ] [ν₂.HaveLebesgueDecomposition μ] [(ν₁ + ν₂).HaveLebesgueDecomposition μ] :
(ν₁ + ν₂).rnDeriv μ =ᵐ[μ] ν₁.rnDeriv μ + ν₂.rnDeriv μ

theorem MeasureTheory.Measure.exists_positive_of_not_mutuallySingular {α : Type u_1} {m : } (μ : ) (ν : ) (h : ¬μ.MutuallySingular ν) :
∃ (ε : NNReal), 0 < ε ∃ (E : Set α), 0 < ν E MeasureTheory.VectorMeasure.restrict (μ.toSignedMeasure - (ε ν).toSignedMeasure) E

If two finite measures μ and ν are not mutually singular, there exists some ε > 0 and a measurable set E, such that ν(E) > 0 and E is positive with respect to μ - εν.

This lemma is useful for the Lebesgue decomposition theorem.

def MeasureTheory.Measure.LebesgueDecomposition.measurableLE {α : Type u_1} {m : } (μ : ) (ν : ) :
Set (αENNReal)

Given two measures μ and ν, measurableLE μ ν is the set of measurable functions f, such that, for all measurable sets A, ∫⁻ x in A, f x ∂μ ≤ ν A.

This is useful for the Lebesgue decomposition theorem.

Equations
• = {f : αENNReal | ∀ (A : Set α), ∫⁻ (x : α) in A, f xμ ν A}
Instances For
theorem MeasureTheory.Measure.LebesgueDecomposition.sup_mem_measurableLE {α : Type u_1} {m : } {μ : } {ν : } {f : αENNReal} {g : αENNReal} :
(fun (a : α) => f a g a)
theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_succ_eq_sup {α : Sort u_3} (f : αENNReal) (m : ) (a : α) :
⨆ (k : ), ⨆ (_ : k m + 1), f k a = f m.succ a ⨆ (k : ), ⨆ (_ : k m), f k a
theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE {α : Type u_1} {m : } {μ : } {ν : } (f : αENNReal) (hf : ∀ (n : ), ) (n : ) :
(fun (x : α) => ⨆ (k : ), ⨆ (_ : k n), f k x)
theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE' {α : Type u_1} {m : } {μ : } {ν : } (f : αENNReal) (hf : ∀ (n : ), ) (n : ) :
⨆ (k : ), ⨆ (_ : k n), f k
theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone {α : Type u_3} (f : αENNReal) :
Monotone fun (n : ) (x : α) => ⨆ (k : ), ⨆ (_ : k n), f k x
theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone' {α : Type u_3} (f : αENNReal) (x : α) :
Monotone fun (n : ) => ⨆ (k : ), ⨆ (_ : k n), f k x
theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_le_le {α : Type u_3} (f : αENNReal) (n : ) (k : ) (hk : k n) :
f k fun (x : α) => ⨆ (k : ), ⨆ (_ : k n), f k x

measurableLEEval μ ν is the set of ∫⁻ x, f x ∂μ for all f ∈ measurableLE μ ν.

Equations
• = (fun (f : αENNReal) => ∫⁻ (x : α), f xμ) ''
Instances For
theorem MeasureTheory.Measure.haveLebesgueDecomposition_of_finiteMeasure {α : Type u_1} {m : } {μ : } {ν : } :
μ.HaveLebesgueDecomposition ν

Any pair of finite measures μ and ν, HaveLebesgueDecomposition. That is to say, there exist a measure ξ and a measurable function f, such that ξ is mutually singular with respect to ν and μ = ξ + ν.withDensity f.

This is not an instance since this is also shown for the more general σ-finite measures with MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite.

theorem MeasureTheory.Measure.HaveLebesgueDecomposition.sfinite_of_isFiniteMeasure {α : Type u_1} {m : } {μ : } {ν : } (_h : ∀ (μ : ) [inst : ], μ.HaveLebesgueDecomposition ν) :
μ.HaveLebesgueDecomposition ν

If any finite measure has a Lebesgue decomposition with respect to ν, then the same is true for any s-finite measure.

@[instance 100]
instance MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite {α : Type u_1} {m : } (μ : ) (ν : ) :
μ.HaveLebesgueDecomposition ν

The Lebesgue decomposition theorem: Any s-finite measure μ has Lebesgue decomposition with respect to any σ-finite measure ν. That is to say, there exist a measure ξ and a measurable function f, such that ξ is mutually singular with respect to ν and μ = ξ + ν.withDensity f

Equations
• =
theorem MeasureTheory.Measure.rnDeriv_smul_left' {α : Type u_1} {m : } (ν : ) (μ : ) (r : NNReal) :
(r ν).rnDeriv μ =ᵐ[μ] r ν.rnDeriv μ

Radon-Nikodym derivative of the scalar multiple of a measure. See also rnDeriv_smul_left, which has no hypothesis on μ but requires finite ν.

theorem MeasureTheory.Measure.rnDeriv_smul_left_of_ne_top' {α : Type u_1} {m : } (ν : ) (μ : ) {r : ENNReal} (hr : r ) :
(r ν).rnDeriv μ =ᵐ[μ] r ν.rnDeriv μ

Radon-Nikodym derivative of the scalar multiple of a measure. See also rnDeriv_smul_left_of_ne_top, which has no hypothesis on μ but requires finite ν.

theorem MeasureTheory.Measure.rnDeriv_smul_right' {α : Type u_1} {m : } (ν : ) (μ : ) {r : NNReal} (hr : r 0) :
ν.rnDeriv (r μ) =ᵐ[μ] r⁻¹ ν.rnDeriv μ

Radon-Nikodym derivative with respect to the scalar multiple of a measure. See also rnDeriv_smul_right, which has no hypothesis on μ but requires finite ν.

theorem MeasureTheory.Measure.rnDeriv_smul_right_of_ne_top' {α : Type u_1} {m : } (ν : ) (μ : ) {r : ENNReal} (hr : r 0) (hr_ne_top : r ) :
ν.rnDeriv (r μ) =ᵐ[μ] r⁻¹ ν.rnDeriv μ

Radon-Nikodym derivative with respect to the scalar multiple of a measure. See also rnDeriv_smul_right_of_ne_top, which has no hypothesis on μ but requires finite ν.

theorem MeasureTheory.Measure.rnDeriv_add' {α : Type u_1} {m : } (ν₁ : ) (ν₂ : ) (μ : ) :
(ν₁ + ν₂).rnDeriv μ =ᵐ[μ] ν₁.rnDeriv μ + ν₂.rnDeriv μ

Radon-Nikodym derivative of a sum of two measures. See also rnDeriv_add, which has no hypothesis on μ but requires finite ν₁ and ν₂.

theorem MeasureTheory.Measure.rnDeriv_add_of_mutuallySingular {α : Type u_1} {m : } (ν₁ : ) (ν₂ : ) (μ : ) (h : ν₂.MutuallySingular μ) :
(ν₁ + ν₂).rnDeriv μ =ᵐ[μ] ν₁.rnDeriv μ