# 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 #

• OuterMeasure.boundedBy is the greatest outer measure that is at most the given function. If you know that the given function sends ∅ to 0, then OuterMeasure.ofFunction is a special case.
• sInf_eq_boundedBy_sInfGen is a characterization of the infimum of outer measures.

## 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 satisying m ∅ = 0, there is a unique maximal outer measure μ satisfying μ s ≤ m s for all s : Set α.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem MeasureTheory.OuterMeasure.ofFunction_apply {α : Type u_1} (m : Set αENNReal) (m_empty : m = 0) (s : Set α) :
() s = ⨅ (t : Set α), ⨅ (_ : s ), ∑' (n : ), m (t n)
theorem MeasureTheory.OuterMeasure.ofFunction_le {α : Type u_1} {m : Set αENNReal} {m_empty : m = 0} (s : Set α) :
() s m s
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)) :
() s = m s
theorem MeasureTheory.OuterMeasure.le_ofFunction {α : Type u_1} {m : Set αENNReal} {m_empty : m = 0} {μ : } :
μ ∀ (s : Set α), μ s m s
theorem MeasureTheory.OuterMeasure.isGreatest_ofFunction {α : Type u_1} {m : Set αENNReal} {m_empty : m = 0} :
IsGreatest {μ : | ∀ (s : Set α), μ s m s} ()
theorem MeasureTheory.OuterMeasure.ofFunction_eq_sSup {α : Type u_1} {m : Set αENNReal} {m_empty : m = 0} :
= sSup {μ : | ∀ (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 = ) :
() (s t) = () s + () t

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 : ) :
= MeasureTheory.OuterMeasure.ofFunction (fun (s : Set β) => m (f '' s))
theorem MeasureTheory.OuterMeasure.map_ofFunction_le {α : Type u_1} {m : Set αENNReal} {m_empty : m = 0} {β : Type u_2} (f : αβ) :
MeasureTheory.OuterMeasure.ofFunction (fun (s : Set β) => m (f ⁻¹' s)) m_empty
theorem MeasureTheory.OuterMeasure.map_ofFunction {α : Type u_1} {m : Set αENNReal} {m_empty : m = 0} {β : Type u_2} {f : αβ} (hf : ) :
= MeasureTheory.OuterMeasure.ofFunction (fun (s : Set β) => m (f ⁻¹' s)) m_empty
theorem MeasureTheory.OuterMeasure.restrict_ofFunction {α : Type u_1} {m : Set αENNReal} {m_empty : m = 0} (s : Set α) (hm : ) :
= MeasureTheory.OuterMeasure.ofFunction (fun (t : Set α) => m (t s))
theorem MeasureTheory.OuterMeasure.smul_ofFunction {α : Type u_1} {m : Set αENNReal} {m_empty : m = 0} {c : ENNReal} (hc : c ) :
c =

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_le {α : Type u_1} {m : Set αENNReal} (s : Set α) :
theorem MeasureTheory.OuterMeasure.boundedBy_eq_ofFunction {α : Type u_1} {m : Set αENNReal} (m_empty : m = 0) (s : Set α) :
= () s
theorem MeasureTheory.OuterMeasure.boundedBy_apply {α : Type u_1} {m : Set αENNReal} (s : Set α) :
= ⨅ (t : Set α), ⨅ (_ : s ), ∑' (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)) :
@[simp]
theorem MeasureTheory.OuterMeasure.le_boundedBy {α : Type u_1} {m : Set αENNReal} {μ : } :
∀ (s : Set α), μ s m s
theorem MeasureTheory.OuterMeasure.le_boundedBy' {α : Type u_1} {m : Set αENNReal} {μ : } :
∀ (s : Set α), s.Nonemptyμ s m s
theorem MeasureTheory.OuterMeasure.smul_boundedBy {α : Type u_1} {m : Set αENNReal} {c : ENNReal} (hc : c ) :
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) ) :
= MeasureTheory.OuterMeasure.boundedBy fun (s : Set β) => m (f '' s)
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.

def MeasureTheory.OuterMeasure.sInfGen {α : Type u_1} (m : ) (s : Set α) :

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
• = μm, μ s
Instances For
theorem MeasureTheory.OuterMeasure.sInfGen_def {α : Type u_1} (m : ) (t : Set α) :
= μm, μ t
theorem MeasureTheory.OuterMeasure.iSup_sInfGen_nonempty {α : Type u_1} {m : } (h : m.Nonempty) (t : Set α) :
⨆ (_ : t.Nonempty), = μm, μ t
theorem MeasureTheory.OuterMeasure.sInf_apply {α : Type u_1} {m : } {s : Set α} (h : m.Nonempty) :
(sInf m) s = ⨅ (t : Set α), ⨅ (_ : s ), ∑' (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 : } {s : Set α} (h : s.Nonempty) :
(sInf m) s = ⨅ (t : Set α), ⨅ (_ : s ), ∑' (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} [] (m : ) (s : Set α) :
(⨅ (i : ι), m i) s = ⨅ (t : Set α), ⨅ (_ : s ), ∑' (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 : ) {s : Set α} (hs : s.Nonempty) :
(⨅ (i : ι), m i) s = ⨅ (t : Set α), ⨅ (_ : s ), ∑' (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 : ) (s : Set α) :
(iI, m i) s = ⨅ (t : Set α), ⨅ (_ : s ), ∑' (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 : ) {s : Set α} (hs : s.Nonempty) :
(iI, m i) s = ⨅ (t : Set α), ⨅ (_ : s ), ∑' (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 : ) :
(⨅ (i : ι), m i) ⨅ (i : ι), (m i)
theorem MeasureTheory.OuterMeasure.comap_iInf {α : Type u_1} {ι : Sort u_2} {β : Type u_3} (f : αβ) (m : ) :
(⨅ (i : ι), m i) = ⨅ (i : ι), (m i)
theorem MeasureTheory.OuterMeasure.map_iInf {α : Type u_1} {ι : Sort u_2} {β : Type u_3} {f : αβ} (hf : ) (m : ) :
(⨅ (i : ι), m i) = (⨅ (i : ι), (m i))
theorem MeasureTheory.OuterMeasure.map_iInf_comap {α : Type u_1} {ι : Sort u_2} {β : Type u_3} [] {f : αβ} (m : ) :
(⨅ (i : ι), (m i)) = ⨅ (i : ι), ( (m i))
theorem MeasureTheory.OuterMeasure.map_biInf_comap {α : Type u_1} {ι : Type u_2} {β : Type u_3} {I : Set ι} (hI : I.Nonempty) {f : αβ} (m : ) :
(iI, (m i)) = iI, ( (m i))
theorem MeasureTheory.OuterMeasure.restrict_iInf_restrict {α : Type u_1} {ι : Sort u_2} (s : Set α) (m : ) :
(⨅ (i : ι), (m i)) = (⨅ (i : ι), m i)
theorem MeasureTheory.OuterMeasure.restrict_iInf {α : Type u_1} {ι : Sort u_2} [] (s : Set α) (m : ) :
(⨅ (i : ι), m i) = ⨅ (i : ι), (m i)
theorem MeasureTheory.OuterMeasure.restrict_biInf {α : Type u_1} {ι : Type u_2} {I : Set ι} (hI : I.Nonempty) (s : Set α) (m : ) :
(iI, m i) = iI, (m i)
theorem MeasureTheory.OuterMeasure.restrict_sInf_eq_sInf_restrict {α : Type u_1} (m : ) {s : Set α} (hm : m.Nonempty) :

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