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 ν.

The Lebesgue decomposition provides the Radon-Nikodym theorem readily.

Main definitions

• MeasureTheory.Measure.HaveLebesgueDecomposition : A pair of measures μ and ν is said to HaveLebesgueDecomposition if there exist a measure ξ and a measurable function f, such that ξ is mutually singular with respect to ν and μ = ξ + ν.withDensity f
• MeasureTheory.Measure.singularPart : If a pair of measures HaveLebesgueDecomposition, then singularPart chooses the measure from HaveLebesgueDecomposition, otherwise it returns the zero measure.
• MeasureTheory.Measure.rnDeriv: If a pair of measures HaveLebesgueDecomposition, then rnDeriv chooses the measurable function from HaveLebesgueDecomposition, otherwise it returns the zero function.

Main results

• MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite : the Lebesgue decomposition theorem.
• MeasureTheory.Measure.eq_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 ν.
• MeasureTheory.Measure.eq_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 ν.

Tags

Lebesgue decomposition theorem

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

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.

• lebesgue_decomposition : ∃ (p : Measure α × (α → ENNReal)), Measurable p.2 ∧ p.1.MutuallySingular ν ∧ μ = p.1 + ν.withDensity p.2

@[irreducible]

noncomputable def MeasureTheory.Measure.singularPart {α : Type u_2} {m : MeasurableSpace α} (μ ν : Measure α) : Measure α

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

• μ.singularPart ν = if h : μ.HaveLebesgueDecomposition ν then (Classical.choose ⋯).1 else 0

theorem MeasureTheory.Measure.singularPart_def {α : Type u_2} {m : MeasurableSpace α} (μ ν : Measure α) : μ.singularPart ν = if h : μ.HaveLebesgueDecomposition ν then (Classical.choose ⋯).1 else 0

@[irreducible]

noncomputable def MeasureTheory.Measure.rnDeriv {α : Type u_2} {m : MeasurableSpace α} (μ ν : Measure α) : α → 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

• μ.rnDeriv ν = if h : μ.HaveLebesgueDecomposition ν then (Classical.choose ⋯).2 else 0

theorem MeasureTheory.Measure.rnDeriv_def {α : Type u_2} {m : MeasurableSpace α} (μ ν : Measure α) : μ.rnDeriv ν = if h : μ.HaveLebesgueDecomposition ν then (Classical.choose ⋯).2 else 0

theorem MeasureTheory.Measure.haveLebesgueDecomposition_spec {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) [h : μ.HaveLebesgueDecomposition ν] : Measurable (μ.rnDeriv ν) ∧ (μ.singularPart ν).MutuallySingular ν ∧ μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)

theorem MeasureTheory.Measure.rnDeriv_of_not_haveLebesgueDecomposition {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} (h : ¬μ.HaveLebesgueDecomposition ν) : μ.rnDeriv ν = 0

theorem MeasureTheory.Measure.singularPart_of_not_haveLebesgueDecomposition {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} (h : ¬μ.HaveLebesgueDecomposition ν) : μ.singularPart ν = 0

theorem MeasureTheory.Measure.measurable_rnDeriv {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) : Measurable (μ.rnDeriv ν)

theorem MeasureTheory.Measure.mutuallySingular_singularPart {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) : (μ.singularPart ν).MutuallySingular ν

theorem MeasureTheory.Measure.MutuallySingular.haveLebesgueDecomposition {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} (h : μ.MutuallySingular ν) : μ.HaveLebesgueDecomposition ν

theorem MeasureTheory.Measure.haveLebesgueDecomposition_add {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) [μ.HaveLebesgueDecomposition ν] : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)

theorem MeasureTheory.Measure.singularPart_add_rnDeriv {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) [μ.HaveLebesgueDecomposition ν] : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = μ

For the versions of this lemma where ν.withDensity (μ.rnDeriv ν) or μ.singularPart ν are isolated, see MeasureTheory.Measure.measure_sub_singularPart and MeasureTheory.Measure.measure_sub_rnDeriv.

