# 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

source
class MeasureTheory.SignedMeasure.HaveLebesgueDecomposition {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (μ : 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 : s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ
- negPart : s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ

Instances

source
theorem MeasureTheory.SignedMeasure.not_haveLebesgueDecomposition_iff {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (μ : Measure α) :
¬s.HaveLebesgueDecomposition μ ↔ ¬s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ ∨ ¬s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ
source
@[instance 100]
instance MeasureTheory.SignedMeasure.haveLebesgueDecomposition_of_sigmaFinite {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (μ : Measure α) [SigmaFinite μ] :
s.HaveLebesgueDecomposition μ
source
instance MeasureTheory.SignedMeasure.haveLebesgueDecomposition_neg {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ] :
(-s).HaveLebesgueDecomposition μ
source
instance MeasureTheory.SignedMeasure.haveLebesgueDecomposition_smul {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ] (r : NNReal) :
(r • s).HaveLebesgueDecomposition μ
source
instance MeasureTheory.SignedMeasure.haveLebesgueDecomposition_smul_real {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ] (r : ℝ) :
(r • s).HaveLebesgueDecomposition μ
source
def MeasureTheory.SignedMeasure.singularPart {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (μ : Measure α) :
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

Instances For

source
theorem MeasureTheory.SignedMeasure.singularPart_mutuallySingular {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (μ : Measure α) :
(s.toJordanDecomposition.posPart.singularPart μ).MutuallySingular (s.toJordanDecomposition.negPart.singularPart μ)
source
theorem MeasureTheory.SignedMeasure.singularPart_totalVariation {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (μ : Measure α) :
(s.singularPart μ).totalVariation = s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ
source
theorem MeasureTheory.SignedMeasure.mutuallySingular_singularPart {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (μ : Measure α) :
VectorMeasure.MutuallySingular (s.singularPart μ) μ.toENNRealVectorMeasure
source
def MeasureTheory.SignedMeasure.rnDeriv {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (μ : 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 `Mathlib/MeasureTheory/Measure/Decomposition/RadonNikodym.lean`.

Equations

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

Instances For

source
theorem MeasureTheory.SignedMeasure.rnDeriv_def {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (μ : Measure α) :
s.rnDeriv μ = fun (x : α) => (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal - (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal
source
theorem MeasureTheory.SignedMeasure.measurable_rnDeriv {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (μ : Measure α) :
Measurable (s.rnDeriv μ)
source
theorem MeasureTheory.SignedMeasure.integrable_rnDeriv {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (μ : Measure α) :
Integrable (s.rnDeriv μ) μ
source
theorem MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eq {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) (s : 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 μ`.

source
theorem MeasureTheory.SignedMeasure.jordanDecomposition_add_withDensity_mutuallySingular {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {t : SignedMeasure α} {f : α → ℝ} (hf : Measurable f) (htμ : 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))
source
theorem MeasureTheory.SignedMeasure.toJordanDecomposition_eq_of_eq_add_withDensity {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s t : SignedMeasure α} {f : α → ℝ} (hf : Measurable f) (hfi : Integrable f μ) (htμ : VectorMeasure.MutuallySingular t μ.toENNRealVectorMeasure) (hadd : s = t + μ.withDensityᵥ f) :
s.toJordanDecomposition = { posPart := t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) => ENNReal.ofReal (f x), negPart := t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) => ENNReal.ofReal (-f x), posPart_finite := ⋯, negPart_finite := ⋯, mutuallySingular := ⋯ }
source
theorem MeasureTheory.SignedMeasure.haveLebesgueDecomposition_mk {α : Type u_1} {m : MeasurableSpace α} {s t : SignedMeasure α} (μ : Measure α) {f : α → ℝ} (hf : Measurable f) (htμ : VectorMeasure.MutuallySingular t μ.toENNRealVectorMeasure) (hadd : s = t + μ.withDensityᵥ f) :
s.HaveLebesgueDecomposition μ
source
theorem MeasureTheory.SignedMeasure.eq_singularPart {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s : SignedMeasure α} (t : SignedMeasure α) (f : α → ℝ) (htμ : 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 `μ`.

source
theorem MeasureTheory.SignedMeasure.singularPart_zero {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) :
singularPart 0 μ = 0
source
theorem MeasureTheory.SignedMeasure.singularPart_neg {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (μ : Measure α) :
(-s).singularPart μ = -s.singularPart μ
source
theorem MeasureTheory.SignedMeasure.singularPart_smul_nnreal {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (μ : Measure α) (r : NNReal) :
(r • s).singularPart μ = r • s.singularPart μ
source
theorem MeasureTheory.SignedMeasure.singularPart_smul {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (μ : Measure α) (r : ℝ) :
(r • s).singularPart μ = r • s.singularPart μ
source
theorem MeasureTheory.SignedMeasure.singularPart_add {α : Type u_1} {m : MeasurableSpace α} (s t : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ] [t.HaveLebesgueDecomposition μ] :
(s + t).singularPart μ = s.singularPart μ + t.singularPart μ
source
theorem MeasureTheory.SignedMeasure.singularPart_sub {α : Type u_1} {m : MeasurableSpace α} (s t : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ] [t.HaveLebesgueDecomposition μ] :
(s - t).singularPart μ = s.singularPart μ - t.singularPart μ
source
theorem MeasureTheory.SignedMeasure.eq_rnDeriv {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s : SignedMeasure α} (t : SignedMeasure α) (f : α → ℝ) (hfi : Integrable f μ) (htμ : VectorMeasure.MutuallySingular t μ.toENNRealVectorMeasure) (hadd : s = t + μ.withDensityᵥ f) :
f =ᶠ[ae μ] 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 `μ`.

source
theorem MeasureTheory.SignedMeasure.rnDeriv_neg {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ] :
(-s).rnDeriv μ =ᶠ[ae μ] -s.rnDeriv μ
source
theorem MeasureTheory.SignedMeasure.rnDeriv_smul {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ] (r : ℝ) :
(r • s).rnDeriv μ =ᶠ[ae μ] r • s.rnDeriv μ
source
theorem MeasureTheory.SignedMeasure.rnDeriv_add {α : Type u_1} {m : MeasurableSpace α} (s t : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ] [t.HaveLebesgueDecomposition μ] [(s + t).HaveLebesgueDecomposition μ] :
(s + t).rnDeriv μ =ᶠ[ae μ] s.rnDeriv μ + t.rnDeriv μ
source
theorem MeasureTheory.SignedMeasure.rnDeriv_sub {α : Type u_1} {m : MeasurableSpace α} (s t : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ] [t.HaveLebesgueDecomposition μ] [hst : (s - t).HaveLebesgueDecomposition μ] :
(s - t).rnDeriv μ =ᶠ[ae μ] s.rnDeriv μ - t.rnDeriv μ
source
class MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition {α : Type u_1} {m : MeasurableSpace α} (c : ComplexMeasure α) (μ : 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 : (re c).HaveLebesgueDecomposition μ
- imPart : (im c).HaveLebesgueDecomposition μ

Instances

source
def MeasureTheory.ComplexMeasure.singularPart {α : Type u_1} {m : MeasurableSpace α} (c : ComplexMeasure α) (μ : Measure α) :
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 μ)

Instances For

source
def MeasureTheory.ComplexMeasure.rnDeriv {α : Type u_1} {m : MeasurableSpace α} (c : ComplexMeasure α) (μ : 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 }

Instances For

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