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

def MeasureTheory.«term∀ᵐ_∂_,_».«delab_app.Filter.Eventually» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

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∃ᵐ_∂_,_».«delab_app.Filter.Frequently» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

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

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

This is notation for Filter.EventuallyEq (MeasureTheory.ae μ) f g.

Equations

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

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

f ≤ᵐ[μ] g means f is eventually less than g along the a.e. filter, i.e. f ≤ g away from a null set.

This is notation for Filter.EventuallyLE (MeasureTheory.ae μ) f g.

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_zero_iff_ae_nmem {α : 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

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

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 =ᶠ[ae μ] 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 =ᶠ[ae μ] 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 =ᶠ[ae μ] g ↔ g =ᶠ[ae μ] 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 =ᶠ[ae μ] g) : g =ᶠ[ae μ] 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 =ᶠ[ae μ] g) (h₂ : g =ᶠ[ae μ] h) : f =ᶠ[ae μ] h

@[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 ≤ᶠ[ae μ] g

@[simp]

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

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 =ᶠ[ae μ] s ↔ μ (s ∩ t) = 0

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 =ᶠ[ae μ] s

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

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 =ᶠ[ae μ] t) (h' : s' =ᶠ[ae μ] t') : s \ s' =ᶠ[ae μ] t \ t'

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 =ᶠ[ae μ] t) (h' : s' =ᶠ[ae μ] t') : symmDiff s s' =ᶠ[ae μ] 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 =ᶠ[ae μ] Set.univ) : s ∪ t =ᶠ[ae μ] 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 =ᶠ[ae μ] Set.univ) : s ∪ t =ᶠ[ae μ] 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 =ᶠ[ae μ] ∅) : s ∪ t =ᶠ[ae μ] 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 =ᶠ[ae μ] ∅) : s ∪ t =ᶠ[ae μ] 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 =ᶠ[ae μ] Set.univ) : s ∩ t =ᶠ[ae μ] 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 =ᶠ[ae μ] Set.univ) : s ∩ t =ᶠ[ae μ] 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 =ᶠ[ae μ] ∅) : s ∩ t =ᶠ[ae μ] ∅

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 =ᶠ[ae μ] ∅) : s ∩ t =ᶠ[ae μ] ∅

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