theorem MeasureTheory.Measure.rnDeriv_add_singularPart {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) [μ.HaveLebesgueDecomposition ν] : ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν = μ

For the versions of this lemma where μ.singularPart ν or ν.withDensity (μ.rnDeriv ν) are isolated, see MeasureTheory.Measure.measure_sub_singularPart and MeasureTheory.Measure.measure_sub_rnDeriv.

instance MeasureTheory.Measure.instHaveLebesgueDecompositionZeroLeft {α : Type u_1} {m : MeasurableSpace α} {ν : Measure α} : HaveLebesgueDecomposition 0 ν

instance MeasureTheory.Measure.instHaveLebesgueDecompositionZeroRight {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} : μ.HaveLebesgueDecomposition 0

instance MeasureTheory.Measure.instHaveLebesgueDecompositionSelf {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} : μ.HaveLebesgueDecomposition μ

instance MeasureTheory.Measure.HaveLebesgueDecomposition.sum_left {α : Type u_1} {m : MeasurableSpace α} {ν : Measure α} {ι : Type u_2} [Countable ι] (μ : ι → Measure α) [∀ (i : ι), (μ i).HaveLebesgueDecomposition ν] : (sum μ).HaveLebesgueDecomposition ν

instance MeasureTheory.Measure.HaveLebesgueDecomposition.add_left {α : Type u_1} {m : MeasurableSpace α} {μ ν μ' : Measure α} [μ.HaveLebesgueDecomposition ν] [μ'.HaveLebesgueDecomposition ν] : (μ + μ').HaveLebesgueDecomposition ν

instance MeasureTheory.Measure.haveLebesgueDecompositionSMul' {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) [μ.HaveLebesgueDecomposition ν] (r : ENNReal) : (r • μ).HaveLebesgueDecomposition ν

instance MeasureTheory.Measure.haveLebesgueDecompositionSMul {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) [μ.HaveLebesgueDecomposition ν] (r : NNReal) : (r • μ).HaveLebesgueDecomposition ν

instance MeasureTheory.Measure.haveLebesgueDecompositionSMulRight {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) [μ.HaveLebesgueDecomposition ν] (r : NNReal) : μ.HaveLebesgueDecomposition (r • ν)

theorem MeasureTheory.Measure.haveLebesgueDecomposition_withDensity {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) {f : α → ENNReal} (hf : Measurable f) : (μ.withDensity f).HaveLebesgueDecomposition μ

instance MeasureTheory.Measure.haveLebesgueDecompositionRnDeriv {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) : (ν.withDensity (μ.rnDeriv ν)).HaveLebesgueDecomposition ν

instance MeasureTheory.Measure.instHaveLebesgueDecompositionSingularPart {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} : (μ.singularPart ν).HaveLebesgueDecomposition ν

theorem MeasureTheory.Measure.singularPart_le {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) : μ.singularPart ν ≤ μ

theorem MeasureTheory.Measure.withDensity_rnDeriv_le {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) : ν.withDensity (μ.rnDeriv ν) ≤ μ

theorem AEMeasurable.singularPart {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_2} {x✝ : MeasurableSpace β} {f : α → β} (hf : AEMeasurable f μ) (ν : MeasureTheory.Measure α) : AEMeasurable f (μ.singularPart ν)

theorem AEMeasurable.withDensity_rnDeriv {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_2} {x✝ : MeasurableSpace β} {f : α → β} (hf : AEMeasurable f μ) (ν : MeasureTheory.Measure α) : AEMeasurable f (ν.withDensity (μ.rnDeriv ν))

theorem MeasureTheory.Measure.MutuallySingular.singularPart {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} (h : μ.MutuallySingular ν) (ν' : Measure α) : (μ.singularPart ν').MutuallySingular ν

theorem MeasureTheory.Measure.absolutelyContinuous_withDensity_rnDeriv {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} [ν.HaveLebesgueDecomposition μ] (hμν : μ.AbsolutelyContinuous ν) : μ.AbsolutelyContinuous (μ.withDensity (ν.rnDeriv μ))

theorem MeasureTheory.Measure.AbsolutelyContinuous.withDensity_rnDeriv {α : Type u_1} {m : MeasurableSpace α} {μ ν ξ : Measure α} [μ.HaveLebesgueDecomposition ν] (hξμ : ξ.AbsolutelyContinuous μ) (hξν : ξ.AbsolutelyContinuous ν) : ξ.AbsolutelyContinuous (ν.withDensity (μ.rnDeriv ν))

theorem MeasureTheory.Measure.absolutelyContinuous_withDensity_rnDeriv_swap {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} [ν.HaveLebesgueDecomposition μ] : (ν.withDensity (μ.rnDeriv ν)).AbsolutelyContinuous (μ.withDensity (ν.rnDeriv μ))

theorem MeasureTheory.Measure.singularPart_eq_zero_of_ac {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} (h : μ.AbsolutelyContinuous ν) : μ.singularPart ν = 0

@[simp]

theorem MeasureTheory.Measure.singularPart_zero {α : Type u_1} {m : MeasurableSpace α} (ν : Measure α) : singularPart 0 ν = 0

@[simp]

theorem MeasureTheory.Measure.singularPart_zero_right {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) : μ.singularPart 0 = μ

theorem MeasureTheory.Measure.singularPart_eq_zero {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) [μ.HaveLebesgueDecomposition ν] : μ.singularPart ν = 0 ↔ μ.AbsolutelyContinuous ν

@[simp]

theorem MeasureTheory.Measure.withDensity_rnDeriv_eq_zero {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) [μ.HaveLebesgueDecomposition ν] : ν.withDensity (μ.rnDeriv ν) = 0 ↔ μ.MutuallySingular ν

@[simp]

theorem MeasureTheory.Measure.rnDeriv_eq_zero {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) [μ.HaveLebesgueDecomposition ν] : μ.rnDeriv ν =ᶠ[ae ν] 0 ↔ μ.MutuallySingular ν

theorem MeasureTheory.Measure.rnDeriv_zero {α : Type u_1} {m : MeasurableSpace α} (ν : Measure α) : rnDeriv 0 ν =ᶠ[ae ν] 0

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

@[simp]

theorem MeasureTheory.Measure.singularPart_withDensity {α : Type u_1} {m : MeasurableSpace α} (ν : Measure α) (f : α → ENNReal) : (ν.withDensity f).singularPart ν = 0

theorem MeasureTheory.Measure.rnDeriv_singularPart {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) : (μ.singularPart ν).rnDeriv ν =ᶠ[ae ν] 0

@[simp]

theorem MeasureTheory.Measure.singularPart_self {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) : μ.singularPart μ = 0

theorem MeasureTheory.Measure.rnDeriv_self {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) [SigmaFinite μ] : μ.rnDeriv μ =ᶠ[ae μ] fun (x : α) => 1

theorem MeasureTheory.Measure.singularPart_eq_self {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} : μ.singularPart ν = μ ↔ μ.MutuallySingular ν

@[simp]

theorem MeasureTheory.Measure.singularPart_singularPart {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) : (μ.singularPart ν).singularPart ν = μ.singularPart ν

instance MeasureTheory.Measure.singularPart.instIsFiniteMeasure {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} [IsFiniteMeasure μ] : IsFiniteMeasure (μ.singularPart ν)

instance MeasureTheory.Measure.singularPart.instSigmaFinite {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} [SigmaFinite μ] : SigmaFinite (μ.singularPart ν)

instance MeasureTheory.Measure.singularPart.instIsLocallyFiniteMeasure {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} [TopologicalSpace α] [IsLocallyFiniteMeasure μ] : IsLocallyFiniteMeasure (μ.singularPart ν)

instance MeasureTheory.Measure.withDensity.instIsFiniteMeasure {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} [IsFiniteMeasure μ] : IsFiniteMeasure (ν.withDensity (μ.rnDeriv ν))

instance MeasureTheory.Measure.withDensity.instSigmaFinite {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} [SigmaFinite μ] : SigmaFinite (ν.withDensity (μ.rnDeriv ν))

instance MeasureTheory.Measure.withDensity.instIsLocallyFiniteMeasure {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} [TopologicalSpace α] [IsLocallyFiniteMeasure μ] : IsLocallyFiniteMeasure (ν.withDensity (μ.rnDeriv ν))

theorem MeasureTheory.Measure.lintegral_rnDeriv_lt_top_of_measure_ne_top {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (ν : Measure α) {s : Set α} (hs : μ s ≠ ⊤) : ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν < ⊤

theorem MeasureTheory.Measure.lintegral_rnDeriv_lt_top {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) [IsFiniteMeasure μ] : ∫⁻ (x : α), μ.rnDeriv ν x ∂ν < ⊤

theorem MeasureTheory.Measure.rnDeriv_lt_top {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) [SigmaFinite μ] : ∀ᵐ (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 : MeasurableSpace α} (μ ν : Measure α) [SigmaFinite μ] : ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ ⊤

theorem MeasureTheory.Measure.eq_singularPart {α : Type u_1} {m : MeasurableSpace α} {μ ν s : Measure α} {f : α → ENNReal} (hf : Measurable f) (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 : MeasurableSpace α} (μ ν : Measure α) (r : NNReal) : (r • μ).singularPart ν = r • μ.singularPart ν

theorem MeasureTheory.Measure.singularPart_smul_right {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) (r : NNReal) (hr : r ≠ 0) : μ.singularPart (r • ν) = μ.singularPart ν

theorem MeasureTheory.Measure.singularPart_add {α : Type u_1} {m : MeasurableSpace α} (μ₁ μ₂ ν : Measure α) [μ₁.HaveLebesgueDecomposition ν] [μ₂.HaveLebesgueDecomposition ν] : (μ₁ + μ₂).singularPart ν = μ₁.singularPart ν + μ₂.singularPart ν

theorem MeasureTheory.Measure.singularPart_restrict {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) [μ.HaveLebesgueDecomposition ν] {s : Set α} (hs : MeasurableSet s) : (μ.restrict s).singularPart ν = (μ.singularPart ν).restrict s

theorem MeasureTheory.Measure.singularPart_eq_restrict' {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} {s : Set α} [μ.HaveLebesgueDecomposition ν] (hμs : (μ.singularPart ν) sᶜ = 0) (hνs : (ν.withDensity (μ.rnDeriv ν)) s = 0) : μ.singularPart ν = μ.restrict s

If a set s separates the absolutely continuous part of μ with respect to ν from the singular part, then the singular part equals the restriction of μ to s.

theorem MeasureTheory.Measure.singularPart_eq_restrict {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} {s : Set α} [μ.HaveLebesgueDecomposition ν] (hμs : (μ.singularPart ν) sᶜ = 0) (hνs : ν s = 0) : μ.singularPart ν = μ.restrict s

If a set s separates ν from the singular part of μ with respect to ν, then the singular part equals the restriction of μ to s.

theorem MeasureTheory.Measure.measure_sub_singularPart {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) [μ.HaveLebesgueDecomposition ν] [IsFiniteMeasure μ] : μ - μ.singularPart ν = ν.withDensity (μ.rnDeriv ν)

theorem MeasureTheory.Measure.measure_sub_rnDeriv {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) [μ.HaveLebesgueDecomposition ν] [IsFiniteMeasure μ] : μ - ν.withDensity (μ.rnDeriv ν) = μ.singularPart ν

theorem MeasureTheory.Measure.eq_withDensity_rnDeriv {α : Type u_1} {m : MeasurableSpace α} {μ ν s : Measure α} {f : α → ENNReal} (hf : Measurable f) (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 : MeasurableSpace α} {μ ν s : Measure α} {f : α → ENNReal} (hf : AEMeasurable f ν) (hs : s.MutuallySingular ν) (hadd : μ = s + ν.withDensity f) : ν.withDensity f = ν.withDensity (μ.rnDeriv ν)

theorem MeasureTheory.Measure.eq_rnDeriv₀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} [SigmaFinite ν] {s : Measure α} {f : α → ENNReal} (hf : AEMeasurable f ν) (hs : s.MutuallySingular ν) (hadd : μ = s + ν.withDensity f) : f =ᶠ[ae ν] μ.rnDeriv ν

theorem MeasureTheory.Measure.eq_rnDeriv {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} [SigmaFinite ν] {s : Measure α} {f : α → ENNReal} (hf : Measurable f) (hs : s.MutuallySingular ν) (hadd : μ = s + ν.withDensity f) : f =ᶠ[ae ν] μ.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 : MeasurableSpace α} (ν : Measure α) [SigmaFinite ν] {f : α → ENNReal} (hf : AEMeasurable f ν) : (ν.withDensity f).rnDeriv ν =ᶠ[ae ν] f

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

