The “almost everywhere” filter of co-null sets.

If μ is an outer measure or a measure on α, then MeasureTheory.ae μ is the filter of co-null sets: s ∈ ae μ ↔ μ sᶜ = 0.

In this file we define the filter and prove some basic theorems about it.

Notation

• ∀ᵐ x ∂μ, p x: the predicate p holds for μ-a.e. all x;
• ∃ᶠ x ∂μ, p x: the predicate p holds on a set of nonzero measure;
• f =ᵐ[μ] g: f x = g x for μ-a.e. all x;
• f ≤ᵐ[μ] g: f x ≤ g x for μ-a.e. all x.

Implementation details

All notation introduced in this file reducibly unfolds to the corresponding definitions about filters, so generic lemmas about Filter.Eventually, Filter.EventuallyEq etc apply. However, we restate some lemmas specifically for ae.

Tags

outer measure, measure, almost everywhere

def MeasureTheory.ae {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] (μ : F) : Filter α

The “almost everywhere” filter of co-null sets.

Equations

• MeasureTheory.ae μ = Filter.ofCountableUnion (fun (x : Set α) => μ x = 0) ⋯ ⋯

theorem MeasureTheory.mem_ae_iff {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} : s ∈ MeasureTheory.ae μ ↔ μ sᶜ = 0

