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

@[simp]

theorem MeasureTheory.measure_empty {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} : μ ∅ = 0

theorem MeasureTheory.measure_mono {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} {t : Set α} (h : s ⊆ t) : μ s ≤ μ t

theorem MeasureTheory.measure_mono_null {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} {t : Set α} (h : s ⊆ t) (ht : μ t = 0) : μ s = 0

theorem MeasureTheory.measure_pos_of_superset {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} {t : Set α} (h : s ⊆ t) (hs : μ s ≠ 0) : 0 < μ t

theorem MeasureTheory.measure_iUnion_le {α : Type u_1} {ι : Type u_2} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} [Countable ι] (s : ι → Set α) : μ (⋃ (i : ι), s i) ≤ ∑' (i : ι), μ (s i)

theorem MeasureTheory.measure_biUnion_le {α : Type u_1} {ι : Type u_2} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {I : Set ι} (μ : F) (hI : I.Countable) (s : ι → Set α) : μ (⋃ i ∈ I, s i) ≤ ∑' (i : ↑I), μ (s ↑i)

theorem MeasureTheory.measure_biUnion_finset_le {α : Type u_1} {ι : Type u_2} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} (I : Finset ι) (s : ι → Set α) : μ (⋃ i ∈ I, s i) ≤ ∑ i ∈ I, μ (s i)

theorem MeasureTheory.measure_iUnion_fintype_le {α : Type u_1} {ι : Type u_2} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] [Fintype ι] (μ : F) (s : ι → Set α) : μ (⋃ (i : ι), s i) ≤ ∑ i : ι, μ (s i)

theorem MeasureTheory.measure_union_le {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} (s : Set α) (t : Set α) : μ (s ∪ t) ≤ μ s + μ t

theorem MeasureTheory.measure_univ_le_add_compl {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} (s : Set α) : μ Set.univ ≤ μ s + μ sᶜ

theorem MeasureTheory.measure_le_inter_add_diff {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] (μ : F) (s : Set α) (t : Set α) : μ s ≤ μ (s ∩ t) + μ (s \ t)

theorem MeasureTheory.measure_diff_null {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} {t : Set α} (ht : μ t = 0) : μ (s \ t) = μ s

theorem MeasureTheory.measure_biUnion_null_iff {α : Type u_1} {ι : Type u_2} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {I : Set ι} (hI : I.Countable) {s : ι → Set α} : μ (⋃ i ∈ I, s i) = 0 ↔ ∀ i ∈ I, μ (s i) = 0

