Documentation

Mathlib.MeasureTheory.OuterMeasure.OfFunction

Outer measures from functions #

Given an arbitrary function m : Set α → ℝ≥0∞ that sends to 0 we can define an outer measure on α that on s is defined to be the infimum of ∑ᵢ, m (sᵢ) for all collections of sets sᵢ that cover s. This is the unique maximal outer measure that is at most the given function.

Given an outer measure m, the Carathéodory-measurable sets are the sets s such that for all sets t we have m t = m (t ∩ s) + m (t \ s). This forms a measurable space.

Main definitions and statements #

References #

Tags #

outer measure, Carathéodory-measurable, Carathéodory's criterion

def MeasureTheory.OuterMeasure.ofFunction {α : Type u_1} (m : Set αENNReal) (m_empty : m = 0) :

Given any function m assigning measures to sets satisfying m ∅ = 0, there is a unique maximal outer measure μ satisfying μ s ≤ m s for all s : Set α.

Equations
Instances For
    theorem MeasureTheory.OuterMeasure.ofFunction_apply {α : Type u_1} (m : Set αENNReal) (m_empty : m = 0) (s : Set α) :
    (MeasureTheory.OuterMeasure.ofFunction m m_empty) s = ⨅ (t : Set α), ⨅ (_ : s Set.iUnion t), ∑' (n : ), m (t n)

    ofFunction of a set s is the infimum of ∑ᵢ, m (tᵢ) for all collections of sets tᵢ that cover s.

    theorem MeasureTheory.OuterMeasure.ofFunction_eq_iInf_mem {α : Type u_1} (m : Set αENNReal) (m_empty : m = 0) {P : Set αProp} (m_top : ∀ (s : Set α), ¬P sm s = ) (s : Set α) :
    (MeasureTheory.OuterMeasure.ofFunction m m_empty) s = ⨅ (t : Set α), ⨅ (_ : ∀ (i : ), P (t i)), ⨅ (_ : s ⋃ (i : ), t i), ∑' (i : ), m (t i)

    ofFunction of a set s is the infimum of ∑ᵢ, m (tᵢ) for all collections of sets tᵢ that cover s, with all tᵢ satisfying a predicate P such that m is infinite for sets that don't satisfy P. This is similar to ofFunction_apply, except that the sets tᵢ satisfy P. The hypothesis m_top applies in particular to a function of the form extend m'.

    theorem MeasureTheory.OuterMeasure.ofFunction_le {α : Type u_1} {m : Set αENNReal} {m_empty : m = 0} (s : Set α) :
    theorem MeasureTheory.OuterMeasure.ofFunction_eq {α : Type u_1} {m : Set αENNReal} {m_empty : m = 0} (s : Set α) (m_mono : ∀ ⦃t : Set α⦄, s tm s m t) (m_subadd : ∀ (s : Set α), m (⋃ (i : ), s i) ∑' (i : ), m (s i)) :
    theorem MeasureTheory.OuterMeasure.le_ofFunction {α : Type u_1} {m : Set αENNReal} {m_empty : m = 0} {μ : MeasureTheory.OuterMeasure α} :
    μ MeasureTheory.OuterMeasure.ofFunction m m_empty ∀ (s : Set α), μ s m s
    theorem MeasureTheory.OuterMeasure.isGreatest_ofFunction {α : Type u_1} {m : Set αENNReal} {m_empty : m = 0} :
    theorem MeasureTheory.OuterMeasure.ofFunction_eq_sSup {α : Type u_1} {m : Set αENNReal} {m_empty : m = 0} :
    MeasureTheory.OuterMeasure.ofFunction m m_empty = sSup {μ : MeasureTheory.OuterMeasure α | ∀ (s : Set α), μ s m s}
    theorem MeasureTheory.OuterMeasure.ofFunction_union_of_top_of_nonempty_inter {α : Type u_1} {m : Set αENNReal} {m_empty : m = 0} {s : Set α} {t : Set α} (h : ∀ (u : Set α), (s u).Nonempty(t u).Nonemptym u = ) :

    If m u = ∞ for any set u that has nonempty intersection both with s and t, then μ (s ∪ t) = μ s + μ t, where μ = MeasureTheory.OuterMeasure.ofFunction m m_empty.

    E.g., if α is an (e)metric space and m u = ∞ on any set of diameter ≥ r, then this lemma implies that μ (s ∪ t) = μ s + μ t on any two sets such that r ≤ edist x y for all x ∈ s and y ∈ t.

    theorem MeasureTheory.OuterMeasure.comap_ofFunction {α : Type u_1} {m : Set αENNReal} {m_empty : m = 0} {β : Type u_2} (f : βα) (h : Monotone m Function.Surjective f) :
    theorem MeasureTheory.OuterMeasure.map_ofFunction_le {α : Type u_1} {m : Set αENNReal} {m_empty : m = 0} {β : Type u_2} (f : αβ) :
    theorem MeasureTheory.OuterMeasure.map_ofFunction {α : Type u_1} {m : Set αENNReal} {m_empty : m = 0} {β : Type u_2} {f : αβ} (hf : Function.Injective f) :

    Given any function m assigning measures to sets, there is a unique maximal outer measure μ satisfying μ s ≤ m s for all s : Set α. This is the same as OuterMeasure.ofFunction, except that it doesn't require m ∅ = 0.

    Equations
    Instances For
      theorem MeasureTheory.OuterMeasure.boundedBy_apply {α : Type u_1} {m : Set αENNReal} (s : Set α) :
      (MeasureTheory.OuterMeasure.boundedBy m) s = ⨅ (t : Set α), ⨅ (_ : s Set.iUnion t), ∑' (n : ), ⨆ (_ : (t n).Nonempty), m (t n)
      theorem MeasureTheory.OuterMeasure.boundedBy_eq {α : Type u_1} {m : Set αENNReal} (s : Set α) (m_empty : m = 0) (m_mono : ∀ ⦃t : Set α⦄, s tm s m t) (m_subadd : ∀ (s : Set α), m (⋃ (i : ), s i) ∑' (i : ), m (s i)) :
      theorem MeasureTheory.OuterMeasure.le_boundedBy' {α : Type u_1} {m : Set αENNReal} {μ : MeasureTheory.OuterMeasure α} :
      μ MeasureTheory.OuterMeasure.boundedBy m ∀ (s : Set α), s.Nonemptyμ s m s
      theorem MeasureTheory.OuterMeasure.comap_boundedBy {α : Type u_1} {m : Set αENNReal} {β : Type u_2} (f : βα) (h : (Monotone fun (s : { s : Set α // s.Nonempty }) => m s) Function.Surjective f) :
      theorem MeasureTheory.OuterMeasure.boundedBy_union_of_top_of_nonempty_inter {α : Type u_1} {m : Set αENNReal} {s : Set α} {t : Set α} (h : ∀ (u : Set α), (s u).Nonempty(t u).Nonemptym u = ) :

      If m u = ∞ for any set u that has nonempty intersection both with s and t, then μ (s ∪ t) = μ s + μ t, where μ = MeasureTheory.OuterMeasure.boundedBy m.

      E.g., if α is an (e)metric space and m u = ∞ on any set of diameter ≥ r, then this lemma implies that μ (s ∪ t) = μ s + μ t on any two sets such that r ≤ edist x y for all x ∈ s and y ∈ t.

      Given a set of outer measures, we define a new function that on a set s is defined to be the infimum of μ(s) for the outer measures μ in the collection. We ensure that this function is defined to be 0 on , even if the collection of outer measures is empty. The outer measure generated by this function is the infimum of the given outer measures.

      Equations
      Instances For
        theorem MeasureTheory.OuterMeasure.iSup_sInfGen_nonempty {α : Type u_1} {m : Set (MeasureTheory.OuterMeasure α)} (h : m.Nonempty) (t : Set α) :
        ⨆ (_ : t.Nonempty), MeasureTheory.OuterMeasure.sInfGen m t = μm, μ t
        theorem MeasureTheory.OuterMeasure.sInf_apply {α : Type u_1} {m : Set (MeasureTheory.OuterMeasure α)} {s : Set α} (h : m.Nonempty) :
        (sInf m) s = ⨅ (t : Set α), ⨅ (_ : s Set.iUnion t), ∑' (n : ), μm, μ (t n)

        The value of the Infimum of a nonempty set of outer measures on a set is not simply the minimum value of a measure on that set: it is the infimum sum of measures of countable set of sets that covers that set, where a different measure can be used for each set in the cover.

        theorem MeasureTheory.OuterMeasure.sInf_apply' {α : Type u_1} {m : Set (MeasureTheory.OuterMeasure α)} {s : Set α} (h : s.Nonempty) :
        (sInf m) s = ⨅ (t : Set α), ⨅ (_ : s Set.iUnion t), ∑' (n : ), μm, μ (t n)

        The value of the Infimum of a set of outer measures on a nonempty set is not simply the minimum value of a measure on that set: it is the infimum sum of measures of countable set of sets that covers that set, where a different measure can be used for each set in the cover.

        theorem MeasureTheory.OuterMeasure.iInf_apply {α : Type u_1} {ι : Sort u_2} [Nonempty ι] (m : ιMeasureTheory.OuterMeasure α) (s : Set α) :
        (⨅ (i : ι), m i) s = ⨅ (t : Set α), ⨅ (_ : s Set.iUnion t), ∑' (n : ), ⨅ (i : ι), (m i) (t n)

        The value of the Infimum of a nonempty family of outer measures on a set is not simply the minimum value of a measure on that set: it is the infimum sum of measures of countable set of sets that covers that set, where a different measure can be used for each set in the cover.

        theorem MeasureTheory.OuterMeasure.iInf_apply' {α : Type u_1} {ι : Sort u_2} (m : ιMeasureTheory.OuterMeasure α) {s : Set α} (hs : s.Nonempty) :
        (⨅ (i : ι), m i) s = ⨅ (t : Set α), ⨅ (_ : s Set.iUnion t), ∑' (n : ), ⨅ (i : ι), (m i) (t n)

        The value of the Infimum of a family of outer measures on a nonempty set is not simply the minimum value of a measure on that set: it is the infimum sum of measures of countable set of sets that covers that set, where a different measure can be used for each set in the cover.

        theorem MeasureTheory.OuterMeasure.biInf_apply {α : Type u_1} {ι : Type u_2} {I : Set ι} (hI : I.Nonempty) (m : ιMeasureTheory.OuterMeasure α) (s : Set α) :
        (⨅ iI, m i) s = ⨅ (t : Set α), ⨅ (_ : s Set.iUnion t), ∑' (n : ), iI, (m i) (t n)

        The value of the Infimum of a nonempty family of outer measures on a set is not simply the minimum value of a measure on that set: it is the infimum sum of measures of countable set of sets that covers that set, where a different measure can be used for each set in the cover.

        theorem MeasureTheory.OuterMeasure.biInf_apply' {α : Type u_1} {ι : Type u_2} (I : Set ι) (m : ιMeasureTheory.OuterMeasure α) {s : Set α} (hs : s.Nonempty) :
        (⨅ iI, m i) s = ⨅ (t : Set α), ⨅ (_ : s Set.iUnion t), ∑' (n : ), iI, (m i) (t n)

        The value of the Infimum of a nonempty family of outer measures on a set is not simply the minimum value of a measure on that set: it is the infimum sum of measures of countable set of sets that covers that set, where a different measure can be used for each set in the cover.

        theorem MeasureTheory.OuterMeasure.map_iInf_le {α : Type u_1} {ι : Sort u_2} {β : Type u_3} (f : αβ) (m : ιMeasureTheory.OuterMeasure α) :
        (MeasureTheory.OuterMeasure.map f) (⨅ (i : ι), m i) ⨅ (i : ι), (MeasureTheory.OuterMeasure.map f) (m i)
        theorem MeasureTheory.OuterMeasure.comap_iInf {α : Type u_1} {ι : Sort u_2} {β : Type u_3} (f : αβ) (m : ιMeasureTheory.OuterMeasure β) :
        (MeasureTheory.OuterMeasure.comap f) (⨅ (i : ι), m i) = ⨅ (i : ι), (MeasureTheory.OuterMeasure.comap f) (m i)
        theorem MeasureTheory.OuterMeasure.map_iInf {α : Type u_1} {ι : Sort u_2} {β : Type u_3} {f : αβ} (hf : Function.Injective f) (m : ιMeasureTheory.OuterMeasure α) :
        theorem MeasureTheory.OuterMeasure.map_iInf_comap {α : Type u_1} {ι : Sort u_2} {β : Type u_3} [Nonempty ι] {f : αβ} (m : ιMeasureTheory.OuterMeasure β) :
        theorem MeasureTheory.OuterMeasure.map_biInf_comap {α : Type u_1} {ι : Type u_2} {β : Type u_3} {I : Set ι} (hI : I.Nonempty) {f : αβ} (m : ιMeasureTheory.OuterMeasure β) :
        theorem MeasureTheory.OuterMeasure.restrict_iInf {α : Type u_1} {ι : Sort u_2} [Nonempty ι] (s : Set α) (m : ιMeasureTheory.OuterMeasure α) :
        (MeasureTheory.OuterMeasure.restrict s) (⨅ (i : ι), m i) = ⨅ (i : ι), (MeasureTheory.OuterMeasure.restrict s) (m i)
        theorem MeasureTheory.OuterMeasure.restrict_biInf {α : Type u_1} {ι : Type u_2} {I : Set ι} (hI : I.Nonempty) (s : Set α) (m : ιMeasureTheory.OuterMeasure α) :
        (MeasureTheory.OuterMeasure.restrict s) (⨅ iI, m i) = iI, (MeasureTheory.OuterMeasure.restrict s) (m i)

        This proves that Inf and restrict commute for outer measures, so long as the set of outer measures is nonempty.