# 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] (μ : F) :

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

Equations
Instances For

Pretty printer defined by notation3 command.

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

∀ᵐ 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.
Instances For

∃ᵐ 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.
Instances For

Pretty printer defined by notation3 command.

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

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.
Instances For

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.
Instances For
theorem MeasureTheory.mem_ae_iff {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] {μ : F} {s : Set α} :
μ s = 0
theorem MeasureTheory.ae_iff {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] {μ : 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] {μ : F} {s : Set α} :
μ s = 0
theorem MeasureTheory.frequently_ae_iff {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] {μ : 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] {μ : 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] {μ : F} {s : Set α} :
μ s = 0 ∀ᵐ (a : α) ∂μ, as
theorem MeasureTheory.ae_of_all {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] {p : αProp} (μ : F) :
(∀ (a : α), p a)∀ᵐ (a : α) ∂μ, p a
instance MeasureTheory.instCountableInterFilter {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] {μ : F} :
Equations
• =
theorem MeasureTheory.ae_all_iff {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] {μ : F} {ι : Sort u_4} [] {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] {μ : 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] {μ : F} [] {p : αProp} :
(∀ᵐ (x : α) ∂μ, p x) ∀ (x : α), μ {x} 0p x
theorem MeasureTheory.ae_ball_iff {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] {μ : F} {ι : Type u_4} {S : Set ι} (hS : S.Countable) {p : α(i : ι) → i SProp} :
(∀ᵐ (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] {μ : F} (f : αβ) :
f =ᵐ[μ] f
theorem MeasureTheory.ae_eq_symm {α : Type u_1} {β : Type u_2} {F : Type u_3} [FunLike F (Set α) ENNReal] {μ : 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] {μ : F} {f : αβ} {g : αβ} {h : αβ} (h₁ : f =ᵐ[μ] g) (h₂ : g =ᵐ[μ] h) :
f =ᵐ[μ] h
theorem MeasureTheory.ae_le_of_ae_lt {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] {μ : F} {β : Type u_4} [] {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] {μ : F} {s : Set α} :
s =ᵐ[μ] μ s = 0
@[simp]
theorem MeasureTheory.ae_eq_univ {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] {μ : F} {s : Set α} :
s =ᵐ[μ] Set.univ μ s = 0
theorem MeasureTheory.ae_le_set {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] {μ : 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] {μ : 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] {μ : 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] {μ : 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] {μ : 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] {μ : 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] {μ : 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] {μ : 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] {μ : 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] {μ : 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] {μ : 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] {μ : 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] {μ : 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] {μ : 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] {μ : 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] {μ : 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] {μ : 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] {μ : 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] {μ : 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] {μ : F} {s : Set α} {t : Set α} (h : t =ᵐ[μ] ) :
s t =ᵐ[μ]
theorem Set.indicator_ae_eq_zero {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] {μ : F} {M : Type u_4} [Zero M] {f : αM} {s : Set α} :
s.indicator f =ᵐ[μ] 0 μ () = 0
theorem Set.mulIndicator_ae_eq_one {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] {μ : F} {M : Type u_4} [One M] {f : αM} {s : Set α} :
s.mulIndicator f =ᵐ[μ] 1 μ () = 0
theorem MeasureTheory.measure_mono_ae {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] {μ : 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] {μ : 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] {μ : 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] {μ : 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] {μ : F} {s : Set α} {t : Set α} (H : s ≤ᵐ[μ] t) (ht : μ t = 0) :
μ s = 0