Documentation

Mathlib.MeasureTheory.Decomposition.SignedLebesgue

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 α) :

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 : s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ
negPart : s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ

Instances

theorem MeasureTheory.SignedMeasure.HaveLebesgueDecomposition.posPart {α : Type u_1} {m : MeasurableSpace α} {s : MeasureTheory.SignedMeasure α} {μ : MeasureTheory.Measure α} [self : s.HaveLebesgueDecomposition μ] :

s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ

theorem MeasureTheory.SignedMeasure.HaveLebesgueDecomposition.negPart {α : Type u_1} {m : MeasurableSpace α} {s : MeasureTheory.SignedMeasure α} {μ : MeasureTheory.Measure α} [self : s.HaveLebesgueDecomposition μ] :

s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ

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

¬s.HaveLebesgueDecomposition μ ↔ ¬s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ ∨ ¬s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ

@[instance 100]

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

s.HaveLebesgueDecomposition μ

Equations

⋯ = ⋯

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

(-s).HaveLebesgueDecomposition μ

Equations

⋯ = ⋯

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

(r • s).HaveLebesgueDecomposition μ

Equations

⋯ = ⋯

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

(r • s).HaveLebesgueDecomposition μ

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

s.singularPart μ = (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure - (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure

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

(s.toJordanDecomposition.posPart.singularPart μ).MutuallySingular (s.toJordanDecomposition.negPart.singularPart μ)

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

(s.singularPart μ).totalVariation = s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ

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

MeasureTheory.VectorMeasure.MutuallySingular (s.singularPart μ) μ.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

s.rnDeriv μ x = (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal - (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal

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

s.rnDeriv μ = fun (x : α) => (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal - (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal

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

Measurable (s.rnDeriv μ)

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

MeasureTheory.Integrable (s.rnDeriv μ) μ

theorem MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eq {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : MeasureTheory.SignedMeasure α) [s.HaveLebesgueDecomposition μ] :

s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) = 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 μ.toENNRealVectorMeasure) :

(t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) => ENNReal.ofReal (f x)).MutuallySingular (t.toJordanDecomposition.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 μ.toENNRealVectorMeasure) (hadd : s = t + μ.withDensityᵥ f) :

s.toJordanDecomposition = MeasureTheory.JordanDecomposition.mk (t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) => ENNReal.ofReal (f x)) (t.toJordanDecomposition.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 μ.toENNRealVectorMeasure) (hadd : s = t + μ.withDensityᵥ f) :

s.HaveLebesgueDecomposition μ

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

t = s.singularPart μ

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 α) :

(-s).singularPart μ = -s.singularPart μ

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

(r • s).singularPart μ = r • s.singularPart μ

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

(r • s).singularPart μ = r • s.singularPart μ

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

(s + t).singularPart μ = s.singularPart μ + t.singularPart μ

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

(s - t).singularPart μ = s.singularPart μ - t.singularPart μ

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 μ.toENNRealVectorMeasure) (hadd : s = t + μ.withDensityᵥ f) :

f =ᵐ[μ] s.rnDeriv μ

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 α) [s.HaveLebesgueDecomposition μ] :

(-s).rnDeriv μ =ᵐ[μ] -s.rnDeriv μ

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

(r • s).rnDeriv μ =ᵐ[μ] r • s.rnDeriv μ

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

(s + t).rnDeriv μ =ᵐ[μ] s.rnDeriv μ + t.rnDeriv μ

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

(s - t).rnDeriv μ =ᵐ[μ] s.rnDeriv μ - t.rnDeriv μ

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

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.ComplexMeasure.re c).HaveLebesgueDecomposition μ
imPart : (MeasureTheory.ComplexMeasure.im c).HaveLebesgueDecomposition μ

Instances

theorem MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition.rePart {α : Type u_1} {m : MeasurableSpace α} {c : MeasureTheory.ComplexMeasure α} {μ : MeasureTheory.Measure α} [self : c.HaveLebesgueDecomposition μ] :

(MeasureTheory.ComplexMeasure.re c).HaveLebesgueDecomposition μ

theorem MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition.imPart {α : Type u_1} {m : MeasurableSpace α} {c : MeasureTheory.ComplexMeasure α} {μ : MeasureTheory.Measure α} [self : c.HaveLebesgueDecomposition μ] :

(MeasureTheory.ComplexMeasure.im c).HaveLebesgueDecomposition μ

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

c.singularPart μ = ((MeasureTheory.ComplexMeasure.re c).singularPart μ).toComplexMeasure ((MeasureTheory.ComplexMeasure.im c).singularPart μ)

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

c.rnDeriv μ x = { re := (MeasureTheory.ComplexMeasure.re c).rnDeriv μ x, im := (MeasureTheory.ComplexMeasure.im c).rnDeriv μ x }

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

MeasureTheory.Integrable (c.rnDeriv μ) μ

theorem MeasureTheory.ComplexMeasure.singularPart_add_withDensity_rnDeriv_eq {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {c : MeasureTheory.ComplexMeasure α} [c.HaveLebesgueDecomposition μ] :

c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ) = c