Lebesgue decomposition

This file proves the Lebesgue decomposition theorem for signed measures. 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 ν.

Main definitions

• MeasureTheory.SignedMeasure.HaveLebesgueDecomposition : A signed measure s and a measure μ is said to HaveLebesgueDecomposition if both the positive part and negative part of s HaveLebesgueDecomposition with respect to μ.
• MeasureTheory.SignedMeasure.singularPart : The singular part between a signed measure s and a measure μ is simply the singular part of the positive part of s with respect to μ minus the singular part of the negative part of s with respect to μ.
• MeasureTheory.SignedMeasure.rnDeriv : The Radon-Nikodym derivative of a signed measure s with respect to a measure μ is the Radon-Nikodym derivative of the positive part of s with respect to μ minus the Radon-Nikodym derivative of the negative part of s with respect to μ.

Main results

• MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eq : the Lebesgue decomposition theorem between a signed measure and a σ-finite positive measure.

Tags

Lebesgue decomposition theorem

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

A signed measure s is said to HaveLebesgueDecomposition with respect to a measure μ if the positive part and the negative part of s both HaveLebesgueDecomposition with respect to μ.

• posPart : MeasureTheory.Measure.HaveLebesgueDecomposition (MeasureTheory.SignedMeasure.toJordanDecomposition s).posPart μ
• negPart : MeasureTheory.Measure.HaveLebesgueDecomposition (MeasureTheory.SignedMeasure.toJordanDecomposition s).negPart μ

theorem MeasureTheory.SignedMeasure.not_haveLebesgueDecomposition_iff {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) : ¬MeasureTheory.SignedMeasure.HaveLebesgueDecomposition s μ ↔ ¬MeasureTheory.Measure.HaveLebesgueDecomposition (MeasureTheory.SignedMeasure.toJordanDecomposition s).posPart μ ∨ ¬MeasureTheory.Measure.HaveLebesgueDecomposition (MeasureTheory.SignedMeasure.toJordanDecomposition s).negPart μ

instance MeasureTheory.SignedMeasure.haveLebesgueDecomposition_of_sigmaFinite {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : MeasureTheory.SignedMeasure.HaveLebesgueDecomposition s μ

Equations

• ⋯ = ⋯

instance MeasureTheory.SignedMeasure.haveLebesgueDecomposition_neg {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) [MeasureTheory.SignedMeasure.HaveLebesgueDecomposition s μ] : MeasureTheory.SignedMeasure.HaveLebesgueDecomposition (-s) μ

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance MeasureTheory.SignedMeasure.haveLebesgueDecomposition_smul_real {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) [MeasureTheory.SignedMeasure.HaveLebesgueDecomposition s μ] (r : ℝ) : MeasureTheory.SignedMeasure.HaveLebesgueDecomposition (r • s) μ

Equations

• ⋯ = ⋯

def MeasureTheory.SignedMeasure.singularPart {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) : MeasureTheory.SignedMeasure α

Given a signed measure s and a measure μ, s.singularPart μ is the signed measure such that s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) = s and s.singularPart μ is mutually singular with respect to μ.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.SignedMeasure.singularPart_mutuallySingular {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) : MeasureTheory.Measure.MutuallySingular ((MeasureTheory.SignedMeasure.toJordanDecomposition s).posPart.singularPart μ) ((MeasureTheory.SignedMeasure.toJordanDecomposition s).negPart.singularPart μ)

theorem MeasureTheory.SignedMeasure.singularPart_totalVariation {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) : MeasureTheory.SignedMeasure.totalVariation (MeasureTheory.SignedMeasure.singularPart s μ) = (MeasureTheory.SignedMeasure.toJordanDecomposition s).posPart.singularPart μ + (MeasureTheory.SignedMeasure.toJordanDecomposition s).negPart.singularPart μ

theorem MeasureTheory.SignedMeasure.mutuallySingular_singularPart {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) : MeasureTheory.VectorMeasure.MutuallySingular (MeasureTheory.SignedMeasure.singularPart s μ) (MeasureTheory.Measure.toENNRealVectorMeasure μ)

def MeasureTheory.SignedMeasure.rnDeriv {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) : α → ℝ

The Radon-Nikodym derivative between a signed measure and a positive measure.

rnDeriv s μ satisfies μ.withDensityᵥ (s.rnDeriv μ) = s if and only if s is absolutely continuous with respect to μ and this fact is known as MeasureTheory.SignedMeasure.absolutelyContinuous_iff_withDensity_rnDeriv_eq and can be found in MeasureTheory.Decomposition.RadonNikodym.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.SignedMeasure.rnDeriv_def {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) : MeasureTheory.SignedMeasure.rnDeriv s μ = fun (x : α) => ((MeasureTheory.SignedMeasure.toJordanDecomposition s).posPart.rnDeriv μ x).toReal - ((MeasureTheory.SignedMeasure.toJordanDecomposition s).negPart.rnDeriv μ x).toReal

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

