mathlib3 documentation

measure_theory.measure.ae_disjoint

Almost everywhere disjoint sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

def measure_theory.ae_disjoint {α : Type u_2} {m : measurable_space α} (μ : measure_theory.measure α) (s t : set α) :
Prop

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

Equations
theorem measure_theory.exists_null_pairwise_disjoint_diff {ι : Type u_1} {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [countable ι] {s : ι set α} (hd : pairwise (measure_theory.ae_disjoint μ on s)) :
(t : ι set α), ( (i : ι), measurable_set (t i)) ( (i : ι), μ (t i) = 0) pairwise (disjoint on λ (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.

@[protected]
theorem measure_theory.ae_disjoint.eq {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {s t : set α} (h : measure_theory.ae_disjoint μ s t) :
μ (s t) = 0
@[protected, symm]
@[protected]
theorem disjoint.ae_disjoint {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {s t : set α} (h : disjoint s t) :
@[protected]
theorem pairwise.ae_disjoint {ι : Type u_1} {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : ι set α} (hf : pairwise (disjoint on f)) :
@[protected]
theorem set.pairwise_disjoint.ae_disjoint {ι : Type u_1} {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : ι set α} {s : set ι} (hf : s.pairwise_disjoint f) :
theorem measure_theory.ae_disjoint.mono_ae {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {s t u v : set α} (h : measure_theory.ae_disjoint μ s t) (hu : u ≤ᵐ[μ] s) (hv : v ≤ᵐ[μ] t) :
@[protected]
theorem measure_theory.ae_disjoint.mono {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {s t u v : set α} (h : measure_theory.ae_disjoint μ s t) (hu : u s) (hv : v t) :
@[protected]
theorem measure_theory.ae_disjoint.congr {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {s t u v : set α} (h : measure_theory.ae_disjoint μ s t) (hu : u =ᵐ[μ] s) (hv : v =ᵐ[μ] t) :
@[simp]
theorem measure_theory.ae_disjoint.Union_left_iff {ι : Type u_1} {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {t : set α} [countable ι] {s : ι set α} :
measure_theory.ae_disjoint μ ( (i : ι), s i) t (i : ι), measure_theory.ae_disjoint μ (s i) t
@[simp]
theorem measure_theory.ae_disjoint.Union_right_iff {ι : Type u_1} {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {s : set α} [countable ι] {t : ι set α} :
measure_theory.ae_disjoint μ s ( (i : ι), t i) (i : ι), measure_theory.ae_disjoint μ s (t i)
theorem measure_theory.ae_disjoint.measure_diff_left {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {s t : set α} (h : measure_theory.ae_disjoint μ s t) :
μ (s \ t) = μ s
theorem measure_theory.ae_disjoint.measure_diff_right {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {s t : set α} (h : measure_theory.ae_disjoint μ s t) :
μ (t \ s) = μ t
theorem measure_theory.ae_disjoint.exists_disjoint_diff {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {s t : set α} (h : measure_theory.ae_disjoint μ s t) :
(u : set α), measurable_set 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 measure_theory.ae_disjoint.of_null_right {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {s t : set α} (h : μ t = 0) :
theorem measure_theory.ae_disjoint.of_null_left {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {s t : set α} (h : μ s = 0) :