Documentation

Mathlib.MeasureTheory.OuterMeasure.Basic

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 α) :
μ (⋃ iI, 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 α) :
μ (⋃ iI, s i) iI, μ (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 α} :
μ (⋃ iI, s i) = 0 iI, μ (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 sS, μ 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 xs, μ {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 : xs, unhdsWithin 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) :
xs, tnhdsWithin 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]
@[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 (⋃ is, t i) = 0 is, 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 sS, 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 (⋃ it, s i) it, 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 : xs, unhdsWithin 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) :
xs, tnhdsWithin 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.ext_iff {α : Type u_1} {μ₁ : MeasureTheory.OuterMeasure α} {μ₂ : MeasureTheory.OuterMeasure α} :
μ₁ = μ₂ ∀ (s : Set α), μ₁ s = μ₂ 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'.