Documentation

Mathlib.MeasureTheory.OuterMeasure.AE

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 #

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

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

Equations
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

      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 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] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} :
                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 α} :
                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 : α) ∂μ, as
                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
                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} 0p 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 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] [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.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 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 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