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.

References

• https://en.wikipedia.org/wiki/Outer_measure
• https://en.wikipedia.org/wiki/Carath%C3%A9odory%27s_criterion

Tags

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

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

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

• MeasureTheory.OuterMeasure.ofFunction m m_empty = { measureOf := fun (s : Set α) => ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i), empty := ⋯, mono := ⋯, iUnion_nat := ⋯ }

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 s → m 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 α) : (MeasureTheory.OuterMeasure.ofFunction m m_empty) 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 ⊆ t → m s ≤ m t) (m_subadd : ∀ (s : ℕ → Set α), m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), m (s i)) : (MeasureTheory.OuterMeasure.ofFunction m m_empty) s = m s

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} : IsGreatest {μ : MeasureTheory.OuterMeasure α | ∀ (s : Set α), μ s ≤ m s} (MeasureTheory.OuterMeasure.ofFunction m m_empty)

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).Nonempty → m u = ⊤) : (MeasureTheory.OuterMeasure.ofFunction m m_empty) (s ∪ t) = (MeasureTheory.OuterMeasure.ofFunction m m_empty) s + (MeasureTheory.OuterMeasure.ofFunction m m_empty) 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 : Monotone m ∨ Function.Surjective f) : (MeasureTheory.OuterMeasure.comap f) (MeasureTheory.OuterMeasure.ofFunction m m_empty) = 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.map f) (MeasureTheory.OuterMeasure.ofFunction m m_empty) ≤ 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 : Function.Injective f) : (MeasureTheory.OuterMeasure.map f) (MeasureTheory.OuterMeasure.ofFunction m m_empty) = 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 : Monotone m) : (MeasureTheory.OuterMeasure.restrict s) (MeasureTheory.OuterMeasure.ofFunction m m_empty) = 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 • MeasureTheory.OuterMeasure.ofFunction m m_empty = MeasureTheory.OuterMeasure.ofFunction (c • m) ⋯

def MeasureTheory.OuterMeasure.boundedBy {α : Type u_1} (m : Set α → ENNReal) : MeasureTheory.OuterMeasure α

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

• MeasureTheory.OuterMeasure.boundedBy m = MeasureTheory.OuterMeasure.ofFunction (fun (s : Set α) => ⨆ (_ : s.Nonempty), m s) ⋯

theorem MeasureTheory.OuterMeasure.boundedBy_le {α : Type u_1} {m : Set α → ENNReal} (s : Set α) : (MeasureTheory.OuterMeasure.boundedBy m) s ≤ m s

theorem MeasureTheory.OuterMeasure.boundedBy_eq_ofFunction {α : Type u_1} {m : Set α → ENNReal} (m_empty : m ∅ = 0) (s : Set α) : (MeasureTheory.OuterMeasure.boundedBy m) s = (MeasureTheory.OuterMeasure.ofFunction m m_empty) s

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 ⊆ t → m s ≤ m t) (m_subadd : ∀ (s : ℕ → Set α), m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), m (s i)) : (MeasureTheory.OuterMeasure.boundedBy m) s = m s

@[simp]

theorem MeasureTheory.OuterMeasure.boundedBy_eq_self {α : Type u_1} (m : MeasureTheory.OuterMeasure α) : MeasureTheory.OuterMeasure.boundedBy ⇑m = m

theorem MeasureTheory.OuterMeasure.le_boundedBy {α : Type u_1} {m : Set α → ENNReal} {μ : MeasureTheory.OuterMeasure α} : μ ≤ MeasureTheory.OuterMeasure.boundedBy m ↔ ∀ (s : Set α), μ s ≤ m s

theorem MeasureTheory.OuterMeasure.le_boundedBy' {α : Type u_1} {m : Set α → ENNReal} {μ : MeasureTheory.OuterMeasure α} : μ ≤ MeasureTheory.OuterMeasure.boundedBy m ↔ ∀ (s : Set α), s.Nonempty → μ s ≤ m s

@[simp]

theorem MeasureTheory.OuterMeasure.boundedBy_top {α : Type u_1} : MeasureTheory.OuterMeasure.boundedBy ⊤ = ⊤

@[simp]

theorem MeasureTheory.OuterMeasure.boundedBy_zero {α : Type u_1} : MeasureTheory.OuterMeasure.boundedBy 0 = 0

