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 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 μ).

Main statements #

Auxiliary definition for MeasureTheory.Measure.toFinite.

Equations
Instances For

    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
    Instances For
      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_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
      @[simp]
      theorem MeasureTheory.toFinite_eq_zero_iff {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] :
      μ.toFinite = 0 μ = 0
      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.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 : α) :

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

      Equations
      Instances For
        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.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