theorem MeasureTheory.Measure.rnDeriv_withDensity {α : Type u_1} {m : MeasurableSpace α} (ν : Measure α) [SigmaFinite ν] {f : α → ENNReal} (hf : Measurable f) : (ν.withDensity f).rnDeriv ν =ᶠ[ae ν] f

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

theorem MeasureTheory.Measure.rnDeriv_restrict {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) [μ.HaveLebesgueDecomposition ν] [SigmaFinite ν] {s : Set α} (hs : MeasurableSet s) : (μ.restrict s).rnDeriv ν =ᶠ[ae ν] s.indicator (μ.rnDeriv ν)

theorem MeasureTheory.Measure.rnDeriv_restrict_self {α : Type u_1} {m : MeasurableSpace α} (ν : Measure α) [SigmaFinite ν] {s : Set α} (hs : MeasurableSet s) : (ν.restrict s).rnDeriv ν =ᶠ[ae ν] 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 : MeasurableSpace α} (ν μ : Measure α) [IsFiniteMeasure ν] [ν.HaveLebesgueDecomposition μ] (r : NNReal) : (r • ν).rnDeriv μ =ᶠ[ae μ] 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 : MeasurableSpace α} (ν μ : Measure α) [IsFiniteMeasure ν] [ν.HaveLebesgueDecomposition μ] {r : ENNReal} (hr : r ≠ ⊤) : (r • ν).rnDeriv μ =ᶠ[ae μ] 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 : MeasurableSpace α} (ν μ : Measure α) [IsFiniteMeasure ν] [ν.HaveLebesgueDecomposition μ] {r : NNReal} (hr : r ≠ 0) : ν.rnDeriv (r • μ) =ᶠ[ae μ] 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 : MeasurableSpace α} (ν μ : Measure α) [IsFiniteMeasure ν] [ν.HaveLebesgueDecomposition μ] {r : ENNReal} (hr : r ≠ 0) (hr_ne_top : r ≠ ⊤) : ν.rnDeriv (r • μ) =ᶠ[ae μ] 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 : MeasurableSpace α} (ν₁ ν₂ μ : Measure α) [IsFiniteMeasure ν₁] [IsFiniteMeasure ν₂] [ν₁.HaveLebesgueDecomposition μ] [ν₂.HaveLebesgueDecomposition μ] [(ν₁ + ν₂).HaveLebesgueDecomposition μ] : (ν₁ + ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ + ν₂.rnDeriv μ

Radon-Nikodym derivative of a sum of two measures. See also rnDeriv_add', which requires sigma-finite ν₁, ν₂ and μ.

theorem MeasureTheory.Measure.exists_positive_of_not_mutuallySingular {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h : ¬μ.MutuallySingular ν) : ∃ (ε : NNReal), 0 < ε ∧ ∃ (E : Set α), MeasurableSet E ∧ 0 < ν E ∧ ∀ (A : Set α), MeasurableSet A → ↑ε * ν (A ∩ E) ≤ μ (A ∩ 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 : MeasurableSpace α} (μ ν : Measure α) : 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

• MeasureTheory.Measure.LebesgueDecomposition.measurableLE μ ν = {f : α → ENNReal | Measurable f ∧ ∀ (A : Set α), MeasurableSet A → ∫⁻ (x : α) in A, f x ∂μ ≤ ν A}

theorem MeasureTheory.Measure.LebesgueDecomposition.zero_mem_measurableLE {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} : 0 ∈ measurableLE μ ν

theorem MeasureTheory.Measure.LebesgueDecomposition.sup_mem_measurableLE {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} {f g : α → ENNReal} (hf : f ∈ measurableLE μ ν) (hg : g ∈ measurableLE μ ν) : (fun (a : α) => max (f a) (g a)) ∈ measurableLE μ ν

theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_succ_eq_sup {α : Sort u_2} (f : ℕ → α → ENNReal) (m : ℕ) (a : α) : ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)

theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} (f : ℕ → α → ENNReal) (hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν) (n : ℕ) : (fun (x : α) => ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k x) ∈ measurableLE μ ν

theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE' {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} (f : ℕ → α → ENNReal) (hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν) (n : ℕ) : ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k ∈ measurableLE μ ν

theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone {α : Type u_2} (f : ℕ → α → ENNReal) : Monotone fun (n : ℕ) (x : α) => ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k x

theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone' {α : Type u_2} (f : ℕ → α → ENNReal) (x : α) : Monotone fun (n : ℕ) => ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k x

theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_le_le {α : Type u_2} (f : ℕ → α → ENNReal) (n k : ℕ) (hk : k ≤ n) : f k ≤ fun (x : α) => ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k x

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

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

Equations

• MeasureTheory.Measure.LebesgueDecomposition.measurableLEEval μ ν = (fun (f : α → ENNReal) => ∫⁻ (x : α), f x ∂μ) '' MeasureTheory.Measure.LebesgueDecomposition.measurableLE μ ν

theorem MeasureTheory.Measure.haveLebesgueDecomposition_of_finiteMeasure {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} [IsFiniteMeasure μ] [IsFiniteMeasure ν] : μ.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 : MeasurableSpace α} {μ ν : Measure α} [SFinite μ] (_h : ∀ (μ : Measure α) [IsFiniteMeasure μ], μ.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 : MeasurableSpace α} (μ ν : Measure α) [SFinite μ] [SigmaFinite ν] : μ.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

