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
- MeasureTheory.AEDisjoint μ s t = (↑↑μ (s ∩ t) = 0)
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))
:
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)
:
theorem
MeasureTheory.AEDisjoint.symm
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(h : MeasureTheory.AEDisjoint μ s t)
:
MeasureTheory.AEDisjoint μ t s
theorem
MeasureTheory.AEDisjoint.symmetric
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
:
theorem
MeasureTheory.AEDisjoint.comm
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
:
MeasureTheory.AEDisjoint μ s t ↔ MeasureTheory.AEDisjoint μ t s
theorem
Disjoint.aedisjoint
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(h : Disjoint s t)
:
MeasureTheory.AEDisjoint μ 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 : Set.PairwiseDisjoint s f)
:
Set.Pairwise s (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 ≤ᶠ[MeasureTheory.Measure.ae μ] s)
(hv : v ≤ᶠ[MeasureTheory.Measure.ae μ] t)
:
MeasureTheory.AEDisjoint μ u v
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)
:
MeasureTheory.AEDisjoint μ u v
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 =ᶠ[MeasureTheory.Measure.ae μ] s)
(hv : v =ᶠ[MeasureTheory.Measure.ae μ] t)
:
MeasureTheory.AEDisjoint μ u v
@[simp]
theorem
MeasureTheory.AEDisjoint.iUnion_left_iff
{ι : Type u_1}
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{t : Set α}
[Countable ι]
{s : ι → Set α}
:
MeasureTheory.AEDisjoint μ (⋃ (i : ι), s i) t ↔ ∀ (i : ι), MeasureTheory.AEDisjoint μ (s i) t
@[simp]
theorem
MeasureTheory.AEDisjoint.iUnion_right_iff
{ι : Type u_1}
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
[Countable ι]
{t : ι → Set α}
:
MeasureTheory.AEDisjoint μ s (⋃ (i : ι), t i) ↔ ∀ (i : ι), MeasureTheory.AEDisjoint μ s (t i)
@[simp]
theorem
MeasureTheory.AEDisjoint.union_left_iff
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
{u : Set α}
:
MeasureTheory.AEDisjoint μ (s ∪ t) u ↔ MeasureTheory.AEDisjoint μ s u ∧ MeasureTheory.AEDisjoint μ t u
@[simp]
theorem
MeasureTheory.AEDisjoint.union_right_iff
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
{u : Set α}
:
MeasureTheory.AEDisjoint μ s (t ∪ u) ↔ MeasureTheory.AEDisjoint μ s t ∧ MeasureTheory.AEDisjoint μ s u
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)
:
MeasureTheory.AEDisjoint μ (s ∪ 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)
:
MeasureTheory.AEDisjoint μ s (t ∪ 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 =ᶠ[MeasureTheory.Measure.ae μ] 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 =ᶠ[MeasureTheory.Measure.ae μ] t
theorem
MeasureTheory.AEDisjoint.measure_diff_left
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(h : MeasureTheory.AEDisjoint μ s t)
:
theorem
MeasureTheory.AEDisjoint.measure_diff_right
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(h : MeasureTheory.AEDisjoint μ s t)
:
theorem
MeasureTheory.AEDisjoint.exists_disjoint_diff
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(h : MeasureTheory.AEDisjoint μ s 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)
:
MeasureTheory.AEDisjoint μ s t
theorem
MeasureTheory.AEDisjoint.of_null_left
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(h : ↑↑μ s = 0)
:
MeasureTheory.AEDisjoint μ s t
theorem
MeasureTheory.aedisjoint_compl_left
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
:
theorem
MeasureTheory.aedisjoint_compl_right
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
: