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 such that a set is μ-null iff it is μ.toFinite-null. In particular, MeasureTheory.ae μ.toFinite = MeasureTheory.ae μ and μ.toFinite = 0 iff μ = 0. As a corollary, μ can be represented as μ.toFinite.withDensity (μ.rnDeriv μ.toFinite).

Our definition of MeasureTheory.Measure.toFinite ensures some extra properties:

• if μ is a finite measure, then μ.toFinite = μ[|univ] = (μ univ)⁻¹ • μ;
• in particular, μ.toFinite = μ for a probability measure;
• if μ ≠ 0, then μ.toFinite is a probability measure.

Main definitions

In this definition 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.

Main statements

• absolutelyContinuous_toFinite: μ ≪ μ.toFinite.
• toFinite_absolutelyContinuous: μ.toFinite ≪ μ.
• ae_toFinite: ae μ.toFinite = ae μ.

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

Auxiliary definition for MeasureTheory.Measure.toFinite.

Equations

• μ.toFiniteAux = if MeasureTheory.IsFiniteMeasure μ then μ else ⋯.choose

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

A finite measure obtained from an s-finite measure μ, such that μ = μ.toFinite.withDensity (μ.rnDeriv µ.toFinite) (see MeasureTheory.Measure.withDensity_rnDeriv_eq along with MeasureTheory.absolutelyContinuous_toFinite). If μ is non-zero, then μ.toFinite is a probability measure.

Equations

• μ.toFinite = μ.toFiniteAux[|Set.univ]

theorem MeasureTheory.ae_toFiniteAux {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} [SFinite μ] : ae μ.toFiniteAux = ae μ

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

@[simp]

theorem MeasureTheory.ae_toFinite {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} [SFinite μ] : ae μ.toFinite = ae μ

@[simp]

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

@[simp]

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

@[simp]

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

theorem MeasureTheory.toFinite_eq_self {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ] : μ.toFinite = μ

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

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

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

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

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

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