# 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 : } (s : ) (μ : ) :

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 :
• negPart :
Instances
Equations
Equations
instance MeasureTheory.SignedMeasure.haveLebesgueDecomposition_smul {α : Type u_1} {m : } (s : ) (μ : ) (r : NNReal) :
Equations
• (_ : ) = (_ : )
instance MeasureTheory.SignedMeasure.haveLebesgueDecomposition_smul_real {α : Type u_1} {m : } (s : ) (μ : ) (r : ) :
Equations
• (_ : ) = (_ : )
def MeasureTheory.SignedMeasure.singularPart {α : Type u_1} {m : } (s : ) (μ : ) :

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.
Instances For
def MeasureTheory.SignedMeasure.rnDeriv {α : Type u_1} {m : } (s : ) (μ : ) :
α

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.
Instances For
theorem MeasureTheory.SignedMeasure.rnDeriv_def {α : Type u_1} {m : } (s : ) (μ : ) :
= fun (x : α) =>
theorem MeasureTheory.SignedMeasure.measurable_rnDeriv {α : Type u_1} {m : } (s : ) (μ : ) :
theorem MeasureTheory.SignedMeasure.integrable_rnDeriv {α : Type u_1} {m : } (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 + μ.with_densityᵥ f. In this case t = s.singular_part μ and f = s.rn_deriv μ.

theorem MeasureTheory.SignedMeasure.haveLebesgueDecomposition_mk {α : Type u_1} {m : } {s : } {t : } (μ : ) {f : α} (hf : ) (hadd : ) :
theorem MeasureTheory.SignedMeasure.eq_singularPart {α : Type u_1} {m : } {μ : } {s : } (t : ) (f : α) (hadd : ) :

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 : } (μ : ) :
theorem MeasureTheory.SignedMeasure.singularPart_neg {α : Type u_1} {m : } (s : ) (μ : ) :
theorem MeasureTheory.SignedMeasure.singularPart_smul_nnreal {α : Type u_1} {m : } (s : ) (μ : ) (r : NNReal) :
theorem MeasureTheory.SignedMeasure.singularPart_smul {α : Type u_1} {m : } (s : ) (μ : ) (r : ) :
theorem MeasureTheory.SignedMeasure.eq_rnDeriv {α : Type u_1} {m : } {μ : } {s : } (t : ) (f : α) (hfi : ) (hadd : ) :

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_smul {α : Type u_1} {m : } (s : ) (μ : ) (r : ) :
class MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition {α : Type u_1} {m : } (c : ) (μ : ) :

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.

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

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

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.
Instances For
theorem MeasureTheory.ComplexMeasure.integrable_rnDeriv {α : Type u_1} {m : } (c : ) (μ : ) :