theorem MeasureTheory.SignedMeasure.integrable_rnDeriv {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) : MeasureTheory.Integrable (MeasureTheory.SignedMeasure.rnDeriv s μ) μ

theorem MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eq {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : MeasureTheory.SignedMeasure α) [MeasureTheory.SignedMeasure.HaveLebesgueDecomposition s μ] : MeasureTheory.SignedMeasure.singularPart s μ + MeasureTheory.Measure.withDensityᵥ μ (MeasureTheory.SignedMeasure.rnDeriv s μ) = s

The Lebesgue Decomposition theorem between a signed measure and a measure: Given a signed measure s and a σ-finite measure μ, there exist a signed measure t and a measurable and integrable function f, such that t is mutually singular with respect to μ and s = t + μ.withDensityᵥ f. In this case t = s.singularPart μ and f = s.rnDeriv μ.

theorem MeasureTheory.SignedMeasure.jordanDecomposition_add_withDensity_mutuallySingular {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : MeasureTheory.SignedMeasure α} {f : α → ℝ} (hf : Measurable f) (htμ : MeasureTheory.VectorMeasure.MutuallySingular t (MeasureTheory.Measure.toENNRealVectorMeasure μ)) : MeasureTheory.Measure.MutuallySingular ((MeasureTheory.SignedMeasure.toJordanDecomposition t).posPart + μ.withDensity fun (x : α) => ENNReal.ofReal (f x)) ((MeasureTheory.SignedMeasure.toJordanDecomposition t).negPart + μ.withDensity fun (x : α) => ENNReal.ofReal (-f x))

theorem MeasureTheory.SignedMeasure.toJordanDecomposition_eq_of_eq_add_withDensity {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : MeasureTheory.SignedMeasure α} {t : MeasureTheory.SignedMeasure α} {f : α → ℝ} (hf : Measurable f) (hfi : MeasureTheory.Integrable f μ) (htμ : MeasureTheory.VectorMeasure.MutuallySingular t (MeasureTheory.Measure.toENNRealVectorMeasure μ)) (hadd : s = t + MeasureTheory.Measure.withDensityᵥ μ f) : MeasureTheory.SignedMeasure.toJordanDecomposition s = MeasureTheory.JordanDecomposition.mk ((MeasureTheory.SignedMeasure.toJordanDecomposition t).posPart + μ.withDensity fun (x : α) => ENNReal.ofReal (f x)) ((MeasureTheory.SignedMeasure.toJordanDecomposition t).negPart + μ.withDensity fun (x : α) => ENNReal.ofReal (-f x)) ⋯

theorem MeasureTheory.SignedMeasure.haveLebesgueDecomposition_mk {α : Type u_1} {m : MeasurableSpace α} {s : MeasureTheory.SignedMeasure α} {t : MeasureTheory.SignedMeasure α} (μ : MeasureTheory.Measure α) {f : α → ℝ} (hf : Measurable f) (htμ : MeasureTheory.VectorMeasure.MutuallySingular t (MeasureTheory.Measure.toENNRealVectorMeasure μ)) (hadd : s = t + MeasureTheory.Measure.withDensityᵥ μ f) : MeasureTheory.SignedMeasure.HaveLebesgueDecomposition s μ

theorem MeasureTheory.SignedMeasure.eq_singularPart {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : MeasureTheory.SignedMeasure α} (t : MeasureTheory.SignedMeasure α) (f : α → ℝ) (htμ : MeasureTheory.VectorMeasure.MutuallySingular t (MeasureTheory.Measure.toENNRealVectorMeasure μ)) (hadd : s = t + MeasureTheory.Measure.withDensityᵥ μ f) : t = MeasureTheory.SignedMeasure.singularPart s μ

Given a measure μ, signed measures s and t, and a function f such that t is mutually singular with respect to μ and s = t + μ.withDensityᵥ f, we have t = singularPart s μ, i.e. t is the singular part of the Lebesgue decomposition between s and μ.

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

theorem MeasureTheory.SignedMeasure.singularPart_neg {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) : MeasureTheory.SignedMeasure.singularPart (-s) μ = -MeasureTheory.SignedMeasure.singularPart s μ

theorem MeasureTheory.SignedMeasure.singularPart_smul_nnreal {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) (r : NNReal) : MeasureTheory.SignedMeasure.singularPart (r • s) μ = r • MeasureTheory.SignedMeasure.singularPart s μ

theorem MeasureTheory.SignedMeasure.singularPart_smul {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) (r : ℝ) : MeasureTheory.SignedMeasure.singularPart (r • s) μ = r • MeasureTheory.SignedMeasure.singularPart s μ

