# Outer Measures #

An outer measure is a function `μ : Set α → ℝ≥0∞`, from the powerset of a type to the extended nonnegative real numbers that satisfies the following conditions:

1. `μ ∅ = 0`;
2. `μ` is monotone;
3. `μ` is countably subadditive. This means that the outer measure of a countable union is at most the sum of the outer measure on the individual sets.

Note that we do not need `α` to be measurable to define an outer measure.

## References #

https://en.wikipedia.org/wiki/Outer_measure

## Tags #

outer measure

source
@[simp]
theorem MeasureTheory.measure_empty {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} :
μ ∅ = 0
source
theorem MeasureTheory.measure_mono {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} {s t : Set α} (h : s ⊆ t) :
μ s ≤ μ t
source
theorem MeasureTheory.measure_mono_null {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} {s t : Set α} (h : s ⊆ t) (ht : μ t = 0) :
μ s = 0
source
theorem MeasureTheory.pos_mono {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} ⦃s t : Set α⦄ (h : s ⊆ t) (hs : 0 < μ s) :
0 < μ t
source
theorem MeasureTheory.measure_eq_top_mono {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} {s t : Set α} (h : s ⊆ t) (hs : μ s = ⊤) :
μ t = ⊤
source
theorem MeasureTheory.measure_lt_top_mono {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} {s t : Set α} (h : s ⊆ t) (ht : μ t < ⊤) :
μ s < ⊤
source
theorem MeasureTheory.measure_pos_of_superset {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} {s t : Set α} (h : s ⊆ t) (hs : μ s ≠ 0) :
0 < μ t
source
theorem MeasureTheory.measure_iUnion_le {α : Type u_1} {ι : Type u_2} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} [Countable ι] (s : ι → Set α) :
μ (⋃ (i : ι), s i) ≤ ∑' (i : ι), μ (s i)
source
theorem MeasureTheory.measure_biUnion_le {α : Type u_1} {ι : Type u_2} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {I : Set ι} (μ : F) (hI : I.Countable) (s : ι → Set α) :
μ (⋃ i ∈ I, s i) ≤ ∑' (i : ↑I), μ (s ↑i)
source
theorem MeasureTheory.measure_biUnion_finset_le {α : Type u_1} {ι : Type u_2} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} (I : Finset ι) (s : ι → Set α) :
μ (⋃ i ∈ I, s i) ≤ ∑ i ∈ I, μ (s i)
source
theorem MeasureTheory.measure_iUnion_fintype_le {α : Type u_1} {ι : Type u_2} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] [Fintype ι] (μ : F) (s : ι → Set α) :
μ (⋃ (i : ι), s i) ≤ ∑ i : ι, μ (s i)
source
theorem MeasureTheory.measure_union_le {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} (s t : Set α) :
μ (s ∪ t) ≤ μ s + μ t
source
theorem MeasureTheory.measure_univ_le_add_compl {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} (s : Set α) :
μ Set.univ ≤ μ s + μ s ᶜ
source
theorem MeasureTheory.measure_le_inter_add_diff {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] (μ : F) (s t : Set α) :
μ s ≤ μ (s ∩ t) + μ (s \ t)
source
theorem MeasureTheory.measure_diff_null {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} {s t : Set α} (ht : μ t = 0) :
μ (s \ t) = μ s
source
theorem MeasureTheory.measure_biUnion_null_iff {α : Type u_1} {ι : Type u_2} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} {I : Set ι} (hI : I.Countable) {s : ι → Set α} :
μ (⋃ i ∈ I, s i) = 0 ↔ ∀ i ∈ I, μ (s i) = 0
source
theorem MeasureTheory.measure_sUnion_null_iff {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} {S : Set (Set α)} (hS : S.Countable) :
μ (⋃₀ S) = 0 ↔ ∀ s ∈ S, μ s = 0
source
@[simp]
theorem MeasureTheory.measure_iUnion_null_iff {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} {ι : Sort u_4} [Countable ι] {s : ι → Set α} :
μ (⋃ (i : ι), s i) = 0 ↔ ∀ (i : ι), μ (s i) = 0
source
theorem MeasureTheory.measure_iUnion_null {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} {ι : Sort u_4} [Countable ι] {s : ι → Set α} :
(∀ (i : ι), μ (s i) = 0) → μ (⋃ (i : ι), s i) = 0

Alias of the reverse direction of `MeasureTheory.measure_iUnion_null_iff`.

