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] [OuterMeasureClass F α] (μ : F) : Filter α

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

Equations

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

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

def MeasureTheory.«term∀ᵐ_∂_,_» : Lean.ParserDescr

∀ᵐ a ∂μ, p a means that p a for a.e. a, i.e. p holds true away from a null set.

This is notation for Filter.Eventually p (MeasureTheory.ae μ).

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.«term∃ᵐ_∂_,_» : Lean.ParserDescr

∃ᵐ a ∂μ, p a means that p holds ∂μ-frequently, i.e. p holds on a set of positive measure.

This is notation for Filter.Frequently p (MeasureTheory.ae μ).

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.«term_=ᵐ[_]_» : Lean.TrailingParserDescr

x =ᵐ[μ] y means that x and y are eventually equal along the a.e. filter, i.e. x = y away from a null set.

This is Filter.EventuallyEq (MeasureTheory.ae μ) x y if x is a function and Filter.EventuallyEqSet (MeasureTheory.ae μ) x y if x is a set.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.«term_≤ᵐ[_]_» : Lean.TrailingParserDescr

x ≤ᵐ[μ] y means that x is eventually less than or equal to y along the a.e. filter, i.e. x ≤ y away from a null set.

This is Filter.EventuallyLE (MeasureTheory.ae μ) x y if x is a function and Filter.EventuallySubset (MeasureTheory.ae μ) x y if x is a set.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.delabAEEventuallyEq : Lean.PrettyPrinter.Delaborator.Delab

Delaborator printing Filter.EventuallyEq (MeasureTheory.ae μ) f g as f =ᵐ[μ] g.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.delabAEEventuallyEqSet : Lean.PrettyPrinter.Delaborator.Delab

Delaborator printing Filter.EventuallyEqSet (MeasureTheory.ae μ) s t as s =ᵐ[μ] t.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.delabAEEventuallyLE : Lean.PrettyPrinter.Delaborator.Delab

Delaborator printing Filter.EventuallyLE (MeasureTheory.ae μ) f g as f ≤ᵐ[μ] g.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.delabAEEventuallySubset : Lean.PrettyPrinter.Delaborator.Delab

Delaborator printing Filter.EventuallySubset (MeasureTheory.ae μ) s t as s ≤ᵐ[μ] t.

Equations

• One or more equations did not get rendered due to their size.

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

theorem MeasureTheory.ae_iff {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [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] [OuterMeasureClass F α] {μ : F} {s : Set α} : sᶜ ∈ ae μ ↔ μ s = 0

theorem MeasureTheory.frequently_ae_iff {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [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] [OuterMeasureClass F α] {μ : F} {s : Set α} : (∃ᵐ (a : α) ∂μ, a ∈ s) ↔ μ s ≠ 0

theorem MeasureTheory.measure_eq_zero_iff_ae_notMem {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [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] [OuterMeasureClass F α] {p : α → Prop} (μ : F) : (∀ (a : α), p a) → ∀ᵐ (a : α) ∂μ, p a

theorem MeasureTheory.ae_all_iff {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [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] [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] [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] [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] [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] [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] [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] [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] [OuterMeasureClass F α] {μ : F} {f g h : α → β} (h₁ : f =ᵐ[μ] g) (h₂ : g =ᵐ[μ] h) : f =ᵐ[μ] h

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

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

@[simp]

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

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

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

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

@[deprecated MeasureTheory.sdiff_ae_eq_self (since := "2026-06-03")]

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

Alias of MeasureTheory.sdiff_ae_eq_self.

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

@[deprecated MeasureTheory.sdiff_null_ae_eq_self (since := "2026-06-03")]

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

Alias of MeasureTheory.sdiff_null_ae_eq_self.

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

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

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

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

@[deprecated MeasureTheory.ae_eq_set_sdiff (since := "2026-06-03")]

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

Alias of MeasureTheory.ae_eq_set_sdiff.

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

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

theorem MeasureTheory.ae_eq_set_biInter {α : Type u_1} {β : Type u_2} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} {s : Set β} (hs : s.Countable) {t t' : β → Set α} (h : ∀ b ∈ s, t b =ᵐ[μ] t' b) : ⋂ b ∈ s, t b =ᵐ[μ] ⋂ b ∈ s, t' b

theorem MeasureTheory.ae_eq_set_biUnion {α : Type u_1} {β : Type u_2} {F : Type u_3} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} {s : Set β} (hs : s.Countable) {t t' : β → Set α} (h : ∀ b ∈ s, t b =ᵐ[μ] t' b) : ⋃ b ∈ s, t b =ᵐ[μ] ⋃ b ∈ s, t' b

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] [OuterMeasureClass F α] {μ : F} {s t : Set α} (H : s ≤ᵐ[μ] t) : μ s ≤ μ t

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

theorem Filter.EventuallySubset.measure_le {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s 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.

@[deprecated Filter.EventuallySubset.measure_le (since := "2026-08-14")]

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

Alias of Filter.EventuallySubset.measure_le.

---

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] [OuterMeasureClass F α] {μ : F} {s t : Set α} (H : s =ᵐ[μ] t) : μ s = μ t

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

theorem Filter.EventuallyEqSet.measure_eq {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s 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.

@[deprecated Filter.EventuallyEqSet.measure_eq (since := "2026-08-14")]

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

Alias of Filter.EventuallyEqSet.measure_eq.

---

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] [OuterMeasureClass F α] {μ : F} {s t : Set α} (H : s ≤ᵐ[μ] t) (ht : μ t = 0) : μ s = 0