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.
• 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.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 ν.
• 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.Measure.HaveLebesgueDecomposition {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) : Prop

• lebesgue_decomposition : ∃ p, Measurable p.snd ∧ MeasureTheory.Measure.MutuallySingular p.fst ν ∧ μ = p.fst + MeasureTheory.Measure.withDensity ν p.snd

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.

theorem MeasureTheory.Measure.singularPart_def {α : Type u_3} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) : MeasureTheory.Measure.singularPart μ ν = if h : MeasureTheory.Measure.HaveLebesgueDecomposition μ ν then (Classical.choose (_ : ∃ p, Measurable p.snd ∧ MeasureTheory.Measure.MutuallySingular p.fst ν ∧ μ = p.fst + MeasureTheory.Measure.withDensity ν p.snd)).fst else 0

@[irreducible]

def MeasureTheory.Measure.singularPart {α : Type u_3} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) : MeasureTheory.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 ν).

@[irreducible]

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

theorem MeasureTheory.Measure.rnDeriv_def {α : Type u_3} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) : MeasureTheory.Measure.rnDeriv μ ν = if h : MeasureTheory.Measure.HaveLebesgueDecomposition μ ν then (Classical.choose (_ : ∃ p, Measurable p.snd ∧ MeasureTheory.Measure.MutuallySingular p.fst ν ∧ μ = p.fst + MeasureTheory.Measure.withDensity ν p.snd)).snd else 0

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem MeasureTheory.Measure.rnDeriv_lt_top {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : ∀ᵐ (x : α) ∂ν, MeasureTheory.Measure.rnDeriv μ ν x < ⊤

The Radon-Nikodym derivative of a sigma-finite measure μ with respect to another measure ν is ν-almost everywhere finite.

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

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

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

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

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

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

theorem MeasureTheory.Measure.rnDeriv_restrict {α : Type u_1} {m : MeasurableSpace α} (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite ν] {s : Set α} (hs : MeasurableSet s) : MeasureTheory.Measure.rnDeriv (MeasureTheory.Measure.restrict ν s) ν =ᶠ[MeasureTheory.Measure.ae ν] Set.indicator s 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.exists_positive_of_not_mutuallySingular {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : ¬MeasureTheory.Measure.MutuallySingular μ ν) : ∃ ε, 0 < ε ∧ ∃ E, MeasurableSet E ∧ 0 < ↑↑ν E ∧ MeasureTheory.VectorMeasure.restrict 0 E ≤ MeasureTheory.VectorMeasure.restrict (MeasureTheory.Measure.toSignedMeasure μ - MeasureTheory.Measure.toSignedMeasure (ε • ν)) 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 α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.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.

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

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

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

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

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

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

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

theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_le_le {α : Type u_3} (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 α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) : Set ENNReal

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

theorem MeasureTheory.Measure.haveLebesgueDecomposition_of_finiteMeasure {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : MeasureTheory.Measure.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.

instance MeasureTheory.Measure.restrict.instIsFiniteMeasure {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {S : MeasureTheory.Measure.FiniteSpanningSetsIn μ {s | MeasurableSet s}} (n : ℕ) : MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.restrict μ (MeasureTheory.Measure.FiniteSpanningSetsIn.set S n))

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

The Lebesgue decomposition theorem: 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

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

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

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

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 μ

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

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) μ

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) μ

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

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

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

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.

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

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 + μ.with_densityᵥ f. In this case t = s.singular_part μ and f = s.rn_deriv μ.

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 + MeasureTheory.Measure.withDensity μ fun x => ENNReal.ofReal (f x)) ((MeasureTheory.SignedMeasure.toJordanDecomposition t).negPart + MeasureTheory.Measure.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 + MeasureTheory.Measure.withDensity μ fun x => ENNReal.ofReal (f x)) ((MeasureTheory.SignedMeasure.toJordanDecomposition t).negPart + MeasureTheory.Measure.withDensity μ fun x => ENNReal.ofReal (-f x)) (_ : MeasureTheory.Measure.MutuallySingular ((MeasureTheory.SignedMeasure.toJordanDecomposition t).posPart + MeasureTheory.Measure.withDensity μ fun x => ENNReal.ofReal (f x)) ((MeasureTheory.SignedMeasure.toJordanDecomposition t).negPart + MeasureTheory.Measure.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

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

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.

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.

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