theorem MeasureTheory.OuterMeasure.smul_boundedBy {α : Type u_1} {m : Set α → ENNReal} {c : ENNReal} (hc : c ≠ ⊤) : c • MeasureTheory.OuterMeasure.boundedBy m = MeasureTheory.OuterMeasure.boundedBy (c • m)

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) : (MeasureTheory.OuterMeasure.comap f) (MeasureTheory.OuterMeasure.boundedBy m) = 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).Nonempty → m u = ⊤) : (MeasureTheory.OuterMeasure.boundedBy m) (s ∪ t) = (MeasureTheory.OuterMeasure.boundedBy m) s + (MeasureTheory.OuterMeasure.boundedBy m) 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.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 : Set (MeasureTheory.OuterMeasure α)) (s : Set α) : ENNReal

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

• MeasureTheory.OuterMeasure.sInfGen m s = ⨅ μ ∈ m, μ s

theorem MeasureTheory.OuterMeasure.sInfGen_def {α : Type u_1} (m : Set (MeasureTheory.OuterMeasure α)) (t : Set α) : MeasureTheory.OuterMeasure.sInfGen m t = ⨅ μ ∈ m, μ t

theorem MeasureTheory.OuterMeasure.sInf_eq_boundedBy_sInfGen {α : Type u_1} (m : Set (MeasureTheory.OuterMeasure α)) : sInf m = MeasureTheory.OuterMeasure.boundedBy (MeasureTheory.OuterMeasure.sInfGen m)

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 α) : (⨅ i ∈ I, m i) s = ⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ i ∈ 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.biInf_apply' {α : Type u_1} {ι : Type u_2} (I : Set ι) (m : ι → MeasureTheory.OuterMeasure α) {s : Set α} (hs : s.Nonempty) : (⨅ i ∈ I, m i) s = ⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ i ∈ 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.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 α) : (MeasureTheory.OuterMeasure.map f) (⨅ (i : ι), m i) = (MeasureTheory.OuterMeasure.restrict (Set.range f)) (⨅ (i : ι), (MeasureTheory.OuterMeasure.map f) (m i))

theorem MeasureTheory.OuterMeasure.map_iInf_comap {α : Type u_1} {ι : Sort u_2} {β : Type u_3} [Nonempty ι] {f : α → β} (m : ι → MeasureTheory.OuterMeasure β) : (MeasureTheory.OuterMeasure.map f) (⨅ (i : ι), (MeasureTheory.OuterMeasure.comap f) (m i)) = ⨅ (i : ι), (MeasureTheory.OuterMeasure.map f) ((MeasureTheory.OuterMeasure.comap f) (m i))

theorem MeasureTheory.OuterMeasure.map_biInf_comap {α : Type u_1} {ι : Type u_2} {β : Type u_3} {I : Set ι} (hI : I.Nonempty) {f : α → β} (m : ι → MeasureTheory.OuterMeasure β) : (MeasureTheory.OuterMeasure.map f) (⨅ i ∈ I, (MeasureTheory.OuterMeasure.comap f) (m i)) = ⨅ i ∈ I, (MeasureTheory.OuterMeasure.map f) ((MeasureTheory.OuterMeasure.comap f) (m i))

theorem MeasureTheory.OuterMeasure.restrict_iInf_restrict {α : Type u_1} {ι : Sort u_2} (s : Set α) (m : ι → MeasureTheory.OuterMeasure α) : (MeasureTheory.OuterMeasure.restrict s) (⨅ (i : ι), (MeasureTheory.OuterMeasure.restrict s) (m i)) = (MeasureTheory.OuterMeasure.restrict s) (⨅ (i : ι), m i)

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) (⨅ i ∈ I, m i) = ⨅ i ∈ I, (MeasureTheory.OuterMeasure.restrict s) (m i)

theorem MeasureTheory.OuterMeasure.restrict_sInf_eq_sInf_restrict {α : Type u_1} (m : Set (MeasureTheory.OuterMeasure α)) {s : Set α} (hm : m.Nonempty) : (MeasureTheory.OuterMeasure.restrict s) (sInf m) = sInf (⇑(MeasureTheory.OuterMeasure.restrict s) '' m)

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