s-finite measures can be written as withDensity of a finite measure

If μ is an s-finite measure, then there exists a finite measure μ.toFinite and a measurable function densityToFinite μ such that μ = μ.toFinite.withDensity μ.densityToFinite. If μ is zero this is the zero measure, and otherwise we can choose a probability measure for μ.toFinite.

That measure is not unique, and in particular our implementation leads to μ.toFinite ≠ μ even if μ is a probability measure.

We use this construction to define a set μ.sigmaFiniteSet, such that μ.restrict μ.sigmaFiniteSet is sigma-finite, and for all measurable sets s ⊆ μ.sigmaFiniteSetᶜ, either μ s = 0 or μ s = ∞.

Main definitions

In these definitions and the results below, μ is an s-finite measure (SFinite μ).

• MeasureTheory.Measure.toFinite: a finite measure with μ ≪ μ.toFinite and μ.toFinite ≪ μ. If μ ≠ 0, this is a probability measure.
• MeasureTheory.Measure.densityToFinite: a measurable function such that μ = μ.toFinite.withDensity μ.densityToFinite.
• MeasureTheory.Measure.sigmaFiniteSet: a measurable set such that μ.restrict μ.sigmaFiniteSet is sigma-finite, and for all sets s ⊆ μ.sigmaFiniteSetᶜ, either μ s = 0 or μ s = ∞.

Main statements

• absolutelyContinuous_toFinite: μ ≪ μ.toFinite.

• toFinite_absolutelyContinuous: μ.toFinite ≪ μ.

• withDensity_densitytoFinite: μ.toFinite.withDensity μ.densityToFinite = μ.

• An instance showing that μ.restrict μ.sigmaFiniteSet is sigma-finite.

• restrict_compl_sigmaFiniteSet_eq_zero_or_top: the measure μ.restrict μ.sigmaFiniteSetᶜ takes only two values: 0 and ∞ .

• measure_compl_sigmaFiniteSet_eq_zero_iff_sigmaFinite: an s-finite measure μ is sigma-finite iff μ μ.sigmaFiniteSetᶜ = 0.

noncomputable def MeasureTheory.Measure.toFiniteAux {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] : MeasureTheory.Measure α

Auxiliary definition for MeasureTheory.Measure.toFinite.

Equations

• μ.toFiniteAux = MeasureTheory.Measure.sum fun (n : ℕ) => (2 ^ (n + 1) * (MeasureTheory.sFiniteSeq μ n) Set.univ)⁻¹ • MeasureTheory.sFiniteSeq μ n

noncomputable def MeasureTheory.Measure.toFinite {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] : MeasureTheory.Measure α

A finite measure obtained from an s-finite measure μ, such that μ = μ.toFinite.withDensity μ.densityToFinite (see withDensity_densitytoFinite). If μ is non-zero, this is a probability measure.

Equations

• μ.toFinite = ProbabilityTheory.cond μ.toFiniteAux Set.univ

theorem MeasureTheory.toFiniteAux_apply {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] (s : Set α) : μ.toFiniteAux s = ∑' (n : ℕ), (2 ^ (n + 1) * (MeasureTheory.sFiniteSeq μ n) Set.univ)⁻¹ * (MeasureTheory.sFiniteSeq μ n) s

theorem MeasureTheory.toFinite_apply {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] (s : Set α) : μ.toFinite s = (μ.toFiniteAux Set.univ)⁻¹ * μ.toFiniteAux s

theorem MeasureTheory.toFiniteAux_zero {α : Type u_1} {mα : MeasurableSpace α} : MeasureTheory.Measure.toFiniteAux 0 = 0

@[simp]

theorem MeasureTheory.toFinite_zero {α : Type u_1} {mα : MeasurableSpace α} : MeasureTheory.Measure.toFinite 0 = 0

theorem MeasureTheory.toFiniteAux_eq_zero_iff {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] : μ.toFiniteAux = 0 ↔ μ = 0

theorem MeasureTheory.toFiniteAux_univ_le_one {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] : μ.toFiniteAux Set.univ ≤ 1

instance MeasureTheory.instIsFiniteMeasureToFiniteAux {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] : MeasureTheory.IsFiniteMeasure μ.toFiniteAux

Equations

• ⋯ = ⋯

@[simp]

theorem MeasureTheory.toFinite_eq_zero_iff {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] : μ.toFinite = 0 ↔ μ = 0

instance MeasureTheory.instIsFiniteMeasureToFinite {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] : MeasureTheory.IsFiniteMeasure μ.toFinite

Equations

• ⋯ = ⋯

instance MeasureTheory.instIsProbabilityMeasureToFiniteOfNeZeroMeasure {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] [h_zero : NeZero μ] : MeasureTheory.IsProbabilityMeasure μ.toFinite

