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.

Main statements

• absolutelyContinuous_toFinite: μ ≪ μ.toFinite.
• toFinite_absolutelyContinuous: μ.toFinite ≪ μ.
• withDensity_densitytoFinite: μ.toFinite.withDensity μ.densityToFinite = μ.

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 ≠ ⊤

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