theorem MeasureTheory.Measure.rnDeriv_smul_left' {α : Type u_1} {m : MeasurableSpace α} (ν μ : Measure α) [SigmaFinite ν] [SigmaFinite μ] (r : NNReal) : (r • ν).rnDeriv μ =ᶠ[ae μ] 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 : MeasurableSpace α} (ν μ : Measure α) [SigmaFinite ν] [SigmaFinite μ] {r : ENNReal} (hr : r ≠ ⊤) : (r • ν).rnDeriv μ =ᶠ[ae μ] 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 : MeasurableSpace α} (ν μ : Measure α) [SigmaFinite ν] [SigmaFinite μ] {r : NNReal} (hr : r ≠ 0) : ν.rnDeriv (r • μ) =ᶠ[ae μ] 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 : MeasurableSpace α} (ν μ : Measure α) [SigmaFinite ν] [SigmaFinite μ] {r : ENNReal} (hr : r ≠ 0) (hr_ne_top : r ≠ ⊤) : ν.rnDeriv (r • μ) =ᶠ[ae μ] 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 : MeasurableSpace α} (ν₁ ν₂ μ : Measure α) [SigmaFinite ν₁] [SigmaFinite ν₂] [SigmaFinite μ] : (ν₁ + ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.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 : MeasurableSpace α} (ν₁ ν₂ μ : Measure α) [SigmaFinite ν₁] [SigmaFinite ν₂] [SigmaFinite μ] (h : ν₂.MutuallySingular μ) : (ν₁ + ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