Documentation

Mathlib.MeasureTheory.Measure.AEDisjoint

Almost everywhere disjoint sets #

We say that sets s and t are μ-a.e. disjoint (see MeasureTheory.AEDisjoint) if their intersection has measure zero. This assumption can be used instead of Disjoint in most theorems in measure theory.

def MeasureTheory.AEDisjoint {α : Type u_2} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α) (t : Set α) :

Two sets are said to be μ-a.e. disjoint if their intersection has measure zero.

Equations
Instances For
    theorem MeasureTheory.exists_null_pairwise_disjoint_diff {ι : Type u_1} {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ιSet α} (hd : Pairwise (MeasureTheory.AEDisjoint μ on s)) :
    ∃ (t : ιSet α), (∀ (i : ι), MeasurableSet (t i)) (∀ (i : ι), μ (t i) = 0) Pairwise (Disjoint on fun (i : ι) => s i \ t i)

    If s : ι → Set α is a countable family of pairwise a.e. disjoint sets, then there exists a family of measurable null sets t i such that s i \ t i are pairwise disjoint.

    theorem MeasureTheory.AEDisjoint.eq {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : MeasureTheory.AEDisjoint μ s t) :
    μ (s t) = 0
    theorem Disjoint.aedisjoint {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : Disjoint s t) :
    theorem Pairwise.aedisjoint {ι : Type u_1} {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ιSet α} (hf : Pairwise (Disjoint on f)) :
    theorem Set.PairwiseDisjoint.aedisjoint {ι : Type u_1} {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ιSet α} {s : Set ι} (hf : s.PairwiseDisjoint f) :
    s.Pairwise (MeasureTheory.AEDisjoint μ on f)
    theorem MeasureTheory.AEDisjoint.mono_ae {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} {u : Set α} {v : Set α} (h : MeasureTheory.AEDisjoint μ s t) (hu : u ≤ᵐ[μ] s) (hv : v ≤ᵐ[μ] t) :
    theorem MeasureTheory.AEDisjoint.mono {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} {u : Set α} {v : Set α} (h : MeasureTheory.AEDisjoint μ s t) (hu : u s) (hv : v t) :
    theorem MeasureTheory.AEDisjoint.congr {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} {u : Set α} {v : Set α} (h : MeasureTheory.AEDisjoint μ s t) (hu : u =ᵐ[μ] s) (hv : v =ᵐ[μ] t) :
    @[simp]
    theorem MeasureTheory.AEDisjoint.iUnion_left_iff {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} {ι : Sort u_3} [Countable ι] {s : ιSet α} :
    MeasureTheory.AEDisjoint μ (⋃ (i : ι), s i) t ∀ (i : ι), MeasureTheory.AEDisjoint μ (s i) t
    @[simp]
    theorem MeasureTheory.AEDisjoint.iUnion_right_iff {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {ι : Sort u_3} [Countable ι] {t : ιSet α} :
    MeasureTheory.AEDisjoint μ s (⋃ (i : ι), t i) ∀ (i : ι), MeasureTheory.AEDisjoint μ s (t i)
    theorem MeasureTheory.AEDisjoint.union_left {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} {u : Set α} (hs : MeasureTheory.AEDisjoint μ s u) (ht : MeasureTheory.AEDisjoint μ t u) :
    theorem MeasureTheory.AEDisjoint.union_right {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} {u : Set α} (ht : MeasureTheory.AEDisjoint μ s t) (hu : MeasureTheory.AEDisjoint μ s u) :
    theorem MeasureTheory.AEDisjoint.diff_ae_eq_left {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : MeasureTheory.AEDisjoint μ s t) :
    s \ t =ᵐ[μ] s
    theorem MeasureTheory.AEDisjoint.diff_ae_eq_right {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : MeasureTheory.AEDisjoint μ s t) :
    t \ s =ᵐ[μ] t
    theorem MeasureTheory.AEDisjoint.measure_diff_left {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : MeasureTheory.AEDisjoint μ s t) :
    μ (s \ t) = μ s
    theorem MeasureTheory.AEDisjoint.measure_diff_right {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : MeasureTheory.AEDisjoint μ s t) :
    μ (t \ s) = μ t
    theorem MeasureTheory.AEDisjoint.exists_disjoint_diff {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : MeasureTheory.AEDisjoint μ s t) :
    ∃ (u : Set α), MeasurableSet u μ u = 0 Disjoint (s \ u) t

    If s and t are μ-a.e. disjoint, then s \ u and t are disjoint for some measurable null set u.

    theorem MeasureTheory.AEDisjoint.of_null_right {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : μ t = 0) :
    theorem MeasureTheory.AEDisjoint.of_null_left {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : μ s = 0) :