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 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 (deprecated, use MeasureTheory.Measure.rnDeriv): the Radon-Nikodym derivative of μ.toFinite with respect to μ.

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 μ.densityToFinite (see withDensity_densitytoFinite). If μ is non-zero, this is a probability measure.

Equations

• μ.toFinite = ProbabilityTheory.cond μ.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

@[deprecated MeasureTheory.sfiniteSeq_absolutelyContinuous_toFinite (since := "2024-10-11")]

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

Alias of MeasureTheory.sfiniteSeq_absolutelyContinuous_toFinite.

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

@[deprecated MeasureTheory.Measure.rnDeriv (since := "2024-10-04")]

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

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

Equations

• μ.densityToFinite a = μ.rnDeriv μ.toFinite a

@[deprecated "No deprecation message was provided." (since := "2024-10-04")]

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

@[deprecated MeasureTheory.Measure.measurable_rnDeriv (since := "2024-10-04")]

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

@[deprecated MeasureTheory.Measure.withDensity_rnDeriv_eq (since := "2024-10-04")]

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

@[deprecated MeasureTheory.Measure.rnDeriv_lt_top (since := "2024-10-04")]

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

@[deprecated MeasureTheory.Measure.rnDeriv_ne_top (since := "2024-10-04")]

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

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