source
@[simp]
theorem MeasureTheory.measure_union_null_iff {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} {s t : Set α} :
μ (s ∪ t) = 0 ↔ μ s = 0 ∧ μ t = 0
source
theorem MeasureTheory.measure_union_null {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} {s t : Set α} (hs : μ s = 0) (ht : μ t = 0) :
μ (s ∪ t) = 0
source
theorem MeasureTheory.measure_null_iff_singleton {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} {s : Set α} (hs : s.Countable) :
μ s = 0 ↔ ∀ x ∈ s, μ {x} = 0
source
theorem MeasureTheory.measure_iUnion_of_tendsto_zero {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {ι : Type u_4} (μ : F) {s : ι → Set α} (l : Filter ι) [l.NeBot] (h0 : Filter.Tendsto (fun (k : ι) => μ ((⋃ (n : ι), s n) \ s k)) l (nhds 0)) :
μ (⋃ (n : ι), s n) = ⨆ (n : ι), μ (s n)

Let `μ` be an (outer) measure; let `s : ι → Set α` be a sequence of sets, `S = ⋃ n, s n`. If `μ (S \ s n)` tends to zero along some nontrivial filter (usually `Filter.atTop` on `ι = ℕ`), then `μ S = ⨆ n, μ (s n)`.

source
theorem MeasureTheory.measure_null_of_locally_null {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} [TopologicalSpace α] [SecondCountableTopology α] (s : Set α) (hs : ∀ x ∈ s, ∃ u ∈ nhdsWithin x s, μ u = 0) :
μ s = 0

If a set has zero measure in a neighborhood of each of its points, then it has zero measure in a second-countable space.

source
theorem MeasureTheory.exists_mem_forall_mem_nhdsWithin_pos_measure {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} [TopologicalSpace α] [SecondCountableTopology α] {s : Set α} (hs : μ s ≠ 0) :
∃ x ∈ s, ∀ t ∈ nhdsWithin x s, 0 < μ t

If `m s ≠ 0`, then for some point `x ∈ s` and any `t ∈ 𝓝[s] x` we have `0 < m t`.

source
theorem MeasureTheory.OuterMeasure.iUnion_of_tendsto_zero {α : Type u_1} {ι : Type u_3} (m : OuterMeasure α) {s : ι → Set α} (l : Filter ι) [l.NeBot] (h0 : Filter.Tendsto (fun (k : ι) => m ((⋃ (n : ι), s n) \ s k)) l (nhds 0)) :
m (⋃ (n : ι), s n) = ⨆ (n : ι), m (s n)

If `s : ι → Set α` is a sequence of sets, `S = ⋃ n, s n`, and `m (S \ s n)` tends to zero along some nontrivial filter (usually `atTop` on `ι = ℕ`), then `m S = ⨆ n, m (s n)`.

source
theorem MeasureTheory.OuterMeasure.iUnion_nat_of_monotone_of_tsum_ne_top {α : Type u_1} (m : OuterMeasure α) {s : ℕ → Set α} (h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)) (h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤) :
m (⋃ (n : ℕ), s n) = ⨆ (n : ℕ), m (s n)

If `s : ℕ → Set α` is a monotone sequence of sets such that `∑' k, m (s (k + 1) \ s k) ≠ ∞`, then `m (⋃ n, s n) = ⨆ n, m (s n)`.

source
theorem MeasureTheory.OuterMeasure.coe_fn_injective {α : Type u_1} :
Function.Injective fun (μ : OuterMeasure α) (s : Set α) => μ s
source
theorem MeasureTheory.OuterMeasure.ext {α : Type u_1} {μ₁ μ₂ : OuterMeasure α} (h : ∀ (s : Set α), μ₁ s = μ₂ s) :
μ₁ = μ₂
source
theorem MeasureTheory.OuterMeasure.ext_iff {α : Type u_1} {μ₁ μ₂ : OuterMeasure α} :
μ₁ = μ₂ ↔ ∀ (s : Set α), μ₁ s = μ₂ s
source
theorem MeasureTheory.OuterMeasure.ext_nonempty {α : Type u_1} {μ₁ μ₂ : OuterMeasure α} (h : ∀ (s : Set α), s.Nonempty → μ₁ s = μ₂ s) :
μ₁ = μ₂

A version of `MeasureTheory.OuterMeasure.ext` that assumes `μ₁ s = μ₂ s` on all nonempty sets `s`, and gets `μ₁ ∅ = μ₂ ∅` from `MeasureTheory.OuterMeasure.empty'`.