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] [OuterMeasureClass F α] {μ : F} : μ ∅ = 0

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

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

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

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)

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)

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)

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)

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

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ᶜ

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)

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

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

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

@[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

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.

@[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

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

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

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).

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.

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.

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).

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).

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

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

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'.