theorem MeasureTheory.measure_sUnion_null_iff {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {S : Set (Set α)} (hS : S.Countable) : μ (⋃₀ S) = 0 ↔ ∀ s ∈ S, μ s = 0

@[simp]

theorem MeasureTheory.measure_iUnion_null_iff {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {ι : Sort u_4} [Countable ι] {s : ι → Set α} : μ (⋃ (i : ι), s i) = 0 ↔ ∀ (i : ι), μ (s i) = 0

theorem MeasureTheory.measure_iUnion_null {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.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.

@[simp]

theorem MeasureTheory.measure_union_null_iff {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} {t : Set α} : μ (s ∪ t) = 0 ↔ μ s = 0 ∧ μ t = 0

theorem MeasureTheory.measure_union_null {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} {t : Set α} (hs : μ s = 0) (ht : μ t = 0) : μ (s ∪ t) = 0

theorem MeasureTheory.measure_null_iff_singleton {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} (hs : s.Countable) : μ s = 0 ↔ ∀ x ∈ s, μ {x} = 0

theorem MeasureTheory.measure_iUnion_of_tendsto_zero {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.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).

theorem MeasureTheory.measure_null_of_locally_null {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.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.

theorem MeasureTheory.exists_mem_forall_mem_nhdsWithin_pos_measure {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.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.

@[deprecated MeasureTheory.measure_empty]

theorem MeasureTheory.OuterMeasure.empty' {α : Type u_1} (m : MeasureTheory.OuterMeasure α) : m ∅ = 0

@[deprecated MeasureTheory.measure_mono]

theorem MeasureTheory.OuterMeasure.mono' {α : Type u_1} (m : MeasureTheory.OuterMeasure α) {s₁ : Set α} {s₂ : Set α} (h : s₁ ⊆ s₂) : m s₁ ≤ m s₂

@[deprecated MeasureTheory.measure_mono_null]

theorem MeasureTheory.OuterMeasure.mono_null {α : Type u_1} (m : MeasureTheory.OuterMeasure α) {s : Set α} {t : Set α} (h : s ⊆ t) (ht : m t = 0) : m s = 0

@[deprecated MeasureTheory.measure_pos_of_superset]

theorem MeasureTheory.OuterMeasure.pos_of_subset_ne_zero {α : Type u_1} (m : MeasureTheory.OuterMeasure α) {a : Set α} {b : Set α} (hs : a ⊆ b) (hnz : m a ≠ 0) : 0 < m b

@[deprecated MeasureTheory.measure_iUnion_le]

theorem MeasureTheory.OuterMeasure.iUnion {α : Type u_1} (m : MeasureTheory.OuterMeasure α) {β : Type u_3} [Countable β] (s : β → Set α) : m (⋃ (i : β), s i) ≤ ∑' (i : β), m (s i)

@[deprecated MeasureTheory.measure_biUnion_null_iff]

theorem MeasureTheory.OuterMeasure.biUnion_null_iff {α : Type u_1} {β : Type u_2} (m : MeasureTheory.OuterMeasure α) {s : Set β} (hs : s.Countable) {t : β → Set α} : m (⋃ i ∈ s, t i) = 0 ↔ ∀ i ∈ s, m (t i) = 0

@[deprecated MeasureTheory.measure_sUnion_null_iff]

theorem MeasureTheory.OuterMeasure.sUnion_null_iff {α : Type u_1} (m : MeasureTheory.OuterMeasure α) {S : Set (Set α)} (hS : S.Countable) : m (⋃₀ S) = 0 ↔ ∀ s ∈ S, m s = 0

@[deprecated MeasureTheory.measure_iUnion_null_iff]

theorem MeasureTheory.OuterMeasure.iUnion_null_iff {α : Type u_1} {ι : Sort u_3} [Countable ι] (m : MeasureTheory.OuterMeasure α) {s : ι → Set α} : m (⋃ (i : ι), s i) = 0 ↔ ∀ (i : ι), m (s i) = 0

@[deprecated MeasureTheory.measure_iUnion_null]

theorem MeasureTheory.OuterMeasure.iUnion_null {α : Type u_1} {ι : Sort u_3} [Countable ι] (m : MeasureTheory.OuterMeasure α) {s : ι → Set α} : (∀ (i : ι), m (s i) = 0) → m (⋃ (i : ι), s i) = 0

Alias of the reverse direction of MeasureTheory.OuterMeasure.iUnion_null_iff.

@[deprecated]

theorem MeasureTheory.OuterMeasure.iUnion_null_iff' {α : Type u_1} (m : MeasureTheory.OuterMeasure α) {ι : Prop} {s : ι → Set α} : m (⋃ (i : ι), s i) = 0 ↔ ∀ (i : ι), m (s i) = 0

@[deprecated MeasureTheory.measure_biUnion_finset_le]

theorem MeasureTheory.OuterMeasure.iUnion_finset {α : Type u_1} {β : Type u_2} (m : MeasureTheory.OuterMeasure α) (s : β → Set α) (t : Finset β) : m (⋃ i ∈ t, s i) ≤ ∑ i ∈ t, m (s i)

@[deprecated MeasureTheory.measure_union_le]

theorem MeasureTheory.OuterMeasure.union {α : Type u_1} (m : MeasureTheory.OuterMeasure α) (s₁ : Set α) (s₂ : Set α) : m (s₁ ∪ s₂) ≤ m s₁ + m s₂

@[deprecated MeasureTheory.measure_null_of_locally_null]

theorem MeasureTheory.OuterMeasure.null_of_locally_null {α : Type u_1} [TopologicalSpace α] [SecondCountableTopology α] (m : MeasureTheory.OuterMeasure α) (s : Set α) (hs : ∀ x ∈ s, ∃ u ∈ nhdsWithin x s, m u = 0) : m 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.

@[deprecated MeasureTheory.exists_mem_forall_mem_nhdsWithin_pos_measure]

theorem MeasureTheory.OuterMeasure.exists_mem_forall_mem_nhds_within_pos {α : Type u_1} [TopologicalSpace α] [SecondCountableTopology α] (m : MeasureTheory.OuterMeasure α) {s : Set α} (hs : m s ≠ 0) : ∃ x ∈ s, ∀ t ∈ nhdsWithin x s, 0 < m t

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

theorem MeasureTheory.OuterMeasure.iUnion_of_tendsto_zero {α : Type u_1} {ι : Type u_3} (m : MeasureTheory.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).

theorem MeasureTheory.OuterMeasure.iUnion_nat_of_monotone_of_tsum_ne_top {α : Type u_1} (m : MeasureTheory.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).

@[deprecated MeasureTheory.measure_le_inter_add_diff]

theorem MeasureTheory.OuterMeasure.le_inter_add_diff {α : Type u_1} {m : MeasureTheory.OuterMeasure α} {t : Set α} (s : Set α) : m t ≤ m (t ∩ s) + m (t \ s)

@[deprecated MeasureTheory.measure_diff_null]

theorem MeasureTheory.OuterMeasure.diff_null {α : Type u_1} (m : MeasureTheory.OuterMeasure α) (s : Set α) {t : Set α} (ht : m t = 0) : m (s \ t) = m s

@[deprecated MeasureTheory.measure_union_null]

theorem MeasureTheory.OuterMeasure.union_null {α : Type u_1} (m : MeasureTheory.OuterMeasure α) {s₁ : Set α} {s₂ : Set α} (h₁ : m s₁ = 0) (h₂ : m s₂ = 0) : m (s₁ ∪ s₂) = 0

theorem MeasureTheory.OuterMeasure.coe_fn_injective {α : Type u_1} : Function.Injective fun (μ : MeasureTheory.OuterMeasure α) (s : Set α) => μ s

theorem MeasureTheory.OuterMeasure.ext {α : Type u_1} {μ₁ : MeasureTheory.OuterMeasure α} {μ₂ : MeasureTheory.OuterMeasure α} (h : ∀ (s : Set α), μ₁ s = μ₂ s) : μ₁ = μ₂

theorem MeasureTheory.OuterMeasure.ext_nonempty {α : Type u_1} {μ₁ : MeasureTheory.OuterMeasure α} {μ₂ : MeasureTheory.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'.