mathlib3 documentation

measure_theory.decomposition.lebesgue

Lebesgue decomposition #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

measure_theory.measure.have_lebesgue_decomposition : A pair of measures μ and ν is said to have_lebesgue_decomposition if there exist a measure ξ and a measurable function f, such that ξ is mutually singular with respect to ν and μ = ξ + ν.with_density f
measure_theory.measure.singular_part : If a pair of measures have_lebesgue_decomposition, then singular_part chooses the measure from have_lebesgue_decomposition, otherwise it returns the zero measure.
measure_theory.measure.rn_deriv: If a pair of measures have_lebesgue_decomposition, then rn_deriv chooses the measurable function from have_lebesgue_decomposition, otherwise it returns the zero function.
measure_theory.signed_measure.have_lebesgue_decomposition : A signed measure s and a measure μ is said to have_lebesgue_decomposition if both the positive part and negative part of s have_lebesgue_decomposition with respect to μ.
measure_theory.signed_measure.singular_part : 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 μ.
measure_theory.signed_measure.rn_deriv : 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 #

measure_theory.measure.have_lebesgue_decomposition_of_sigma_finite : the Lebesgue decomposition theorem.
measure_theory.measure.eq_singular_part : Given measures μ and ν, if s is a measure mutually singular to ν and f is a measurable function such that μ = s + fν, then s = μ.singular_part ν.
measure_theory.measure.eq_rn_deriv : Given measures μ and ν, if s is a measure mutually singular to ν and f is a measurable function such that μ = s + fν, then f = μ.rn_deriv ν.
measure_theory.signed_measure.singular_part_add_with_density_rn_deriv_eq : the Lebesgue decomposition theorem between a signed measure and a σ-finite positive measure.

Tags #

Lebesgue decomposition theorem

@[class]

structure measure_theory.measure.have_lebesgue_decomposition {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α) :

Prop

lebesgue_decomposition : ∃ (p : measure_theory.measure α × (α → ennreal)), measurable p.snd ∧ p.fst.mutually_singular ν ∧ μ = p.fst + ν.with_density p.snd

A pair of measures μ and ν is said to have_lebesgue_decomposition if there exists a measure ξ and a measurable function f, such that ξ is mutually singular with respect to ν and μ = ξ + ν.with_density f.

Instances of this typeclass

@[irreducible]

noncomputable def measure_theory.measure.singular_part {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α) :

measure_theory.measure α

If a pair of measures have_lebesgue_decomposition, then singular_part chooses the measure from have_lebesgue_decomposition, otherwise it returns the zero measure. For sigma-finite measures, μ = μ.singular_part ν + ν.with_density (μ.rn_deriv ν).

Equations

μ.singular_part ν = dite (μ.have_lebesgue_decomposition ν) (λ (h : μ.have_lebesgue_decomposition ν), (classical.some measure_theory.measure.have_lebesgue_decomposition.lebesgue_decomposition).fst) (λ (h : ¬μ.have_lebesgue_decomposition ν), 0)

Instances for measure_theory.measure.singular_part

@[irreducible]

noncomputable def measure_theory.measure.rn_deriv {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α) :

If a pair of measures have_lebesgue_decomposition, then rn_deriv chooses the measurable function from have_lebesgue_decomposition, otherwise it returns the zero function. For sigma-finite measures, μ = μ.singular_part ν + ν.with_density (μ.rn_deriv ν).

Equations

μ.rn_deriv ν = dite (μ.have_lebesgue_decomposition ν) (λ (h : μ.have_lebesgue_decomposition ν), (classical.some measure_theory.measure.have_lebesgue_decomposition.lebesgue_decomposition).snd) (λ (h : ¬μ.have_lebesgue_decomposition ν), 0)

theorem measure_theory.measure.have_lebesgue_decomposition_spec {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α) [h : μ.have_lebesgue_decomposition ν] :

measurable (μ.rn_deriv ν) ∧ (μ.singular_part ν).mutually_singular ν ∧ μ = μ.singular_part ν + ν.with_density (μ.rn_deriv ν)

