Documentation

Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Classes for s-finite measures #

We introduce the following typeclasses for measures:

class MeasureTheory.SFinite {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) :

A measure is called s-finite if it is a countable sum of finite measures.

Instances
    noncomputable def MeasureTheory.sfiniteSeq {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [h : SFinite μ] :
    Measure α

    A sequence of finite measures such that μ = sum (sfiniteSeq μ) (see sum_sfiniteSeq).

    Equations
    theorem MeasureTheory.sum_sfiniteSeq {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [h : SFinite μ] :
    theorem MeasureTheory.sfiniteSeq_le {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [SFinite μ] (n : ) :
    sfiniteSeq μ n μ
    @[simp]
    theorem MeasureTheory.sfiniteSeq_zero {α : Type u_1} {m0 : MeasurableSpace α} (n : ) :
    theorem MeasureTheory.sfinite_sum_of_countable {α : Type u_1} {ι : Type u_3} {m0 : MeasurableSpace α} [Countable ι] (m : ιMeasure α) [∀ (n : ι), IsFiniteMeasure (m n)] :

    A countable sum of finite measures is s-finite. This lemma is superseded by the instance below.

    instance MeasureTheory.instSFiniteSumOfCountable {α : Type u_1} {ι : Type u_3} {m0 : MeasurableSpace α} [Countable ι] (m : ιMeasure α) [∀ (n : ι), SFinite (m n)] :
    instance MeasureTheory.instSFiniteHAddMeasure {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} [SFinite μ] [SFinite ν] :
    SFinite (μ + ν)
    instance MeasureTheory.instSFiniteRestrict {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [SFinite μ] (s : Set α) :

    For an s-finite measure μ, there exists a finite measure ν such that each of μ and ν is absolutely continuous with respect to the other.

    class MeasureTheory.SigmaFinite {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) :

    A measure μ is called σ-finite if there is a countable collection of sets { A i | i ∈ ℕ } such that μ (A i) < ∞ and ⋃ i, A i = s.

    Instances

      If μ is σ-finite it has finite spanning sets in the collection of all measurable sets.

      Equations
      def MeasureTheory.spanningSets {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [SigmaFinite μ] (i : ) :
      Set α

      A noncomputable way to get a monotone collection of sets that span univ and have finite measure using Classical.choose. This definition satisfies monotonicity in addition to all other properties in SigmaFinite.

      Equations
      theorem MeasureTheory.spanningSets_mono {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [SigmaFinite μ] {m n : } (hmn : m n) :
      theorem MeasureTheory.measure_spanningSets_lt_top {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [SigmaFinite μ] (i : ) :
      μ (spanningSets μ i) <
      @[simp]
      theorem MeasureTheory.iUnion_spanningSets {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [SigmaFinite μ] :
      ⋃ (i : ), spanningSets μ i = Set.univ
      noncomputable def MeasureTheory.spanningSetsIndex {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [SigmaFinite μ] (x : α) :

      spanningSetsIndex μ x is the least n : ℕ such that x ∈ spanningSets μ n.

      Equations
      theorem MeasureTheory.spanningSetsIndex_eq_iff {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [SigmaFinite μ] {x : α} {n : } :
      theorem MeasureTheory.mem_spanningSets_of_index_le {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [SigmaFinite μ] (x : α) {n : } (hn : spanningSetsIndex μ x n) :
      theorem MeasureTheory.measure_singleton_lt_top {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {a : α} [SigmaFinite μ] :
      μ {a} <
      @[instance 100]
      theorem MeasureTheory.Measure.forall_measure_inter_spanningSets_eq_zero {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [SigmaFinite μ] (s : Set α) :
      (∀ (n : ), μ (s spanningSets μ n) = 0) μ s = 0

      A set in a σ-finite space has zero measure if and only if its intersection with all members of the countable family of finite measure spanning sets has zero measure.

      theorem MeasureTheory.Measure.exists_measure_inter_spanningSets_pos {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [SigmaFinite μ] (s : Set α) :
      (∃ (n : ), 0 < μ (s spanningSets μ n)) 0 < μ s

      A set in a σ-finite space has positive measure if and only if its intersection with some member of the countable family of finite measure spanning sets has positive measure.

      theorem MeasureTheory.Measure.finite_const_le_meas_of_disjoint_iUnion₀ {α : Type u_1} {ι : Type u_4} [MeasurableSpace α] (μ : Measure α) {ε : ENNReal} (ε_pos : 0 < ε) {As : ιSet α} (As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ) (As_disj : Pairwise (Function.onFun (AEDisjoint μ) As)) (Union_As_finite : μ (⋃ (i : ι), As i) ) :
      {i : ι | ε μ (As i)}.Finite

      If the union of a.e.-disjoint null-measurable sets has finite measure, then there are only finitely many members of the union whose measure exceeds any given positive number.

      theorem MeasureTheory.Measure.finite_const_le_meas_of_disjoint_iUnion {α : Type u_1} {ι : Type u_4} [MeasurableSpace α] (μ : Measure α) {ε : ENNReal} (ε_pos : 0 < ε) {As : ιSet α} (As_mble : ∀ (i : ι), MeasurableSet (As i)) (As_disj : Pairwise (Function.onFun Disjoint As)) (Union_As_finite : μ (⋃ (i : ι), As i) ) :
      {i : ι | ε μ (As i)}.Finite

      If the union of disjoint measurable sets has finite measure, then there are only finitely many members of the union whose measure exceeds any given positive number.

      theorem Set.Infinite.meas_eq_top {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSingletonClass α] {s : Set α} (hs : s.Infinite) (h' : ∃ (ε : ENNReal), ε 0 xs, ε μ {x}) :
      μ s =

      If all elements of an infinite set have measure uniformly separated from zero, then the set has infinite measure.

      theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀ {α : Type u_1} {ι : Type u_4} {x✝ : MeasurableSpace α} (μ : Measure α) {As : ιSet α} (As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ) (As_disj : Pairwise (Function.onFun (AEDisjoint μ) As)) (Union_As_finite : μ (⋃ (i : ι), As i) ) :
      {i : ι | 0 < μ (As i)}.Countable

      If the union of a.e.-disjoint null-measurable sets has finite measure, then there are only countably many members of the union whose measure is positive.

      theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top {α : Type u_1} {ι : Type u_4} {x✝ : MeasurableSpace α} (μ : Measure α) {As : ιSet α} (As_mble : ∀ (i : ι), MeasurableSet (As i)) (As_disj : Pairwise (Function.onFun Disjoint As)) (Union_As_finite : μ (⋃ (i : ι), As i) ) :
      {i : ι | 0 < μ (As i)}.Countable

      If the union of disjoint measurable sets has finite measure, then there are only countably many members of the union whose measure is positive.

      theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_iUnion₀ {α : Type u_1} {ι : Type u_4} {x✝ : MeasurableSpace α} {μ : Measure α} [SFinite μ] {As : ιSet α} (As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ) (As_disj : Pairwise (Function.onFun (AEDisjoint μ) As)) :
      {i : ι | 0 < μ (As i)}.Countable

      In an s-finite space, among disjoint null-measurable sets, only countably many can have positive measure.

      theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_iUnion {α : Type u_1} {ι : Type u_4} {x✝ : MeasurableSpace α} {μ : Measure α} [SFinite μ] {As : ιSet α} (As_mble : ∀ (i : ι), MeasurableSet (As i)) (As_disj : Pairwise (Function.onFun Disjoint As)) :
      {i : ι | 0 < μ (As i)}.Countable

      In an s-finite space, among disjoint measurable sets, only countably many can have positive measure.

      theorem MeasureTheory.Measure.countable_meas_level_set_pos₀ {α : Type u_4} {β : Type u_5} {x✝ : MeasurableSpace α} {μ : Measure α} [SFinite μ] [MeasurableSpace β] [MeasurableSingletonClass β] {g : αβ} (g_mble : NullMeasurable g μ) :
      {t : β | 0 < μ {a : α | g a = t}}.Countable
      theorem MeasureTheory.Measure.countable_meas_level_set_pos {α : Type u_4} {β : Type u_5} {x✝ : MeasurableSpace α} {μ : Measure α} [SFinite μ] [MeasurableSpace β] [MeasurableSingletonClass β] {g : αβ} (g_mble : Measurable g) :
      {t : β | 0 < μ {a : α | g a = t}}.Countable
      theorem MeasureTheory.Measure.measure_toMeasurable_inter_of_sum {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hs : MeasurableSet s) {t : Set α} {m : Measure α} (hv : ∀ (n : ), (m n) t ) ( : μ = sum m) :
      μ (toMeasurable μ t s) = μ (t s)

      If a measure μ is the sum of a countable family mₙ, and a set t has finite measure for each mₙ, then its measurable superset toMeasurable μ t (which has the same measure as t) satisfies, for any measurable set s, the equality μ (toMeasurable μ t ∩ s) = μ (t ∩ s).

      theorem MeasureTheory.Measure.measure_toMeasurable_inter_of_cover {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hs : MeasurableSet s) {t : Set α} {v : Set α} (hv : t ⋃ (n : ), v n) (h'v : ∀ (n : ), μ (t v n) ) :
      μ (toMeasurable μ t s) = μ (t s)

      If a set t is covered by a countable family of finite measure sets, then its measurable superset toMeasurable μ t (which has the same measure as t) satisfies, for any measurable set s, the equality μ (toMeasurable μ t ∩ s) = μ (t ∩ s).

      theorem MeasureTheory.Measure.restrict_toMeasurable_of_cover {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {v : Set α} (hv : s ⋃ (n : ), v n) (h'v : ∀ (n : ), μ (s v n) ) :
      theorem MeasureTheory.Measure.measure_toMeasurable_inter_of_sFinite {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [SFinite μ] {s : Set α} (hs : MeasurableSet s) (t : Set α) :
      μ (toMeasurable μ t s) = μ (t s)

      The measurable superset toMeasurable μ t of t (which has the same measure as t) satisfies, for any measurable set s, the equality μ (toMeasurable μ t ∩ s) = μ (t ∩ s). This only holds when μ is s-finite -- for example for σ-finite measures. For a version without this assumption (but requiring that t has finite measure), see measure_toMeasurable_inter.

      @[simp]
      theorem MeasureTheory.Measure.iSup_restrict_spanningSets_of_measurableSet {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [SigmaFinite μ] (hs : MeasurableSet s) :
      ⨆ (i : ), (μ.restrict (spanningSets μ i)) s = μ s

      Auxiliary lemma for iSup_restrict_spanningSets.

      theorem MeasureTheory.Measure.iSup_restrict_spanningSets {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [SigmaFinite μ] (s : Set α) :
      ⨆ (i : ), (μ.restrict (spanningSets μ i)) s = μ s
      theorem MeasureTheory.Measure.exists_subset_measure_lt_top {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [SigmaFinite μ] {r : ENNReal} (hs : MeasurableSet s) (h's : r < μ s) :
      ∃ (t : Set α), MeasurableSet t t s r < μ t μ t <

      In a σ-finite space, any measurable set of measure > r contains a measurable subset of finite measure > r.

      def MeasureTheory.Measure.FiniteSpanningSetsIn.mono' {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {C D : Set (Set α)} (h : μ.FiniteSpanningSetsIn C) (hC : C {s : Set α | μ s < } D) :

      If μ has finite spanning sets in C and C ∩ {s | μ s < ∞} ⊆ D then μ has finite spanning sets in D.

      Equations
      • h.mono' hC = { set := h.set, set_mem := , finite := , spanning := }
      def MeasureTheory.Measure.FiniteSpanningSetsIn.mono {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {C D : Set (Set α)} (h : μ.FiniteSpanningSetsIn C) (hC : C D) :

      If μ has finite spanning sets in C and C ⊆ D then μ has finite spanning sets in D.

      Equations

      If μ has finite spanning sets in the collection of measurable sets C, then μ is σ-finite.

      theorem MeasureTheory.Measure.FiniteSpanningSetsIn.ext {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} {C : Set (Set α)} (hA : m0 = MeasurableSpace.generateFrom C) (hC : IsPiSystem C) (h : μ.FiniteSpanningSetsIn C) (h_eq : sC, μ s = ν s) :
      μ = ν

      An extensionality for measures. It is ext_of_generateFrom_of_iUnion formulated in terms of FiniteSpanningSetsIn.

      theorem MeasureTheory.Measure.sigmaFinite_of_countable {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {S : Set (Set α)} (hc : S.Countable) ( : sS, μ s < ) (hU : ⋃₀ S = Set.univ) :
      def MeasureTheory.Measure.FiniteSpanningSetsIn.ofLE {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h : ν μ) {C : Set (Set α)} (S : μ.FiniteSpanningSetsIn C) :

      Given measures μ, ν where ν ≤ μ, FiniteSpanningSetsIn.ofLe provides the induced FiniteSpanningSet with respect to ν from a FiniteSpanningSet with respect to μ.

      Equations
      theorem MeasureTheory.Measure.sigmaFinite_of_le {α : Type u_1} {m0 : MeasurableSpace α} {ν : Measure α} (μ : Measure α) [hs : SigmaFinite μ] (h : ν μ) :
      @[simp]
      theorem MeasureTheory.Measure.add_right_inj {α : Type u_1} {m0 : MeasurableSpace α} (μ ν₁ ν₂ : Measure α) [SigmaFinite μ] :
      μ + ν₁ = μ + ν₂ ν₁ = ν₂
      @[simp]
      theorem MeasureTheory.Measure.add_left_inj {α : Type u_1} {m0 : MeasurableSpace α} (μ ν₁ ν₂ : Measure α) [SigmaFinite μ] :
      ν₁ + μ = ν₂ + μ ν₁ = ν₂
      @[instance 100]

      Every finite measure is σ-finite.

      A measure on a countable space is sigma-finite iff it gives finite mass to every singleton.

      See measure_singleton_lt_top for the forward direction without the countability assumption.

      instance MeasureTheory.Restrict.sigmaFinite {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [SigmaFinite μ] (s : Set α) :
      instance MeasureTheory.sum.sigmaFinite {α : Type u_1} {m0 : MeasurableSpace α} {ι : Type u_4} [Finite ι] (μ : ιMeasure α) [∀ (i : ι), SigmaFinite (μ i)] :
      instance MeasureTheory.Add.sigmaFinite {α : Type u_1} {m0 : MeasurableSpace α} (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] :
      SigmaFinite (μ + ν)
      instance MeasureTheory.SMul.sigmaFinite {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [SigmaFinite μ] (c : NNReal) :
      instance MeasureTheory.instSigmaFiniteRestrictInterSet {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} [SigmaFinite (μ.restrict s)] :
      theorem MeasureTheory.SigmaFinite.of_map {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] (μ : Measure α) {f : αβ} (hf : AEMeasurable f μ) (h : SigmaFinite (Measure.map f μ)) :
      theorem MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict' {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} (ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] (P : αProp) (h : ∀ (s : Set α), MeasurableSet sμ s < ν s < ∀ᵐ (x : α) μ.restrict s, P x) :
      ∀ᵐ (x : α) μ, P x

      Similar to ae_of_forall_measure_lt_top_ae_restrict, but where you additionally get the hypothesis that another σ-finite measure has finite values on s.

      theorem MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [SigmaFinite μ] (P : αProp) (h : ∀ (s : Set α), MeasurableSet sμ s < ∀ᵐ (x : α) μ.restrict s, P x) :
      ∀ᵐ (x : α) μ, P x

      To prove something for almost all x w.r.t. a σ-finite measure, it is sufficient to show that this holds almost everywhere in sets where the measure has finite value.

      Given S : μ.FiniteSpanningSetsIn {s | MeasurableSet s}, FiniteSpanningSetsIn.disjointed provides a FiniteSpanningSetsIn {s | MeasurableSet s} such that its underlying sets are pairwise disjoint.

      Equations