MeasureTheory.exists_null_pairwise_disjoint_diff
theorem MeasureTheory.exists_null_pairwise_disjoint_diff :
∀ {ι : Type u_1} {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Countable ι]
{s : ι → Set α},
Pairwise (MeasureTheory.AEDisjoint μ on s) →
∃ t,
(∀ (i : ι), MeasurableSet (t i)) ∧ (∀ (i : ι), ↑↑μ (t i) = 0) ∧ Pairwise (Disjoint on fun i => s i \ t i)
The theorem `MeasureTheory.exists_null_pairwise_disjoint_diff` states that for any countable family of sets `s : ι → Set α`, which are pairwise almost everywhere disjoint with respect to a measure `μ`, there exists a family of measurable null sets `t i` such that the difference sets `s i \ t i` are pairwise disjoint. Here, a set is almost everywhere disjoint with another if their intersection has measure zero, and a set is called a null set if it has measure zero. Pairwise disjointness means that any two distinct sets in the family do not intersect.
More concisely: Given a countable family of pairwise almost everywhere disjoint sets with respect to a measure, there exists a family of measurable null sets such that the differences are pairwise disjoint.
|
Disjoint.aedisjoint
theorem Disjoint.aedisjoint :
∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
Disjoint s t → MeasureTheory.AEDisjoint μ s t
This theorem states that for any type `α`, given a measurable space over `α`, a measure `μ` on that space, and two sets `s` and `t` of type `α`, if `s` and `t` are disjoint in the sense that their infimum is the bottom element, then `s` and `t` are almost everywhere disjoint with respect to the measure `μ`. In other words, the intersection of `s` and `t` has a measure of zero under `μ`. This theorem connects the concept of disjointness in a lattice setting with the concept of almost everywhere disjointness in a measure theory setting.
More concisely: If `α` is a type with a measurable structure, `μ` is a measure on `α`, and `s` and `t` are disjoint subsets of `α` (i.e., `s ∧ t = ⊥`), then `μ(s ∩ t) = 0`.
|
MeasureTheory.AEDisjoint.symm
theorem MeasureTheory.AEDisjoint.symm :
∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
MeasureTheory.AEDisjoint μ s t → MeasureTheory.AEDisjoint μ t s
This theorem states that the property of two sets being "almost everywhere disjoint" with respect to a given measure is symmetric. In other words, for any type `α` equipped with a measurable space structure `m` and a measure `μ`, if two sets `s` and `t` of type `α` are almost everywhere disjoint under the measure `μ` (i.e., the measure of their intersection is zero), then swapping the roles of `s` and `t` doesn't change this fact: `t` and `s` are also almost everywhere disjoint under the measure `μ`.
More concisely: If sets `s` and `t` of type `α` are almost everywhere disjoint under measure `μ` (i.e., `μ(s ∩ t) = 0`), then `s` and `t` are also almost everywhere disjoint under `μ` in the opposite direction (i.e., `μ(s ∩ t) = 0`).
|
Set.PairwiseDisjoint.aedisjoint
theorem Set.PairwiseDisjoint.aedisjoint :
∀ {ι : Type u_1} {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ι → Set α} {s : Set ι},
s.PairwiseDisjoint f → s.Pairwise (MeasureTheory.AEDisjoint μ on f)
This theorem states that for any type `ι`, any measurable space `α`, any measure `μ` on `α`, any function `f` from `ι` to sets of `α`, and any set `s` of `ι`, if the set `s` is pairwise disjoint with respect to function `f` (meaning the images of any two distinct elements of `s` under `f` are disjoint), then the relation `MeasureTheory.AEDisjoint μ` holds pairwise on the set `s` on the function `f` (meaning for all distinct `x` and `y` in `s`, the sets `f(x)` and `f(y)` are almost everywhere disjoint with respect to measure `μ`, i.e., the intersection of `f(x)` and `f(y)` has measure zero).
More concisely: If `s` is a pairwise disjoint set of indices for a measurable function `f` on measurable space `(α, μ)`, then for all distinct `x, y ∈ s`, the sets `f(x)` and `f(y)` are almost everywhere disjoint with respect to `μ`.
|
MeasureTheory.aedisjoint_compl_right
theorem MeasureTheory.aedisjoint_compl_right :
∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
MeasureTheory.AEDisjoint μ s sᶜ
This theorem states that for any given type `α`, any measurable space `m` defined over this type, any measure `μ` defined on this measurable space, and any set `s` of type `α`, the set `s` and its complement `sᶜ` are almost everywhere (a.e.) disjoint with respect to the measure `μ`. In other words, the intersection of set `s` and its complement `sᶜ` has measure zero under the measure `μ`. This is a common property in measure theory as a set and its complement should not have any common elements almost everywhere.
More concisely: For any measurable space `(α, m)`, measure `μ`, and sets `s` and `sᶜ` of type `α` with `μ(s ∩ sᶜ) = 0`, the sets `s` and `sᶜ` are almost everywhere disjoint.
|
Pairwise.aedisjoint
theorem Pairwise.aedisjoint :
∀ {ι : Type u_1} {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ι → Set α},
Pairwise (Disjoint on f) → Pairwise (MeasureTheory.AEDisjoint μ on f)
The theorem `Pairwise.aedisjoint` says that for any type `ι`, any measurable space `α`, any measure `μ` on `α`, and any function `f` from `ι` to the sets of `α`, if every two distinct sets in the image of `f` are disjoint (in the sense that their infimum is the bottom element), then every two distinct sets in the image of `f` are also almost everywhere disjoint with respect to measure `μ` (that is, their intersection has measure zero).
More concisely: For any measurable space `(α, Σ, μ)`, measurable function `f : ι → Σ`, and pairwise disjoint image sets `{f i, i ∈ ι}`, we have `∀ i ≠ j, μ(f i ∩ f j) = 0`.
|
MeasureTheory.AEDisjoint.exists_disjoint_diff
theorem MeasureTheory.AEDisjoint.exists_disjoint_diff :
∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
MeasureTheory.AEDisjoint μ s t → ∃ u, MeasurableSet u ∧ ↑↑μ u = 0 ∧ Disjoint (s \ u) t
The theorem `MeasureTheory.AEDisjoint.exists_disjoint_diff` states that for any type `α` with a measurable space `m` and a measure `μ`, and for any sets `s` and `t` of type `α`, if `s` and `t` are almost everywhere disjoint with respect to measure `μ` (i.e., the measure of the intersection of `s` and `t` is zero), then there exists a measurable set `u` such that the measure of `u` is zero and the set difference `s \ u` is disjoint from `t`. Here, a set is said to be measurable if it can be measured by the ambient measure space, and two elements (or sets) are disjoint if their infimum (greatest lower bound) is the bottom element.
More concisely: Given a measurable space `(α, m)` and measure `μ`, if sets `s` and `t` are almost everywhere disjoint with respect to `μ`, then there exists a measurable set `u` of measure zero such that `s \ u` is disjoint from `t`.
|