theorem measure_theory.measure.have_lebesgue_decomposition_add {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α) [μ.have_lebesgue_decomposition ν] :

μ = μ.singular_part ν + ν.with_density (μ.rn_deriv ν)

@[protected, instance]

def measure_theory.measure.have_lebesgue_decomposition_smul {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α) [μ.have_lebesgue_decomposition ν] (r : nnreal) :

(r • μ).have_lebesgue_decomposition ν

@[measurability]

theorem measure_theory.measure.measurable_rn_deriv {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α) :

measurable (μ.rn_deriv ν)

theorem measure_theory.measure.mutually_singular_singular_part {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α) :

(μ.singular_part ν).mutually_singular ν

theorem measure_theory.measure.singular_part_le {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α) :

μ.singular_part ν ≤ μ

theorem measure_theory.measure.with_density_rn_deriv_le {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α) :

ν.with_density (μ.rn_deriv ν) ≤ μ

@[protected, instance]

def measure_theory.measure.singular_part.measure_theory.is_finite_measure {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} [measure_theory.is_finite_measure μ] :

measure_theory.is_finite_measure (μ.singular_part ν)

@[protected, instance]

def measure_theory.measure.singular_part.measure_theory.sigma_finite {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} [measure_theory.sigma_finite μ] :

measure_theory.sigma_finite (μ.singular_part ν)

@[protected, instance]

def measure_theory.measure.singular_part.measure_theory.is_locally_finite_measure {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} [topological_space α] [measure_theory.is_locally_finite_measure μ] :

measure_theory.is_locally_finite_measure (μ.singular_part ν)

@[protected, instance]

def measure_theory.measure.with_density.measure_theory.is_finite_measure {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} [measure_theory.is_finite_measure μ] :

measure_theory.is_finite_measure (ν.with_density (μ.rn_deriv ν))

@[protected, instance]

def measure_theory.measure.with_density.measure_theory.sigma_finite {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} [measure_theory.sigma_finite μ] :

measure_theory.sigma_finite (ν.with_density (μ.rn_deriv ν))

@[protected, instance]

def measure_theory.measure.with_density.measure_theory.is_locally_finite_measure {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} [topological_space α] [measure_theory.is_locally_finite_measure μ] :

measure_theory.is_locally_finite_measure (ν.with_density (μ.rn_deriv ν))

