MeasureTheory.NullMeasurableSet.of_null
theorem MeasureTheory.NullMeasurableSet.of_null :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
↑↑μ s = 0 → MeasureTheory.NullMeasurableSet s μ
This theorem states that for all types `α` with a measurable space `m0` and a measure `μ`, and for any set `s` of type `α`, if the measure of the set `s` equals zero, then the set `s` is a Null Measurable Set. In mathematical terms, for a measure space (α, m0, μ) and a set s of α, if the measure of s is 0 (i.e., μ(s) = 0), then s is a null measurable set.
More concisely: If the measure of a set in a measurable space is zero, then the set is a null measurable set.
|
MeasureTheory.NullMeasurableSet.iUnion
theorem MeasureTheory.NullMeasurableSet.iUnion :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Sort u_5} [inst : Countable ι]
{s : ι → Set α},
(∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) → MeasureTheory.NullMeasurableSet (⋃ i, s i) μ
This theorem states that for any type `α`, any `MeasurableSpace` on `α`, any measure `μ` on `α`, and any countable index type `ι`, if each set `s i` indexed by `ι` is a `NullMeasurableSet` with respect to measure `μ`, then the union of all such sets (i.e., `(⋃ i, s i)`) is also a `NullMeasurableSet` with respect to the same measure `μ`. In other words, the countable union of null measurable sets is also a null measurable set.
More concisely: If each set in a countable collection is null measurable, then their countable union is also null measurable.
|
MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq
theorem MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
MeasureTheory.NullMeasurableSet s μ → μ.ae.EventuallyEq (MeasureTheory.toMeasurable μ s) s
This theorem states that for any type `α`, any measurable space `m0` on `α`, any measure `μ` on `α`, and any set `s` of `α`, if `s` is a Null Measurable Set with respect to the measure `μ`, then the set `s` is almost everywhere equal to the measurable version of set `s` under the measure `μ`. In other words, the measurable version of a Null Measurable Set is equivalent to the original set almost everywhere with respect to the given measure.
More concisely: A Null Measurable Set `s` with respect to measure `μ` on type `α` equals its measurable version almost everywhere.
|
MeasureTheory.measure_iUnion₀
theorem MeasureTheory.measure_iUnion₀ :
∀ {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Countable ι]
{f : ι → Set α},
Pairwise (MeasureTheory.AEDisjoint μ on f) →
(∀ (i : ι), MeasureTheory.NullMeasurableSet (f i) μ) → ↑↑μ (⋃ i, f i) = ∑' (i : ι), ↑↑μ (f i)
The theorem `MeasureTheory.measure_iUnion₀` is a property about measure theory. Given an index type `ι` that is countable and a measurable space `α` with a measure `μ`, we consider a function `f` that maps each index `i` in `ι` to a set in `α`. If the sets `f i` are almost everywhere disjoint (that is, their intersection has measure zero), and each `f i` is a null measurable set (that is, each `f i` can be approximated by a measurable set up to a set of null measure), then the measure of the union of all `f i` is equal to the sum of the measures of each `f i`. In mathematical notation, this theorem states that if the sets `f(i)` for `i` in `ι` are pairwise `μ`-almost everywhere disjoint and null measurable, then `μ(∪ i, f(i)) = ∑' (i : ι), μ(f(i))`.
More concisely: Given a countable index type `ι`, measurable space `α` with measure `μ`, and a family `f(i)` of pairwise almost everywhere disjoint, null measurable sets, the measure of their union is equal to the sum of their individual measures.
|
MeasureTheory.nullMeasurableSet_univ
theorem MeasureTheory.nullMeasurableSet_univ :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α},
MeasureTheory.NullMeasurableSet Set.univ μ
This theorem states that for any type `α`, any measurable space `m0` on `α`, and any measure `μ` on that measurable space, the universal set (the set of all elements in `α`) is a null-measurable set. In other words, the universal set can be approximated by a measurable set up to a set of null measure. This is a universal property of the universal set in the context of measure theory.
More concisely: In measure theory, the universal set of any measurable space is null-measurable.
|
Measurable.nullMeasurable
theorem Measurable.nullMeasurable :
∀ {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β}
{μ : MeasureTheory.Measure α}, Measurable f → MeasureTheory.NullMeasurable f μ
This theorem states that for any two types `α` and `β`, each equipped with a measurable space structure, and for any function `f` from `α` to `β` and a measure `μ` on `α`, if `f` is a measurable function, then it is also a null measurable function with respect to the measure `μ`. In other words, the preimage of any measurable set under `f` is a null measurable set with respect to `μ`.
More concisely: For any measurable functions `f: α → β` between measurable spaces `(α, Σα)` and `(β, Σβ)` with measure `μ` on `Σα`, the preimage of any measurable set `E ∈ Σβ` is a null set with respect to `μ`: `∀E ∈ Σβ, f⁻¹(E) ∈ Σα, μ(f⁻¹(E)) = 0`.
|
MeasurableSet.nullMeasurableSet
theorem MeasurableSet.nullMeasurableSet :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
MeasurableSet s → MeasureTheory.NullMeasurableSet s μ
This theorem states that for any type `α`, any measurable space `m0` over `α`, any measure `μ` from the `MeasureTheory.Measure` class over `α`, and any set `s` of type `α`, if `s` is a measurable set (i.e., `MeasurableSet s` is true), then `s` is also a null measurable set with respect to measure `μ` (i.e., `MeasureTheory.NullMeasurableSet s μ` is true). In other words, any measurable set can be approximated by a measurable set up to a set of null measure.
More concisely: Any measurable set in a measurable space is a null measurable set with respect to any measure.
|
MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq
theorem MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
MeasureTheory.NullMeasurableSet s μ → ∃ t ⊆ s, MeasurableSet t ∧ μ.ae.EventuallyEq t s
This theorem states that for any type `α` equipped with a measure space `m0` and a measure `μ`, and for any set `s` of `α`, if `s` is a null measurable set with respect to `μ`, there exists a subset `t` of `s` such that `t` is a measurable set and `t` is almost everywhere equal to `s` with respect to the measure `μ`. In other words, every null measurable set can be approximated almost everywhere by a measurable set.
More concisely: Given a measure space `(α, m0, μ)` and a null measurable set `s ⊆ α`, there exists a measurable set `t ∋ s` such that `μ(s \ t) = 0`.
|
MeasureTheory.NullMeasurableSet.congr
theorem MeasureTheory.NullMeasurableSet.congr :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
MeasureTheory.NullMeasurableSet s μ → μ.ae.EventuallyEq s t → MeasureTheory.NullMeasurableSet t μ
This theorem states that for any type `α` equipped with a measurable space and a measure `μ`, and any two sets `s` and `t` of type `α`, if `s` is a null measurable set with respect to `μ`, and `s` equals `t` almost everywhere (i.e., except for a set of null measure), then `t` is also a null measurable set with respect to `μ`. In other words, it says that the property of being a null measurable set is preserved under equality almost everywhere.
More concisely: If two sets have the same elements almost everywhere and are null measurable with respect to a measure, then each is null measurable.
|
MeasureTheory.measure_inter_add_diff₀
theorem MeasureTheory.measure_inter_add_diff₀ :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α),
MeasureTheory.NullMeasurableSet t μ → ↑↑μ (s ∩ t) + ↑↑μ (s \ t) = ↑↑μ s
The theorem `MeasureTheory.measure_inter_add_diff₀` states that for any type `α` equipped with a measurable space `m0` and a measure `μ`, and for any set `t` of this type that is null measurable, for all sets `s` of this type, the measure of the intersection of `s` and `t` plus the measure of the difference of `s` and `t` is equal to the measure of `s`. In mathematical terms, this is stating that a null measurable set `t` satisfies the property of Carathéodory measurability, which is expressed as `μ (s ∩ t) + μ (s \ t) = μ s` for any set `s`.
More concisely: For any null measurable set `t` in a measurable space `(α, m0, μ)`, the measure of the intersection of `t` with any set `s` plus the measure of the difference between `s` and `t` equals the measure of `s`. That is, `μ (s ∩ t) + μ (s \ t) = μ s`.
|
MeasureTheory.NullMeasurableSet.compl
theorem MeasureTheory.NullMeasurableSet.compl :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
MeasureTheory.NullMeasurableSet s μ → MeasureTheory.NullMeasurableSet sᶜ μ
The theorem `MeasureTheory.NullMeasurableSet.compl` states that for any type `α`, measurable space `m0`, measure `μ`, and set `s`, if `s` is a null measurable set with respect to measure `μ`, then the complement of `s` (denoted by `sᶜ`) is also a null measurable set with respect to the same measure `μ`. In other words, the property of being a null measurable set is preserved under taking complements.
More concisely: If a set `s` is null measurable with respect to measure `μ` in measurable space `m0`, then its complement `sᶜ` is also null measurable with respect to `μ` in `m0`.
|
MeasureTheory.exists_subordinate_pairwise_disjoint
theorem MeasureTheory.exists_subordinate_pairwise_disjoint :
∀ {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Countable ι]
{s : ι → Set α},
(∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) →
Pairwise (MeasureTheory.AEDisjoint μ on s) →
∃ t,
(∀ (i : ι), t i ⊆ s i) ∧
(∀ (i : ι), μ.ae.EventuallyEq (s i) (t i)) ∧
(∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)
This theorem states that given a countable family of null measurable sets, which are pairwise almost everywhere disjoint with respect to a certain measure `μ`, there exists a subordinate family of measurable sets, which are pairwise disjoint, such that each member of the subordinate family is a subset of the corresponding set in the original family and is almost everywhere equal to it with respect to the measure `μ`.
In detail, let `sᵢ` be a countable family of sets in a measurable space `α` that are each null measurable with respect to a measure `μ` and pairwise almost everywhere disjoint. This theorem then asserts the existence of another family of sets `tᵢ`, each of which is a subset of the corresponding `sᵢ` and is equal to `sᵢ` almost everywhere with respect to `μ`. Further, each `tᵢ` is a measurable set, and the `tᵢ` are pairwise disjoint.
More concisely: Given a countable family of null measurable, pairwise almost everywhere disjoint sets in a measurable space with respect to a measure, there exists a subordinate family of measurable, pairwise disjoint sets, each of which is almost everywhere equal to its corresponding original set.
|
MeasureTheory.measure_iUnion
theorem MeasureTheory.measure_iUnion :
∀ {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Countable ι]
{f : ι → Set α},
Pairwise (Disjoint on f) → (∀ (i : ι), MeasurableSet (f i)) → ↑↑μ (⋃ i, f i) = ∑' (i : ι), ↑↑μ (f i)
The theorem `MeasureTheory.measure_iUnion` states that for any countable type `ι`, any type `α`, any `MeasurableSpace α` named `m0`, any `MeasureTheory.Measure α` named `μ`, and a function `f` from `ι` to `Set α`, if the sets produced by `f` are pairwise disjoint and each of these sets is measurable, then the measure of the union of these sets (⋃ i, f i) is equal to the sum of the measures of each individual set (∑' (i : ι), ↑↑μ (f i)). In other words, in a countable collection of pairwise disjoint measurable sets, the measure of the union of the sets is the sum of their individual measures.
More concisely: For any countable family of pairwise disjoint measurable sets in a Measurable Space, the measure of their union equals the sum of the measures of each individual set.
|
MeasureTheory.NullMeasurableSet.diff
theorem MeasureTheory.NullMeasurableSet.diff :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
MeasureTheory.NullMeasurableSet s μ →
MeasureTheory.NullMeasurableSet t μ → MeasureTheory.NullMeasurableSet (s \ t) μ
The theorem `MeasureTheory.NullMeasurableSet.diff` states that for any given type `α`, measurable space `m0` over `α`, measure `μ` over the measurable space, and sets `s` and `t` of type `α`, if `s` and `t` are both null measurable sets with respect to measure `μ`, then the difference set (`s \ t`) is also a null measurable set with respect to the same measure `μ`. In other words, the difference of two null measurable sets is also a null measurable set.
More concisely: If `s` and `t` are null measurable sets in a measurable space `(α, m0, μ)`, then `s \ t` is also a null measurable set.
|
MeasureTheory.NullMeasurableSet.inter
theorem MeasureTheory.NullMeasurableSet.inter :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
MeasureTheory.NullMeasurableSet s μ →
MeasureTheory.NullMeasurableSet t μ → MeasureTheory.NullMeasurableSet (s ∩ t) μ
This theorem, `MeasureTheory.NullMeasurableSet.inter`, states that for any type `α` with a measurable space structure `m0` and a measure `μ`, and for any two sets `s` and `t` of type `α`, if both `s` and `t` are "null measurable sets" with respect to the measure `μ`, then their intersection (`s ∩ t`) is also a "null measurable set" with respect to the same measure `μ`. In other words, the intersection of two null measurable sets is itself a null measurable set.
More concisely: If `s` and `t` are null measurable sets in the measurable space `(α, m0)` with respect to measure `μ`, then their intersection `s ∩ t` is also a null measurable set.
|