theorem MeasureTheory.SignedMeasure.singularPart_add {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (t : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) [MeasureTheory.SignedMeasure.HaveLebesgueDecomposition s μ] [MeasureTheory.SignedMeasure.HaveLebesgueDecomposition t μ] : MeasureTheory.SignedMeasure.singularPart (s + t) μ = MeasureTheory.SignedMeasure.singularPart s μ + MeasureTheory.SignedMeasure.singularPart t μ

theorem MeasureTheory.SignedMeasure.singularPart_sub {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (t : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) [MeasureTheory.SignedMeasure.HaveLebesgueDecomposition s μ] [MeasureTheory.SignedMeasure.HaveLebesgueDecomposition t μ] : MeasureTheory.SignedMeasure.singularPart (s - t) μ = MeasureTheory.SignedMeasure.singularPart s μ - MeasureTheory.SignedMeasure.singularPart t μ

theorem MeasureTheory.SignedMeasure.eq_rnDeriv {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : MeasureTheory.SignedMeasure α} (t : MeasureTheory.SignedMeasure α) (f : α → ℝ) (hfi : MeasureTheory.Integrable f μ) (htμ : MeasureTheory.VectorMeasure.MutuallySingular t (MeasureTheory.Measure.toENNRealVectorMeasure μ)) (hadd : s = t + MeasureTheory.Measure.withDensityᵥ μ f) : f =ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.SignedMeasure.rnDeriv s μ

Given a measure μ, signed measures s and t, and a function f such that t is mutually singular with respect to μ and s = t + μ.withDensityᵥ f, we have f = rnDeriv s μ, i.e. f is the Radon-Nikodym derivative of s and μ.

theorem MeasureTheory.SignedMeasure.rnDeriv_neg {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) [MeasureTheory.SignedMeasure.HaveLebesgueDecomposition s μ] : MeasureTheory.SignedMeasure.rnDeriv (-s) μ =ᶠ[MeasureTheory.Measure.ae μ] -MeasureTheory.SignedMeasure.rnDeriv s μ

theorem MeasureTheory.SignedMeasure.rnDeriv_smul {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) [MeasureTheory.SignedMeasure.HaveLebesgueDecomposition s μ] (r : ℝ) : MeasureTheory.SignedMeasure.rnDeriv (r • s) μ =ᶠ[MeasureTheory.Measure.ae μ] r • MeasureTheory.SignedMeasure.rnDeriv s μ

theorem MeasureTheory.SignedMeasure.rnDeriv_add {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (t : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) [MeasureTheory.SignedMeasure.HaveLebesgueDecomposition s μ] [MeasureTheory.SignedMeasure.HaveLebesgueDecomposition t μ] [MeasureTheory.SignedMeasure.HaveLebesgueDecomposition (s + t) μ] : MeasureTheory.SignedMeasure.rnDeriv (s + t) μ =ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.SignedMeasure.rnDeriv s μ + MeasureTheory.SignedMeasure.rnDeriv t μ

theorem MeasureTheory.SignedMeasure.rnDeriv_sub {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (t : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) [MeasureTheory.SignedMeasure.HaveLebesgueDecomposition s μ] [MeasureTheory.SignedMeasure.HaveLebesgueDecomposition t μ] [hst : MeasureTheory.SignedMeasure.HaveLebesgueDecomposition (s - t) μ] : MeasureTheory.SignedMeasure.rnDeriv (s - t) μ =ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.SignedMeasure.rnDeriv s μ - MeasureTheory.SignedMeasure.rnDeriv t μ

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

A complex measure is said to HaveLebesgueDecomposition with respect to a positive measure if both its real and imaginary part HaveLebesgueDecomposition with respect to that measure.

• rePart : MeasureTheory.SignedMeasure.HaveLebesgueDecomposition (MeasureTheory.ComplexMeasure.re c) μ
• imPart : MeasureTheory.SignedMeasure.HaveLebesgueDecomposition (MeasureTheory.ComplexMeasure.im c) μ

def MeasureTheory.ComplexMeasure.singularPart {α : Type u_1} {m : MeasurableSpace α} (c : MeasureTheory.ComplexMeasure α) (μ : MeasureTheory.Measure α) : MeasureTheory.ComplexMeasure α

The singular part between a complex measure c and a positive measure μ is the complex measure satisfying c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ) = c. This property is given by MeasureTheory.ComplexMeasure.singularPart_add_withDensity_rnDeriv_eq.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.ComplexMeasure.rnDeriv {α : Type u_1} {m : MeasurableSpace α} (c : MeasureTheory.ComplexMeasure α) (μ : MeasureTheory.Measure α) : α → ℂ

The Radon-Nikodym derivative between a complex measure and a positive measure.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.ComplexMeasure.integrable_rnDeriv {α : Type u_1} {m : MeasurableSpace α} (c : MeasureTheory.ComplexMeasure α) (μ : MeasureTheory.Measure α) : MeasureTheory.Integrable (MeasureTheory.ComplexMeasure.rnDeriv c μ) μ

theorem MeasureTheory.ComplexMeasure.singularPart_add_withDensity_rnDeriv_eq {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {c : MeasureTheory.ComplexMeasure α} [MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition c μ] : MeasureTheory.ComplexMeasure.singularPart c μ + MeasureTheory.Measure.withDensityᵥ μ (MeasureTheory.ComplexMeasure.rnDeriv c μ) = c