theorem measure_theory.measure.lintegral_rn_deriv_lt_top_of_measure_ne_top {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (ν : measure_theory.measure α) {s : set α} (hs : ⇑μ s ≠ ⊤) :

∫⁻ (x : α) in s, μ.rn_deriv ν x ∂ν < ⊤

theorem measure_theory.measure.lintegral_rn_deriv_lt_top {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α) [measure_theory.is_finite_measure μ] :

∫⁻ (x : α), μ.rn_deriv ν x ∂ν < ⊤

theorem measure_theory.measure.rn_deriv_lt_top {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α) [measure_theory.sigma_finite μ] :

∀ᵐ (x : α) ∂ν, μ.rn_deriv ν x < ⊤

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

theorem measure_theory.measure.eq_singular_part {α : Type u_1} {m : measurable_space α} {μ ν s : measure_theory.measure α} {f : α → ennreal} (hf : measurable f) (hs : s.mutually_singular ν) (hadd : μ = s + ν.with_density f) :

s = μ.singular_part ν

Given measures μ and ν, if s is a measure mutually singular to ν and f is a measurable function such that μ = s + fν, then s = μ.singular_part μ.

This theorem provides the uniqueness of the singular_part in the Lebesgue decomposition theorem, while measure_theory.measure.eq_rn_deriv provides the uniqueness of the rn_deriv.

theorem measure_theory.measure.singular_part_zero {α : Type u_1} {m : measurable_space α} (ν : measure_theory.measure α) :

0.singular_part ν = 0

theorem measure_theory.measure.singular_part_smul {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α) (r : nnreal) :

(r • μ).singular_part ν = r • μ.singular_part ν

theorem measure_theory.measure.singular_part_add {α : Type u_1} {m : measurable_space α} (μ₁ μ₂ ν : measure_theory.measure α) [μ₁.have_lebesgue_decomposition ν] [μ₂.have_lebesgue_decomposition ν] :

(μ₁ + μ₂).singular_part ν = μ₁.singular_part ν + μ₂.singular_part ν

theorem measure_theory.measure.singular_part_with_density {α : Type u_1} {m : measurable_space α} (ν : measure_theory.measure α) {f : α → ennreal} (hf : measurable f) :

(ν.with_density f).singular_part ν = 0

theorem measure_theory.measure.eq_with_density_rn_deriv {α : Type u_1} {m : measurable_space α} {μ ν s : measure_theory.measure α} {f : α → ennreal} (hf : measurable f) (hs : s.mutually_singular ν) (hadd : μ = s + ν.with_density f) :

ν.with_density f = ν.with_density (μ.rn_deriv ν)

Given measures μ and ν, if s is a measure mutually singular to ν and f is a measurable function such that μ = s + fν, then f = μ.rn_deriv ν.

This theorem provides the uniqueness of the rn_deriv in the Lebesgue decomposition theorem, while measure_theory.measure.eq_singular_part provides the uniqueness of the singular_part. Here, the uniqueness is given in terms of the measures, while the uniqueness in terms of the functions is given in eq_rn_deriv.

theorem measure_theory.measure.eq_rn_deriv {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} [measure_theory.sigma_finite ν] {s : measure_theory.measure α} {f : α → ennreal} (hf : measurable f) (hs : s.mutually_singular ν) (hadd : μ = s + ν.with_density f) :

f =ᵐ[ν] μ.rn_deriv ν

Given measures μ and ν, if s is a measure mutually singular to ν and f is a measurable function such that μ = s + fν, then f = μ.rn_deriv ν.

This theorem provides the uniqueness of the rn_deriv in the Lebesgue decomposition theorem, while measure_theory.measure.eq_singular_part provides the uniqueness of the singular_part. Here, the uniqueness is given in terms of the functions, while the uniqueness in terms of the functions is given in eq_with_density_rn_deriv.

theorem measure_theory.measure.rn_deriv_with_density {α : Type u_1} {m : measurable_space α} (ν : measure_theory.measure α) [measure_theory.sigma_finite ν] {f : α → ennreal} (hf : measurable f) :

(ν.with_density f).rn_deriv ν =ᵐ[ν] f

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

theorem measure_theory.measure.rn_deriv_restrict {α : Type u_1} {m : measurable_space α} (ν : measure_theory.measure α) [measure_theory.sigma_finite ν] {s : set α} (hs : measurable_set s) :

(ν.restrict s).rn_deriv ν =ᵐ[ν] s.indicator 1

The Radon-Nikodym derivative of the restriction of a measure to a measurable set is the indicator function of this set.

theorem measure_theory.measure.exists_positive_of_not_mutually_singular {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α) [measure_theory.is_finite_measure μ] [measure_theory.is_finite_measure ν] (h : ¬μ.mutually_singular ν) :

∃ (ε : nnreal), 0 < ε ∧ ∃ (E : set α), measurable_set E ∧ 0 < ⇑ν E ∧ 0.restrict E ≤ (μ.to_signed_measure - (ε • ν).to_signed_measure).restrict 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 measure_theory.measure.lebesgue_decomposition.measurable_le {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α) :

set (α → ennreal)

Given two measures μ and ν, measurable_le μ ν 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.

Equations

measure_theory.measure.lebesgue_decomposition.measurable_le μ ν = {f : α → ennreal | measurable f ∧ ∀ (A : set α), measurable_set A → ∫⁻ (x : α) in A, f x ∂μ ≤ ⇑ν A}

theorem measure_theory.measure.lebesgue_decomposition.zero_mem_measurable_le {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} :

0 ∈ measure_theory.measure.lebesgue_decomposition.measurable_le μ ν

theorem measure_theory.measure.lebesgue_decomposition.sup_mem_measurable_le {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} {f g : α → ennreal} (hf : f ∈ measure_theory.measure.lebesgue_decomposition.measurable_le μ ν) (hg : g ∈ measure_theory.measure.lebesgue_decomposition.measurable_le μ ν) :

(λ (a : α), f a ⊔ g a) ∈ measure_theory.measure.lebesgue_decomposition.measurable_le μ ν

theorem measure_theory.measure.lebesgue_decomposition.supr_succ_eq_sup {α : Sort u_1} (f : ℕ → α → ennreal) (m : ℕ) (a : α) :

(⨆ (k : ℕ) (hk : k ≤ m + 1), f k a) = f m.succ a ⊔ ⨆ (k : ℕ) (hk : k ≤ m), f k a

theorem measure_theory.measure.lebesgue_decomposition.supr_mem_measurable_le {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} (f : ℕ → α → ennreal) (hf : ∀ (n : ℕ), f n ∈ measure_theory.measure.lebesgue_decomposition.measurable_le μ ν) (n : ℕ) :

(λ (x : α), ⨆ (k : ℕ) (hk : k ≤ n), f k x) ∈ measure_theory.measure.lebesgue_decomposition.measurable_le μ ν

theorem measure_theory.measure.lebesgue_decomposition.supr_mem_measurable_le' {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} (f : ℕ → α → ennreal) (hf : ∀ (n : ℕ), f n ∈ measure_theory.measure.lebesgue_decomposition.measurable_le μ ν) (n : ℕ) :

(⨆ (k : ℕ) (hk : k ≤ n), f k) ∈ measure_theory.measure.lebesgue_decomposition.measurable_le μ ν

theorem measure_theory.measure.lebesgue_decomposition.supr_monotone {α : Type u_1} (f : ℕ → α → ennreal) :

monotone (λ (n : ℕ) (x : α), ⨆ (k : ℕ) (hk : k ≤ n), f k x)

theorem measure_theory.measure.lebesgue_decomposition.supr_monotone' {α : Type u_1} (f : ℕ → α → ennreal) (x : α) :

monotone (λ (n : ℕ), ⨆ (k : ℕ) (hk : k ≤ n), f k x)

theorem measure_theory.measure.lebesgue_decomposition.supr_le_le {α : Type u_1} (f : ℕ → α → ennreal) (n k : ℕ) (hk : k ≤ n) :

f k ≤ λ (x : α), ⨆ (k : ℕ) (hk : k ≤ n), f k x

def measure_theory.measure.lebesgue_decomposition.measurable_le_eval {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α) :

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

Equations

measure_theory.measure.lebesgue_decomposition.measurable_le_eval μ ν = (λ (f : α → ennreal), ∫⁻ (x : α), f x ∂μ) '' measure_theory.measure.lebesgue_decomposition.measurable_le μ ν

theorem measure_theory.measure.have_lebesgue_decomposition_of_finite_measure {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} [measure_theory.is_finite_measure μ] [measure_theory.is_finite_measure ν] :

μ.have_lebesgue_decomposition ν

Any pair of finite measures μ and ν, have_lebesgue_decomposition. That is to say, there exist a measure ξ and a measurable function f, such that ξ is mutually singular with respect to ν and μ = ξ + ν.with_density f.

This is not an instance since this is also shown for the more general σ-finite measures with measure_theory.measure.have_lebesgue_decomposition_of_sigma_finite.

@[protected, instance]

def measure_theory.measure.restrict.measure_theory.is_finite_measure {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {S : μ.finite_spanning_sets_in {s : set α | measurable_set s}} (n : ℕ) :

measure_theory.is_finite_measure (μ.restrict (S.set n))

@[protected, instance]

def measure_theory.measure.have_lebesgue_decomposition_of_sigma_finite {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α) [measure_theory.sigma_finite μ] [measure_theory.sigma_finite ν] :

μ.have_lebesgue_decomposition ν

The Lebesgue decomposition theorem: Any pair of σ-finite measures μ and ν have_lebesgue_decomposition. That is to say, there exist a measure ξ and a measurable function f, such that ξ is mutually singular with respect to ν and μ = ξ + ν.with_density f

@[class]

structure measure_theory.signed_measure.have_lebesgue_decomposition {α : Type u_1} {m : measurable_space α} (s : measure_theory.signed_measure α) (μ : measure_theory.measure α) :

Prop

pos_part : s.to_jordan_decomposition.pos_part.have_lebesgue_decomposition μ
neg_part : s.to_jordan_decomposition.neg_part.have_lebesgue_decomposition μ

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

Instances of this typeclass

theorem measure_theory.signed_measure.not_have_lebesgue_decomposition_iff {α : Type u_1} {m : measurable_space α} (s : measure_theory.signed_measure α) (μ : measure_theory.measure α) :

¬s.have_lebesgue_decomposition μ ↔ ¬s.to_jordan_decomposition.pos_part.have_lebesgue_decomposition μ ∨ ¬s.to_jordan_decomposition.neg_part.have_lebesgue_decomposition μ

@[protected, instance]

def measure_theory.signed_measure.have_lebesgue_decomposition_of_sigma_finite {α : Type u_1} {m : measurable_space α} (s : measure_theory.signed_measure α) (μ : measure_theory.measure α) [measure_theory.sigma_finite μ] :

s.have_lebesgue_decomposition μ

@[protected, instance]

def measure_theory.signed_measure.have_lebesgue_decomposition_neg {α : Type u_1} {m : measurable_space α} (s : measure_theory.signed_measure α) (μ : measure_theory.measure α) [s.have_lebesgue_decomposition μ] :

(-s).have_lebesgue_decomposition μ

@[protected, instance]

def measure_theory.signed_measure.have_lebesgue_decomposition_smul {α : Type u_1} {m : measurable_space α} (s : measure_theory.signed_measure α) (μ : measure_theory.measure α) [s.have_lebesgue_decomposition μ] (r : nnreal) :

(r • s).have_lebesgue_decomposition μ

@[protected, instance]

def measure_theory.signed_measure.have_lebesgue_decomposition_smul_real {α : Type u_1} {m : measurable_space α} (s : measure_theory.signed_measure α) (μ : measure_theory.measure α) [s.have_lebesgue_decomposition μ] (r : ℝ) :

(r • s).have_lebesgue_decomposition μ

noncomputable def measure_theory.signed_measure.singular_part {α : Type u_1} {m : measurable_space α} (s : measure_theory.signed_measure α) (μ : measure_theory.measure α) :

measure_theory.signed_measure α

Given a signed measure s and a measure μ, s.singular_part μ is the signed measure such that s.singular_part μ + μ.with_densityᵥ (s.rn_deriv μ) = s and s.singular_part μ is mutually singular with respect to μ.

Equations

s.singular_part μ = (s.to_jordan_decomposition.pos_part.singular_part μ).to_signed_measure - (s.to_jordan_decomposition.neg_part.singular_part μ).to_signed_measure

theorem measure_theory.signed_measure.singular_part_mutually_singular {α : Type u_1} {m : measurable_space α} (s : measure_theory.signed_measure α) (μ : measure_theory.measure α) :

(s.to_jordan_decomposition.pos_part.singular_part μ).mutually_singular (s.to_jordan_decomposition.neg_part.singular_part μ)

theorem measure_theory.signed_measure.singular_part_total_variation {α : Type u_1} {m : measurable_space α} (s : measure_theory.signed_measure α) (μ : measure_theory.measure α) :

(s.singular_part μ).total_variation = s.to_jordan_decomposition.pos_part.singular_part μ + s.to_jordan_decomposition.neg_part.singular_part μ

theorem measure_theory.signed_measure.mutually_singular_singular_part {α : Type u_1} {m : measurable_space α} (s : measure_theory.signed_measure α) (μ : measure_theory.measure α) :

measure_theory.vector_measure.mutually_singular (s.singular_part μ) μ.to_ennreal_vector_measure

noncomputable def measure_theory.signed_measure.rn_deriv {α : Type u_1} {m : measurable_space α} (s : measure_theory.signed_measure α) (μ : measure_theory.measure α) :

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

rn_deriv s μ satisfies μ.with_densityᵥ (s.rn_deriv μ) = s if and only if s is absolutely continuous with respect to μ and this fact is known as measure_theory.signed_measure.absolutely_continuous_iff_with_density_rn_deriv_eq and can be found in measure_theory.decomposition.radon_nikodym.

Equations

s.rn_deriv μ = λ (x : α), (s.to_jordan_decomposition.pos_part.rn_deriv μ x).to_real - (s.to_jordan_decomposition.neg_part.rn_deriv μ x).to_real

@[measurability]

theorem measure_theory.signed_measure.measurable_rn_deriv {α : Type u_1} {m : measurable_space α} (s : measure_theory.signed_measure α) (μ : measure_theory.measure α) :

measurable (s.rn_deriv μ)

theorem measure_theory.signed_measure.integrable_rn_deriv {α : Type u_1} {m : measurable_space α} (s : measure_theory.signed_measure α) (μ : measure_theory.measure α) :

measure_theory.integrable (s.rn_deriv μ) μ

theorem measure_theory.signed_measure.singular_part_add_with_density_rn_deriv_eq {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) (s : measure_theory.signed_measure α) [s.have_lebesgue_decomposition μ] :

s.singular_part μ + μ.with_densityᵥ (s.rn_deriv μ) = 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 measure_theory.signed_measure.jordan_decomposition_add_with_density_mutually_singular {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {t : measure_theory.signed_measure α} {f : α → ℝ} (hf : measurable f) (htμ : measure_theory.vector_measure.mutually_singular t μ.to_ennreal_vector_measure) :

(t.to_jordan_decomposition.pos_part + μ.with_density (λ (x : α), ennreal.of_real (f x))).mutually_singular (t.to_jordan_decomposition.neg_part + μ.with_density (λ (x : α), ennreal.of_real (-f x)))

theorem measure_theory.signed_measure.to_jordan_decomposition_eq_of_eq_add_with_density {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {s t : measure_theory.signed_measure α} {f : α → ℝ} (hf : measurable f) (hfi : measure_theory.integrable f μ) (htμ : measure_theory.vector_measure.mutually_singular t μ.to_ennreal_vector_measure) (hadd : s = t + μ.with_densityᵥ f) :

s.to_jordan_decomposition = {pos_part := t.to_jordan_decomposition.pos_part + μ.with_density (λ (x : α), ennreal.of_real (f x)), neg_part := t.to_jordan_decomposition.neg_part + μ.with_density (λ (x : α), ennreal.of_real (-f x)), pos_part_finite := _, neg_part_finite := _, mutually_singular := _}

theorem measure_theory.signed_measure.have_lebesgue_decomposition_mk {α : Type u_1} {m : measurable_space α} {s t : measure_theory.signed_measure α} (μ : measure_theory.measure α) {f : α → ℝ} (hf : measurable f) (htμ : measure_theory.vector_measure.mutually_singular t μ.to_ennreal_vector_measure) (hadd : s = t + μ.with_densityᵥ f) :

s.have_lebesgue_decomposition μ

theorem measure_theory.signed_measure.eq_singular_part {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {s : measure_theory.signed_measure α} (t : measure_theory.signed_measure α) (f : α → ℝ) (htμ : measure_theory.vector_measure.mutually_singular t μ.to_ennreal_vector_measure) (hadd : s = t + μ.with_densityᵥ f) :

t = s.singular_part μ

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

theorem measure_theory.signed_measure.singular_part_zero {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) :

0.singular_part μ = 0

theorem measure_theory.signed_measure.singular_part_neg {α : Type u_1} {m : measurable_space α} (s : measure_theory.signed_measure α) (μ : measure_theory.measure α) :

(-s).singular_part μ = -s.singular_part μ

theorem measure_theory.signed_measure.singular_part_smul_nnreal {α : Type u_1} {m : measurable_space α} (s : measure_theory.signed_measure α) (μ : measure_theory.measure α) (r : nnreal) :

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

theorem measure_theory.signed_measure.singular_part_smul {α : Type u_1} {m : measurable_space α} (s : measure_theory.signed_measure α) (μ : measure_theory.measure α) (r : ℝ) :

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

theorem measure_theory.signed_measure.singular_part_add {α : Type u_1} {m : measurable_space α} (s t : measure_theory.signed_measure α) (μ : measure_theory.measure α) [s.have_lebesgue_decomposition μ] [t.have_lebesgue_decomposition μ] :

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

theorem measure_theory.signed_measure.singular_part_sub {α : Type u_1} {m : measurable_space α} (s t : measure_theory.signed_measure α) (μ : measure_theory.measure α) [s.have_lebesgue_decomposition μ] [t.have_lebesgue_decomposition μ] :

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

theorem measure_theory.signed_measure.eq_rn_deriv {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {s : measure_theory.signed_measure α} (t : measure_theory.signed_measure α) (f : α → ℝ) (hfi : measure_theory.integrable f μ) (htμ : measure_theory.vector_measure.mutually_singular t μ.to_ennreal_vector_measure) (hadd : s = t + μ.with_densityᵥ f) :

f =ᵐ[μ] s.rn_deriv μ

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

theorem measure_theory.signed_measure.rn_deriv_neg {α : Type u_1} {m : measurable_space α} (s : measure_theory.signed_measure α) (μ : measure_theory.measure α) [s.have_lebesgue_decomposition μ] :

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

theorem measure_theory.signed_measure.rn_deriv_smul {α : Type u_1} {m : measurable_space α} (s : measure_theory.signed_measure α) (μ : measure_theory.measure α) [s.have_lebesgue_decomposition μ] (r : ℝ) :

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

theorem measure_theory.signed_measure.rn_deriv_add {α : Type u_1} {m : measurable_space α} (s t : measure_theory.signed_measure α) (μ : measure_theory.measure α) [s.have_lebesgue_decomposition μ] [t.have_lebesgue_decomposition μ] [(s + t).have_lebesgue_decomposition μ] :

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

theorem measure_theory.signed_measure.rn_deriv_sub {α : Type u_1} {m : measurable_space α} (s t : measure_theory.signed_measure α) (μ : measure_theory.measure α) [s.have_lebesgue_decomposition μ] [t.have_lebesgue_decomposition μ] [hst : (s - t).have_lebesgue_decomposition μ] :

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

@[class]

structure measure_theory.complex_measure.have_lebesgue_decomposition {α : Type u_1} {m : measurable_space α} (c : measure_theory.complex_measure α) (μ : measure_theory.measure α) :

Prop

re_part : (⇑measure_theory.complex_measure.re c).have_lebesgue_decomposition μ
im_part : (⇑measure_theory.complex_measure.im c).have_lebesgue_decomposition μ

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

noncomputable def measure_theory.complex_measure.singular_part {α : Type u_1} {m : measurable_space α} (c : measure_theory.complex_measure α) (μ : measure_theory.measure α) :

measure_theory.complex_measure α

The singular part between a complex measure c and a positive measure μ is the complex measure satisfying c.singular_part μ + μ.with_densityᵥ (c.rn_deriv μ) = c. This property is given by measure_theory.complex_measure.singular_part_add_with_density_rn_deriv_eq.

Equations

c.singular_part μ = ((⇑measure_theory.complex_measure.re c).singular_part μ).to_complex_measure ((⇑measure_theory.complex_measure.im c).singular_part μ)

noncomputable def measure_theory.complex_measure.rn_deriv {α : Type u_1} {m : measurable_space α} (c : measure_theory.complex_measure α) (μ : measure_theory.measure α) :

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

Equations

c.rn_deriv μ = λ (x : α), {re := (⇑measure_theory.complex_measure.re c).rn_deriv μ x, im := (⇑measure_theory.complex_measure.im c).rn_deriv μ x}

theorem measure_theory.complex_measure.integrable_rn_deriv {α : Type u_1} {m : measurable_space α} (c : measure_theory.complex_measure α) (μ : measure_theory.measure α) :

measure_theory.integrable (c.rn_deriv μ) μ

theorem measure_theory.complex_measure.singular_part_add_with_density_rn_deriv_eq {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {c : measure_theory.complex_measure α} [c.have_lebesgue_decomposition μ] :

c.singular_part μ + μ.with_densityᵥ (c.rn_deriv μ) = c