theorem MeasureTheory.ae_iff {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {p : α → Prop} : (∀ᵐ (a : α) ∂μ, p a) ↔ μ {a : α | ¬p a} = 0

theorem MeasureTheory.compl_mem_ae_iff {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} : sᶜ ∈ MeasureTheory.ae μ ↔ μ s = 0

theorem MeasureTheory.frequently_ae_iff {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {p : α → Prop} : (∃ᵐ (a : α) ∂μ, p a) ↔ μ {a : α | p a} ≠ 0

theorem MeasureTheory.frequently_ae_mem_iff {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} : (∃ᵐ (a : α) ∂μ, a ∈ s) ↔ μ s ≠ 0

theorem MeasureTheory.measure_zero_iff_ae_nmem {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} : μ s = 0 ↔ ∀ᵐ (a : α) ∂μ, a ∉ s

theorem MeasureTheory.ae_of_all {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {p : α → Prop} (μ : F) : (∀ (a : α), p a) → ∀ᵐ (a : α) ∂μ, p a

instance MeasureTheory.instCountableInterFilter {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} : CountableInterFilter (MeasureTheory.ae μ)

Equations

• ⋯ = ⋯

theorem MeasureTheory.ae_all_iff {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {ι : Sort u_4} [Countable ι] {p : α → ι → Prop} : (∀ᵐ (a : α) ∂μ, ∀ (i : ι), p a i) ↔ ∀ (i : ι), ∀ᵐ (a : α) ∂μ, p a i

theorem MeasureTheory.all_ae_of {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {ι : Sort u_4} {p : α → ι → Prop} (hp : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), p a i) (i : ι) : ∀ᵐ (a : α) ∂μ, p a i

theorem MeasureTheory.ae_iff_of_countable {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} [Countable α] {p : α → Prop} : (∀ᵐ (x : α) ∂μ, p x) ↔ ∀ (x : α), μ {x} ≠ 0 → p x

theorem MeasureTheory.ae_ball_iff {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {ι : Type u_4} {S : Set ι} (hS : S.Countable) {p : α → (i : ι) → i ∈ S → Prop} : (∀ᵐ (x : α) ∂μ, ∀ (i : ι) (hi : i ∈ S), p x i hi) ↔ ∀ (i : ι) (hi : i ∈ S), ∀ᵐ (x : α) ∂μ, p x i hi

theorem MeasureTheory.ae_eq_refl {α : Type u_1} {β : Type u_2} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} (f : α → β) : f =ᵐ[μ] f

theorem MeasureTheory.ae_eq_rfl {α : Type u_1} {β : Type u_2} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {f : α → β} : f =ᵐ[μ] f

theorem MeasureTheory.ae_eq_comm {α : Type u_1} {β : Type u_2} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {f : α → β} {g : α → β} : f =ᵐ[μ] g ↔ g =ᵐ[μ] f

theorem MeasureTheory.ae_eq_symm {α : Type u_1} {β : Type u_2} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {f : α → β} {g : α → β} (h : f =ᵐ[μ] g) : g =ᵐ[μ] f

theorem MeasureTheory.ae_eq_trans {α : Type u_1} {β : Type u_2} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {f : α → β} {g : α → β} {h : α → β} (h₁ : f =ᵐ[μ] g) (h₂ : g =ᵐ[μ] h) : f =ᵐ[μ] h

@[simp]

theorem MeasureTheory.ae_eq_top {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} : MeasureTheory.ae μ = ⊤ ↔ ∀ (a : α), μ {a} ≠ 0

theorem MeasureTheory.ae_le_of_ae_lt {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {β : Type u_4} [Preorder β] {f : α → β} {g : α → β} (h : ∀ᵐ (x : α) ∂μ, f x < g x) : f ≤ᵐ[μ] g

@[simp]

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

@[simp]

theorem MeasureTheory.ae_eq_univ {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} : s =ᵐ[μ] Set.univ ↔ μ sᶜ = 0

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

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

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

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

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

theorem MeasureTheory.diff_null_ae_eq_self {α : 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.ae_eq_set {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} {t : Set α} : s =ᵐ[μ] t ↔ μ (s \ t) = 0 ∧ μ (t \ s) = 0

@[simp]

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

@[simp]

theorem MeasureTheory.ae_eq_set_compl_compl {α : 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.ae_eq_set_compl {α : 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.ae_eq_set_inter {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} {t : Set α} {s' : Set α} {t' : Set α} (h : s =ᵐ[μ] t) (h' : s' =ᵐ[μ] t') : s ∩ s' =ᵐ[μ] t ∩ t'

theorem MeasureTheory.ae_eq_set_union {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} {t : Set α} {s' : Set α} {t' : Set α} (h : s =ᵐ[μ] t) (h' : s' =ᵐ[μ] t') : s ∪ s' =ᵐ[μ] t ∪ t'

theorem MeasureTheory.union_ae_eq_univ_of_ae_eq_univ_left {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} {t : Set α} (h : s =ᵐ[μ] Set.univ) : s ∪ t =ᵐ[μ] Set.univ

theorem MeasureTheory.union_ae_eq_univ_of_ae_eq_univ_right {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} {t : Set α} (h : t =ᵐ[μ] Set.univ) : s ∪ t =ᵐ[μ] Set.univ

theorem MeasureTheory.union_ae_eq_right_of_ae_eq_empty {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} {t : Set α} (h : s =ᵐ[μ] ∅) : s ∪ t =ᵐ[μ] t

theorem MeasureTheory.union_ae_eq_left_of_ae_eq_empty {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} {t : Set α} (h : t =ᵐ[μ] ∅) : s ∪ t =ᵐ[μ] s

theorem MeasureTheory.inter_ae_eq_right_of_ae_eq_univ {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} {t : Set α} (h : s =ᵐ[μ] Set.univ) : s ∩ t =ᵐ[μ] t

theorem MeasureTheory.inter_ae_eq_left_of_ae_eq_univ {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} {t : Set α} (h : t =ᵐ[μ] Set.univ) : s ∩ t =ᵐ[μ] s

theorem MeasureTheory.inter_ae_eq_empty_of_ae_eq_empty_left {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} {t : Set α} (h : s =ᵐ[μ] ∅) : s ∩ t =ᵐ[μ] ∅

theorem MeasureTheory.inter_ae_eq_empty_of_ae_eq_empty_right {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} {t : Set α} (h : t =ᵐ[μ] ∅) : s ∩ t =ᵐ[μ] ∅

theorem Set.mulIndicator_ae_eq_one {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {M : Type u_4} [One M] {f : α → M} {s : Set α} : s.mulIndicator f =ᵐ[μ] 1 ↔ μ (s ∩ Function.mulSupport f) = 0

theorem Set.indicator_ae_eq_zero {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {M : Type u_4} [Zero M] {f : α → M} {s : Set α} : s.indicator f =ᵐ[μ] 0 ↔ μ (s ∩ Function.support f) = 0

theorem MeasureTheory.measure_mono_ae {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} {t : Set α} (H : s ≤ᵐ[μ] t) : μ s ≤ μ t

If s ⊆ t modulo a set of measure 0, then μ s ≤ μ t.

theorem Filter.EventuallyLE.measure_le {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} {t : Set α} (H : s ≤ᵐ[μ] t) : μ s ≤ μ t

Alias of MeasureTheory.measure_mono_ae.

---

If s ⊆ t modulo a set of measure 0, then μ s ≤ μ t.

theorem MeasureTheory.measure_congr {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} {t : Set α} (H : s =ᵐ[μ] t) : μ s = μ t

If two sets are equal modulo a set of measure zero, then μ s = μ t.

theorem Filter.EventuallyEq.measure_eq {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} {t : Set α} (H : s =ᵐ[μ] t) : μ s = μ t

Alias of MeasureTheory.measure_congr.

---

If two sets are equal modulo a set of measure zero, then μ s = μ t.

theorem MeasureTheory.measure_mono_null_ae {α : 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