Documentation

Mathlib.MeasureTheory.Measure.WithDensityFinite

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:

Main definitions #

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

Main statements #

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

Auxiliary definition for MeasureTheory.Measure.toFinite.

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

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
theorem MeasureTheory.ae_toFiniteAux {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} [SFinite μ] :
@[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]
@[deprecated MeasureTheory.sfiniteSeq_absolutelyContinuous_toFinite (since := "2024-10-11")]

Alias of MeasureTheory.sfiniteSeq_absolutelyContinuous_toFinite.

@[deprecated MeasureTheory.Measure.rnDeriv (since := "2024-10-04")]
noncomputable def MeasureTheory.Measure.densityToFinite {α : Type u_1} {mα : MeasurableSpace α} (μ : Measure α) [SFinite μ] (a : α) :

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

Equations
@[deprecated "No deprecation message was provided." (since := "2024-10-04")]
@[deprecated MeasureTheory.Measure.measurable_rnDeriv (since := "2024-10-04")]
@[deprecated MeasureTheory.Measure.withDensity_rnDeriv_eq (since := "2024-10-04")]
@[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")]