Equations

• ⋯ = ⋯

theorem MeasureTheory.sFiniteSeq_absolutelyContinuous_toFiniteAux {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] (n : ℕ) : (MeasureTheory.sFiniteSeq μ n).AbsolutelyContinuous μ.toFiniteAux

theorem MeasureTheory.toFiniteAux_absolutelyContinuous_toFinite {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] : μ.toFiniteAux.AbsolutelyContinuous μ.toFinite

theorem MeasureTheory.sFiniteSeq_absolutelyContinuous_toFinite {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] (n : ℕ) : (MeasureTheory.sFiniteSeq μ n).AbsolutelyContinuous μ.toFinite

theorem MeasureTheory.absolutelyContinuous_toFinite {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] : μ.AbsolutelyContinuous μ.toFinite

theorem MeasureTheory.toFinite_absolutelyContinuous {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] : μ.toFinite.AbsolutelyContinuous μ

noncomputable def MeasureTheory.Measure.densityToFinite {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] (a : α) : ENNReal

A measurable function such that μ.toFinite.withDensity μ.densityToFinite = μ. See withDensity_densitytoFinite.

Equations

• μ.densityToFinite a = ∑' (n : ℕ), (MeasureTheory.sFiniteSeq μ n).rnDeriv μ.toFinite a

theorem MeasureTheory.densityToFinite_def {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] : μ.densityToFinite = fun (a : α) => ∑' (n : ℕ), (MeasureTheory.sFiniteSeq μ n).rnDeriv μ.toFinite a

theorem MeasureTheory.measurable_densityToFinite {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] : Measurable μ.densityToFinite

theorem MeasureTheory.withDensity_densitytoFinite {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] : μ.toFinite.withDensity μ.densityToFinite = μ

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

theorem MeasureTheory.densityToFinite_ae_ne_top {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : ∀ᵐ (x : α) ∂μ, μ.densityToFinite x ≠ ⊤

def MeasureTheory.Measure.sigmaFiniteSet {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] : Set α

A measurable set such that μ.restrict μ.sigmaFiniteSet is sigma-finite, and for all measurable sets s ⊆ μ.sigmaFiniteSetᶜ, either μ s = 0 or μ s = ∞.

Equations

• μ.sigmaFiniteSet = {x : α | μ.densityToFinite x ≠ ⊤}

theorem MeasureTheory.measurableSet_sigmaFiniteSet {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] : MeasurableSet μ.sigmaFiniteSet

theorem MeasureTheory.restrict_compl_sigmaFiniteSet {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] : μ.restrict μ.sigmaFiniteSetᶜ = ⊤ • μ.toFinite.restrict μ.sigmaFiniteSetᶜ

theorem MeasureTheory.restrict_compl_sigmaFiniteSet_eq_zero_or_top {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] (s : Set α) : (μ.restrict μ.sigmaFiniteSetᶜ) s = 0 ∨ (μ.restrict μ.sigmaFiniteSetᶜ) s = ⊤

The measure μ.restrict μ.sigmaFiniteSetᶜ takes only two values: 0 and ∞ .

theorem MeasureTheory.measure_eq_zero_or_top_of_subset_compl_sigmaFiniteSet {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} [MeasureTheory.SFinite μ] (ht_subset : t ⊆ μ.sigmaFiniteSetᶜ) : μ t = 0 ∨ μ t = ⊤

theorem MeasureTheory.toFinite_withDensity_restrict_sigmaFiniteSet {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] : (μ.toFinite.withDensity fun (x : α) => if μ.densityToFinite x ≠ ⊤ then μ.densityToFinite x else 1).restrict μ.sigmaFiniteSet = μ.restrict μ.sigmaFiniteSet

instance MeasureTheory.instSigmaFiniteRestrictSigmaFiniteSet {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] : MeasureTheory.SigmaFinite (μ.restrict μ.sigmaFiniteSet)

The restriction of an s-finite measure μ to μ.sigmaFiniteSet is sigma-finite.

Equations

• ⋯ = ⋯

theorem MeasureTheory.sigmaFinite_of_measure_compl_sigmaFiniteSet_eq_zero {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] (h : μ μ.sigmaFiniteSetᶜ = 0) : MeasureTheory.SigmaFinite μ

@[simp]

theorem MeasureTheory.measure_compl_sigmaFiniteSet {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : μ μ.sigmaFiniteSetᶜ = 0

theorem MeasureTheory.measure_compl_sigmaFiniteSet_eq_zero_iff_sigmaFinite {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] : μ μ.sigmaFiniteSetᶜ = 0 ↔ MeasureTheory.SigmaFinite μ

An s-finite measure μ is sigma-finite iff μ μ.sigmaFiniteSetᶜ = 0.