MeasureTheory.measure_zero_iff_ae_nmem
theorem MeasureTheory.measure_zero_iff_ae_nmem :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α},
↑↑μ s = 0 ↔ ∀ᵐ (a : α) ∂μ, a ∉ s
This theorem states that for any type `α` equipped with a `MeasurableSpace` structure, any measure `μ` on `α`, and any set `s` of elements of `α`, the measure of `s` with respect to `μ` is zero if and only if almost every element of `α` (with respect to the measure `μ`) is not a member of `s`. In other words, a set has zero measure if and only if it does not contain almost all elements.
More concisely: For any measurable space `(α, Σ, μ)`, a set `s ∈ Σ` has measure zero with respect to `μ` if and only if its complement is almost everywhere contained in `s`.
|
AEMeasurable.congr
theorem AEMeasurable.congr :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : MeasurableSpace β] {f g : α → β}
{μ : MeasureTheory.Measure α}, AEMeasurable f μ → μ.ae.EventuallyEq f g → AEMeasurable g μ
This theorem states that for any two functions `f` and `g` from a measurable space `α` to another measurable space `β`, along with a measure `μ` on `α`, if the function `f` is almost everywhere measurable with respect to measure `μ` and `f` is almost everywhere equal to `g` (in the measure-theoretic sense), then `g` is also almost everywhere measurable with respect to the same measure `μ`.
In simpler terms, if two functions are almost everywhere the same, and one of them is known to be almost everywhere measurable, then the other function must also be almost everywhere measurable.
More concisely: If two functions from a measurable space to another, with respect to a given measure, are almost everywhere equal and one is almost everywhere measurable, then the other is also almost everywhere measurable.
|
MeasureTheory.ae_eq_empty
theorem MeasureTheory.ae_eq_empty :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α},
μ.ae.EventuallyEq s ∅ ↔ ↑↑μ s = 0
The theorem `MeasureTheory.ae_eq_empty` states that for any type `α`, which is equipped with a `MeasurableSpace` structure, a measure `μ` of type `MeasureTheory.Measure α`, and a set `s` of elements of type `α`, `s` is almost everywhere equal to the empty set with respect to the filter associated with `μ` if and only if the measure of `s` is zero. The filter associated with `μ` represents the "almost everywhere" concept, which means that a property holds except on a set of measure zero. In simple terms, in a given measurable space, a set is essentially empty (almost everywhere) if its measure is zero.
More concisely: For any measurable space `(α, Σ, μ)`, a set `s ∈ Σ` is almost everywhere equal to the empty set if and only if its measure `μ(s)` is zero.
|
MeasureTheory.subset_toMeasurable
theorem MeasureTheory.subset_toMeasurable :
∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α),
s ⊆ MeasureTheory.toMeasurable μ s
This theorem states that for any type `α` that is equipped with a `MeasurableSpace` structure, any measure `μ` on this measurable space, and any set `s` of elements of type `α`, the set `s` is a subset of the set `MeasureTheory.toMeasurable μ s`. In other words, every element of `s` is also an element of `MeasureTheory.toMeasurable μ s`. This is a crucial property in measure theory, which ensures that we can always find a measurable set that contains a given set.
More concisely: For any measurable space `(α, Σ)`, measure `μ : MeasurableSpace.Measure Σ α`, and set `s ∈ Σ`, we have `s ⊆ MeasurableTheory.toMeasurable μ s`.
|
MeasureTheory.exists_measurable_superset_of_null
theorem MeasureTheory.exists_measurable_superset_of_null :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α},
↑↑μ s = 0 → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑↑μ t = 0
This theorem, `MeasureTheory.exists_measurable_superset_of_null`, states that for any type `α`, measurable space `α`, measure `μ` on `α`, and set `s` of `α`, if the measure of set `s` is zero, then there exists a measurable superset `t` of `s` such that the measure of `t` is also zero. In mathematical terms, for all sets `s` with `μ(s) = 0`, there exists a set `t` such that `s` is a subset of `t`, `t` is a measurable set, and `μ(t) = 0`.
More concisely: For any measurable space `(α, μ)` and measurable set `s` with `μ(s) = 0`, there exists a measurable set `t` containing `s` such that `μ(t) = 0`.
|
MeasureTheory.Measure.ofMeasurable_apply
theorem MeasureTheory.Measure.ofMeasurable_apply :
∀ {α : Type u_1} [inst : MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal} {m0 : m ∅ ⋯ = 0}
{mU :
∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯}
(s : Set α) (hs : MeasurableSet s), ↑↑(MeasureTheory.Measure.ofMeasurable m m0 mU) s = m s hs
The theorem `MeasureTheory.Measure.ofMeasurable_apply` states that for any type `α` equipped with a measure space and a function `m` that maps measurable sets from `α` to the extended nonnegative real numbers (known as a measure), if this measure of the empty set is zero and the measure is countably additive on pairwise disjoint sets, then for any measurable set `s`, the measure of `s` obtained from the function `m` using `MeasureTheory.Measure.ofMeasurable` equals to the measure `m` of `s`. In other words, the measure of a set obtained by the construction `MeasureTheory.Measure.ofMeasurable` is consistent with the original measure function `m`.
More concisely: If `m` is a countably additive measure on a measurable space with `m(`empty set`) = 0`, then for any measurable set `s`, `MeasureTheory.Measure.ofMeasurable s = m s`.
|
MeasureTheory.measure_eq_iInf
theorem MeasureTheory.measure_eq_iInf :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} (s : Set α),
↑↑μ s = ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), ↑↑μ t
The theorem `MeasureTheory.measure_eq_iInf` states that for any given type `α` that forms a measurable space, any measure `μ` on that space, and any set `s` of type `α`, the measure of `s` is equal to the infimum of the measures of all measurable sets `t` such that `s` is a subset of `t`. In other words, we can calculate the measure of a set by looking at all larger measurable sets and finding the smallest measure among them.
More concisely: For any measurable space `(α, Σ, μ)`, the measure of a measurable set `s` is equal to the infimum of the measures of all measurable sets `t` containing `s`.
|
MeasureTheory.diff_ae_eq_self
theorem MeasureTheory.diff_ae_eq_self :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α},
μ.ae.EventuallyEq (s \ t) s ↔ ↑↑μ (s ∩ t) = 0
This theorem is about measure theory in the context of sets and measurable spaces. It states that for any type `α`, with a measurable space instance, a measure `μ`, and two sets `s` and `t` of type `α`, the set difference `s \ t` is almost everywhere equal to set `s` with respect to the measure `μ` if and only if the measure of the intersection of `s` and `t` is zero. In other words, if the intersection of `s` and `t` contributes nothing to the measure of `s`, then `s` minus `t` is the same as `s` almost everywhere with respect to the measure `μ`.
More concisely: For any measurable sets `s` and `t` of type `α` in a measurable space with measure `μ`, `s \ t` is almost everywhere equal to `s` if and only if the measure of `s ∩ t` is zero.
|
MeasureTheory.exists_measurable_superset
theorem MeasureTheory.exists_measurable_superset :
∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α),
∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑↑μ t = ↑↑μ s
The theorem `MeasureTheory.exists_measurable_superset` states that for every set `s` in a measurable space `α`, with a given measure `μ`, there exists a superset `t` of `s` such that `t` is a measurable set and the measure `μ` of `t` is equal to the measure `μ` of `s`. In other words, no matter which set and measure we start with, we can always find a larger or equal measurable set with the same measure.
More concisely: Given a measurable space `(α, Σ, μ)` and a measurable set `s ∈ Σ`, there exists a measurable set `t ∈ Σ` such that `t supseteq s` and `μ(t) = μ(s)`.
|
AEMeasurable.measurable_mk
theorem AEMeasurable.measurable_mk :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
{μ : MeasureTheory.Measure α} (h : AEMeasurable f μ), Measurable (AEMeasurable.mk f h)
The theorem `AEMeasurable.measurable_mk` states that for any types `α` and `β`, given a measurable space structure on `α`, a measurable space on `β`, a function `f` from `α` to `β`, and a measure `μ` on `α`, if `f` is almost everywhere measurable with respect to `μ`, then the function associated to `f`, which coincides with `f` almost everywhere, is measurable. This means that the preimage of any measurable set under this associated function is also a measurable set.
More concisely: If a function between measurable spaces is almost everywhere defined by a measurable function and a measure is given, then the function is measurable.
|
Mathlib.MeasureTheory.Measure.MeasureSpaceDef._auxLemma.18
theorem Mathlib.MeasureTheory.Measure.MeasureSpaceDef._auxLemma.18 :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α},
μ.ae.EventuallyLE s t = (↑↑μ (s \ t) = 0)
This theorem states that for any type `α`, equipped with a `MeasurableSpace` structure, and for any measure `μ` defined on this measurable space, along with any two sets `s` and `t` of type `α`, the property that `s` is less than or equal to `t` almost everywhere with respect to the measure `μ` is equivalent to the measure of the set difference `s \ t` being zero. In standard mathematical notation, this would be expressed as $s \leq_{\mu-a.e.} t$ if and only if $\mu(s \setminus t) = 0$.
More concisely: For any measurable spaces `(α, Σ)` with measure `μ`, sets `s` and `t` in `α` are almost everywhere equal with respect to `μ` if and only if their set difference has measure zero: `s ∩^μ t = ∫ x in α, 1{s(x) = t(x)} dμ = μ(s \ t) = 0`.
|
MeasureTheory.frequently_ae_mem_iff
theorem MeasureTheory.frequently_ae_mem_iff :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α},
(∃ᵐ (a : α) ∂μ, a ∈ s) ↔ ↑↑μ s ≠ 0
The theorem `MeasureTheory.frequently_ae_mem_iff` states that for any given type `α` equipped with a measurable space structure, a measure `μ` on that space, and a set `s` of elements of type `α`, the condition that there almost everywhere exists an element `a` of type `α` (with respect to measure `μ`) which belongs to the set `s` is equivalent to the measure of the set `s` not being zero. In other words, if a set `s` has non-zero measure then almost every point in the measurable space `α` will be a member of `s`, and vice versa.
More concisely: A measurable set in a measure space has non-zero measure if and only if almost every point in the space belongs to the set.
|
MeasureTheory.toMeasurable_def
theorem MeasureTheory.toMeasurable_def :
∀ {α : Type u_6} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α),
MeasureTheory.toMeasurable μ s =
if h : ∃ t ⊇ s, MeasurableSet t ∧ μ.ae.EventuallyEq t s then h.choose
else
if h' : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t ∩ u) = ↑↑μ (s ∩ u) then h'.choose
else ⋯.choose
The theorem `MeasureTheory.toMeasurable_def` states that for any type `α` with a `MeasurableSpace` instance and for any measure `μ` and a set `s` of type `α`, the measurable representative `MeasureTheory.toMeasurable` of the set `s` according to the measure `μ` is defined as follows: If there exists a set `t` that contains `s`, is measurable, and is equal to `s` almost everywhere with respect to the measure `μ`, then the measurable representative is the set extracted from this existential statement. If such a `t` does not exist but there exists a `t` that contains `s` and is measurable, and for all measurable sets `u`, the measure of the intersection of `t` and `u` is equal to the measure of the intersection of `s` and `u`, then the measurable representative is the set extracted from this second existential statement. If neither of these conditions is met, then the measurable representative is obtained from another (unspecified here) existential statement.
More concisely: If a set in a measurable space can be represented as the measurable subset equal almost everywhere or having equal measures with some other measurable set, then that set is the measurable representative according to the given measure. Otherwise, the measurable representative is obtained from some other existential statement.
|
MeasureTheory.measure_empty
theorem MeasureTheory.measure_empty :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}, ↑↑μ ∅ = 0
This theorem states that for any type `α`, given that `α` is a measurable space and `μ` is a measure on that space, the measure of the empty set is zero. In mathematical terms, for all spaces `α` and measures `μ`, it holds that `μ(∅) = 0`.
More concisely: In a measurable space `(α, Σ, μ)`, the measure of the empty set `∅` is zero, i.e., `μ(∅) = 0`.
|
MeasureTheory.measure_iUnion_le
theorem MeasureTheory.measure_iUnion_le :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : Countable β]
(s : β → Set α), ↑↑μ (⋃ i, s i) ≤ ∑' (i : β), ↑↑μ (s i)
The theorem `MeasureTheory.measure_iUnion_le` states that for any types `α` and `β`, given a measurable space on `α` and a countable set of indices `β`, if `s` is a function mapping each index in `β` to a set in `α`, then the measure of the union of all sets `s i` (where `i` ranges over each index in `β`) with respect to a measure `μ` is less than or equal to the sum of the measures of each individual set `s i`. This theorem corresponds to the sub-additivity property of measures, stating that the measure of a union of sets is not greater than the sum of their individual measures.
More concisely: For any measurable space with measure `μ`, and a countable collection of measurable sets `{s i | i ∈ β}`, the measure of their union is less than or equal to the sum of the measures of each individual set. `μ(⋃i∈β si) ≤ ∑i∈β μ(si)`
|
aemeasurable_const
theorem aemeasurable_const :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
{b : β}, AEMeasurable (fun _a => b) μ
The theorem `aemeasurable_const` states that for any type `α`, measurable space `m` over `α`, type `β`, measurable space over `β`, measure `μ` over `α`, and element `b` of type `β`, the function which assigns `b` to every element of `α` is almost everywhere measurable with respect to `μ`. In other words, a constant function is almost everywhere measurable.
More concisely: For any measurable spaces (α, m) and (β, ν) over types α and β, and any measure μ over (α, m) and constant function f : α → β, the function f is almost everywhere measurable with respect to μ.
|
MeasureTheory.measure_biUnion_finset_le
theorem MeasureTheory.measure_biUnion_finset_le :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} (s : Finset β)
(f : β → Set α), ↑↑μ (⋃ b ∈ s, f b) ≤ s.sum fun p => ↑↑μ (f p)
This theorem states that for any given measurable space `α`, any type `β`, and any measure `μ` defined on `α`, if `s` is a finite set of elements from `β` and `f` is a function from `β` to a set of elements in `α`, then the measure of the union of sets `f b` for every `b` in `s` is less than or equal to the sum of the measures of each `f p` for every `p` in `s`. In mathematical notation, this theorem is asserting that for a measure `μ`, a finite set `s`, and a function `f`, we have
\[
μ\left(\bigcup_{b\in s} f(b)\right) \leq \sum_{p\in s} μ(f(p))
\]
This theorem is a statement about the subadditivity of measures in measure theory.
More concisely: For any measure μ, finite set s, and function f from a measurable space to itself, the measure of the union of images of elements in s under f is less than or equal to the sum of the measures of the images of those elements. That is, μ(⋃b∈s f(b)) ≤ ∑p∈s μ(f(p)).
|
AEMeasurable.ae_eq_mk
theorem AEMeasurable.ae_eq_mk :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
{μ : MeasureTheory.Measure α} (h : AEMeasurable f μ), μ.ae.EventuallyEq f (AEMeasurable.mk f h)
The theorem `AEMeasurable.ae_eq_mk` states that for any types `α` and `β`, given a measurable space `α`, and `β` with a measurable space instance, and any function `f` from `α` to `β`, and a measure `μ` on `α`, if `f` is an almost everywhere measurable function, then `f` is equal almost everywhere (according to the measure `μ`) to a corresponding measurable function obtained from `AEMeasurable.mk f h`, where `h` is the proof that `f` is almost everywhere measurable. In other words, a function that is almost everywhere measurable is equivalent to a measurable function on almost all of the domain.
More concisely: If `f` is an almost everywhere measurable function from the measurable space `(α, Σ, μ)` to `(β, Σ', ν)`, then there exists a measurable function `g : α → β` such that `μ({x : α | f x ≠ g x}) = 0`.
|
MeasureTheory.ae_of_all
theorem MeasureTheory.ae_of_all :
∀ {α : Type u_1} [inst : MeasurableSpace α] {p : α → Prop} (μ : MeasureTheory.Measure α),
(∀ (a : α), p a) → ∀ᵐ (a : α) ∂μ, p a
This theorem, `MeasureTheory.ae_of_all`, states that for any measurable space `α` and any property `p` on `α`, if every element in `α` satisfies the property `p`, then `p` holds almost everywhere with respect to the measure `μ`. In other words, any property that is true for every point in a given measurable space is also true almost everywhere under any measure applied to that space. "Almost everywhere" means that the set of points where the property is not true is of measure zero.
More concisely: If every point in a measurable space carries a measurable property and the set of points where the property doesn't hold has measure zero, then the property holds almost everywhere.
|
Filter.EventuallyLE.measure_le
theorem Filter.EventuallyLE.measure_le :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α},
μ.ae.EventuallyLE s t → ↑↑μ s ≤ ↑↑μ t
This theorem, known as an **alias of `MeasureTheory.measure_mono_ae`**, states that for any type `α` that is a `MeasurableSpace`, a measure `μ` on `α`, and sets `s` and `t` of `α`, if `s` is a subset of `t` modulo a set of measure `0` (represented as `μ.ae.EventuallyLE s t`), then the measure of set `s` is less than or equal to the measure of set `t`. In other words, if `s` is almost everywhere contained in `t`, we can guarantee that the measure of `s` will not exceed the measure of `t`.
More concisely: If `s` is a subset of `t` up to a set of measure 0 in a measurable space `(α, μ)`, then `μ(s) ≤ μ(t)`.
|
MeasureTheory.measure_congr
theorem MeasureTheory.measure_congr :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α},
μ.ae.EventuallyEq s t → ↑↑μ s = ↑↑μ t
This theorem states that, given a measurable space and a measure on that space, if two sets are essentially equal (they only differ by a set of measure zero), then the measure of these two sets is also the same. In other words, for any measurable space `α`, measure `μ` on `α`, and sets `s` and `t` in `α`, if `s` and `t` are equal almost everywhere (ignoring a set of measure zero), then the measure of `s` is equal to the measure of `t`.
More concisely: If two measurable sets have the same measure almost everywhere in a measurable space with respect to a given measure, then they have equal measures.
|
MeasureTheory.measurableSet_toMeasurable
theorem MeasureTheory.measurableSet_toMeasurable :
∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α),
MeasurableSet (MeasureTheory.toMeasurable μ s)
The theorem `MeasureTheory.measurableSet_toMeasurable` states that for any type `α` equipped with a `MeasurableSpace` structure, any measure `μ` on this space, and any set `s` of elements of type `α`, the set `MeasureTheory.toMeasurable μ s` is a measurable set. In other words, this theorem ensures that the operation `toMeasurable`, when applied to a measure and a set, always results in a measurable set, as defined in the associated measurable space.
More concisely: For any measurable space `(α, Σ, μ)`, the image `toMeasurable μ s` of any set `s ∈ Σ` is measurable.
|
MeasureTheory.ae_eq_trans
theorem MeasureTheory.ae_eq_trans :
∀ {α : Type u_1} {δ : Type u_4} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g h : α → δ},
μ.ae.EventuallyEq f g → μ.ae.EventuallyEq g h → μ.ae.EventuallyEq f h
The theorem `MeasureTheory.ae_eq_trans` states that for any measure space `α`, any type `δ`, and any measure `μ` on `α`, if two functions `f` and `g` from `α` to `δ` are equal almost everywhere with respect to `μ`, and `g` and another function `h` are also equal almost everywhere with respect to `μ`, then `f` and `h` are equal almost everywhere with respect to `μ`. This is the transitive property for the equivalence relation of being equal almost everywhere.
More concisely: If functions `f` and `g`, and `g` and `h` are equal almost everywhere with respect to measure `μ` on measure space `α`, then `f` and `h` are equal almost everywhere with respect to `μ`.
|
MeasureTheory.ae_all_iff
theorem MeasureTheory.ae_all_iff :
∀ {α : Type u_1} {ι : Sort u_5} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : Countable ι]
{p : α → ι → Prop}, (∀ᵐ (a : α) ∂μ, ∀ (i : ι), p a i) ↔ ∀ (i : ι), ∀ᵐ (a : α) ∂μ, p a i
This theorem states that, given a measurable space `α`, a countably infinite set `ι`, a measure `μ` on `α`, and a property `p` that relates elements of `α` and `ι`, the property `p` holds almost everywhere (i.e., everywhere except on a set of measure zero) for all elements of `α` and `ι` if and only if for each element of `ι`, `p` holds almost everywhere for all elements of `α`. In mathematical terms, this is written as `∀ᵐ (a : α) ∂μ, ∀ (i : ι), p a i` is equivalent to `∀ (i : ι), ∀ᵐ (a : α) ∂μ, p a i`.
More concisely: Given a measurable space `(α, Σ, μ)`, a countably infinite index set `ι`, and a property `p(a, i)` relating elements `a ∈ α` and `i ∈ ι`, the property `p` holds almost everywhere for all `a ∈ α` if and only if it holds almost everywhere for all `i ∈ ι`, i.e., `∀ᵐ a ∂μ ∀ i ∈ ι, p(a, i)` is equivalent to `∀ i ∈ ι, ∀ᵐ a ∂μ, p(a, i)`.
|
MeasureTheory.measure_eq_iInf'
theorem MeasureTheory.measure_eq_iInf' :
∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α), ↑↑μ s = ⨅ t, ↑↑μ ↑t := by
sorry
This theorem, named `MeasureTheory.measure_eq_iInf'`, states that for any type `α` that has a `MeasurableSpace` instance, any measure `μ` from `MeasureTheory.Measure α`, and any set `s` belonging to type `α`, the measure of set `s` is equal to the infimum (greatest lower bound) of the measure of set `t`. This theorem is useful when we apply another lemma that works only for non-empty infima. In such cases, we can use `nonempty_measurable_superset`. The symbol `⨅` denotes infimum in Lean 4.
More concisely: For any measurable space `(α, Σ, μ)`, and any set `s ∈ Σ`, the measure of `s` is equal to the infimum of the measures of sets in `Σ` that contain `s`.
|
MeasureTheory.measure_mono_ae
theorem MeasureTheory.measure_mono_ae :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α},
μ.ae.EventuallyLE s t → ↑↑μ s ≤ ↑↑μ t
The theorem `MeasureTheory.measure_mono_ae` states that for any measurable space `α` and any measure `μ` on this space, if a set `s` is contained within another set `t` almost everywhere (i.e., outside of a set of measure `0`), then the measure of set `s` is less than or equal to the measure of set `t`. In other words, if a set is almost entirely contained in another, then its measure will not exceed the measure of the containing set.
More concisely: If `s` is a measurable subset of measurable space `(α, Σ, μ)` and `μ(t \ s) = 0` for some `t ∈ Σ`, then `μ(s) ≤ μ(t)`.
|
MeasurableSpace.ae_induction_on_inter
theorem MeasurableSpace.ae_induction_on_inter :
∀ {α : Type u_1} {β : Type u_6} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure β} {C : β → Set α → Prop}
{s : Set (Set α)} [m : MeasurableSpace α],
m = MeasurableSpace.generateFrom s →
IsPiSystem s →
(∀ᵐ (x : β) ∂μ, C x ∅) →
(∀ᵐ (x : β) ∂μ, ∀ t ∈ s, C x t) →
(∀ᵐ (x : β) ∂μ, ∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ) →
(∀ᵐ (x : β) ∂μ,
∀ (f : ℕ → Set α),
Pairwise (Disjoint on f) →
(∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ i, f i)) →
∀ᵐ (x : β) ∂μ, ∀ ⦃t : Set α⦄, MeasurableSet t → C x t
This theorem states that given two measurable spaces `α` and `β`, a measure `μ` on `β`, a predicate `C` on `β` and `Set α`, and a collection `s` of subsets of `α` that generates the σ-algebra of `α` and forms a π-system. If the predicate `C` holds for almost every `x` in `β` and the empty set in `Set α`, and for almost every `x` in `β` the predicate holds for all subsets in `s`. Moreover, if for almost every `x` in `β`, the predicate `C` is closed under the operations of taking complements and countable disjoint unions of measurable sets, then the predicate `C` holds for almost every `x` in `β` and for all measurable sets of `α`. This theorem is a version of `MeasurableSpace.induction_on_inter` where the condition is dependent on the measurable space `β` and it holds almost everywhere with respect to the measure `μ`.
More concisely: Given measurable spaces `α` and `β`, a measure `μ` on `β`, a predicate `C` on `α × β`, and a σ-algebra generating π-system `s` of `α` such that `C` holds almost everywhere in `β` for the empty set and all sets in `s`, and `C` is measurable and closed under complements and countable disjoint unions almost everywhere in `β`, then `C` holds almost everywhere in `β` for all measurable sets of `α`.
|
MeasureTheory.ae_le_set
theorem MeasureTheory.ae_le_set :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α},
μ.ae.EventuallyLE s t ↔ ↑↑μ (s \ t) = 0
This theorem, in the field of measure theory, states that for any given type `α`, any measurable space `α`, any measure `μ` on that measurable space, and any two sets `s` and `t` of type `α`, `s` is almost everywhere less than or equal to `t` (as per the filter defined by `MeasureTheory.Measure.ae μ`) if and only if the measure of the set difference `s \ t` is 0. In other words, the set `s` is less than or equal to the set `t` almost everywhere when the measure of elements in `s` that are not in `t` is zero.
More concisely: For any measurable spaces `α`, measures `μ` on `α`, and sets `s` and `t` of type `α`, `s ⊆ t` almost everywhere (with respect to `μ`) if and only if `μ(s \ t) = 0`.
|
Measurable.aemeasurable
theorem Measurable.aemeasurable :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
{μ : MeasureTheory.Measure α}, Measurable f → AEMeasurable f μ
The `Measurable.aemeasurable` theorem states that for any two types `α` and `β`, given a measurable space over `α`, a measurable function `f` from `α` to `β`, and a measure `μ` over `α`, if `f` is measurable, then `f` is also almost everywhere measurable with respect to the measure `μ`. In other words, a measurable function coincides almost everywhere with itself, providing a bridge between the concepts of measurability and almost everywhere measurability.
More concisely: A measurable function between measurable spaces is almost everywhere measurable with respect to the given measure.
|
Mathlib.MeasureTheory.Measure.MeasureSpaceDef._auxLemma.17
theorem Mathlib.MeasureTheory.Measure.MeasureSpaceDef._auxLemma.17 :
∀ {α : Type u} {β : Type v} [inst : PartialOrder β] {l : Filter α} {f g : α → β},
l.EventuallyEq f g = (l.EventuallyLE f g ∧ l.EventuallyLE g f)
This theorem states that for any two functions `f` and `g` from a type `α` to a partially ordered type `β`, the equality of `f` and `g` almost everywhere (i.e., with respect to a filter `l` on `α`) is equivalent to `f` being less than or equal to `g` almost everywhere and `g` being less than or equal to `f` almost everywhere. Essentially, this is saying in the context of measure theory, two functions are equal almost everywhere if and only if they are both less than or equal to each other almost everywhere.
More concisely: For functions `f` and `g` from type `α` to a partially ordered type `β`, `f` and `g` are equal almost everywhere with respect to filter `l` if and only if they are both less than or equal to each other almost everywhere with respect to `l`.
|
MeasureTheory.measure_union_le
theorem MeasureTheory.measure_union_le :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} (s₁ s₂ : Set α),
↑↑μ (s₁ ∪ s₂) ≤ ↑↑μ s₁ + ↑↑μ s₂
The theorem `MeasureTheory.measure_union_le` states that for any type `α` equipped with a `MeasurableSpace` structure and for any measure `μ` on `α`, the measure `μ` of the union of two sets `s₁` and `s₂` is always less than or equal to the sum of the measures of `s₁` and `s₂`. In other words, the measure of the union of two sets is at most the sum of their individual measures.
More concisely: For any measurable spaces `(α, Σ, μ)` and sets `s₁, s₂ ∈ Σ`, we have `μ(s₁ ∪ s₂) ≤ μ(s₁) + μ(s₂)`.
|
MeasureTheory.measure_biUnion_null_iff
theorem MeasureTheory.measure_biUnion_null_iff :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {ι : Type u_6} {s : Set ι},
s.Countable → ∀ {t : ι → Set α}, ↑↑μ (⋃ i ∈ s, t i) = 0 ↔ ∀ i ∈ s, ↑↑μ (t i) = 0
This theorem, `MeasureTheory.measure_biUnion_null_iff`, states that for any type `α` with a `MeasurableSpace` instance, a measure `μ` in measure theory, and any type `ι`, if we have a countable set `s` of type `ι`, then for any function `t` mapping elements of `ι` to sets of `α`, the measure of the union of all sets `t i` for all `i` in `s` is zero if and only if the measure of each individual set `t i` is zero for all `i` in `s`. That is to say, in measure theory, a countable union of sets has measure zero if and only if each of the sets in the union has measure zero.
More concisely: For any countable family of measurable sets in a MeasurableSpace with measure μ, their union has measure zero if and only if each set has measure zero.
|
MeasureTheory.compl_mem_ae_iff
theorem MeasureTheory.compl_mem_ae_iff :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α}, sᶜ ∈ μ.ae ↔ ↑↑μ s = 0 := by
sorry
This theorem states that for any type `α`, any measurable space instance of `α`, any measure `μ` of the measurable space, and any set `s` of `α`, the complement of `s` is in the "almost everywhere" filter of the measure `μ` if and only if the measure of `s` is equal to zero. Here, "almost everywhere" refers to the "almost everywhere" filter of co-null sets, and the measure of a set is a concept from measure theory that intuitively represents the "size" or "volume" of the set. The complement of a set `s` (denoted by `sᶜ`) is the set of elements not in `s`.
More concisely: For any measurable space and measure, a set has zero measure if and only if its complement belongs to the "almost everywhere" filter of co-null sets.
|
MeasureTheory.measure_union_null
theorem MeasureTheory.measure_union_null :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α},
↑↑μ s₁ = 0 → ↑↑μ s₂ = 0 → ↑↑μ (s₁ ∪ s₂) = 0
This theorem, `MeasureTheory.measure_union_null`, states that for any type `α` with an instance of `MeasurableSpace` and for any measure `μ` of type `MeasureTheory.Measure α`, if the measures of two sets `s₁` and `s₂` of type `Set α` are both zero, then the measure of the union of `s₁` and `s₂` is also zero. In mathematical terms, if the measures μ(s₁) and μ(s₂) are both 0, then the measure of the union of the sets, μ(s₁ ∪ s₂), is also 0. This theorem is a statement about the properties of measures in measure theory, a branch of mathematics that studies concepts such as size, volume, and quantity.
More concisely: If two sets in a measurable space have zero measure, then their union also has zero measure.
|
Measurable.comp_aemeasurable
theorem Measurable.comp_aemeasurable :
∀ {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m : MeasurableSpace α} [inst : MeasurableSpace β]
{μ : MeasureTheory.Measure α} [inst_1 : MeasurableSpace δ] {f : α → δ} {g : δ → β},
Measurable g → AEMeasurable f μ → AEMeasurable (g ∘ f) μ
The theorem `Measurable.comp_aemeasurable` states that for all types `α`, `β`, and `δ` and for a given measurable space `α`, measurable spaces `β` and `δ`, a measure `μ` on `α`, and functions `f : α → δ` and `g : δ → β`, if function `g` is measurable and function `f` is almost everywhere measurable with respect to measure `μ`, then the composition of `g` and `f` (denoted as `g ∘ f`) is also almost everywhere measurable with respect to measure `μ`. In more mathematical terms, this theorem says that the composition of a measurable function and an almost everywhere measurable function remains almost everywhere measurable.
More concisely: If `f : α → δ` is almost everywhere measurable and `g : δ → β` is measurable, then their composition `g ∘ f : α → β` is almost everywhere measurable.
|
MeasureTheory.measure_iUnion_null_iff
theorem MeasureTheory.measure_iUnion_null_iff :
∀ {α : Type u_1} {ι : Sort u_5} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : Countable ι]
{s : ι → Set α}, ↑↑μ (⋃ i, s i) = 0 ↔ ∀ (i : ι), ↑↑μ (s i) = 0
The theorem `MeasureTheory.measure_iUnion_null_iff` states that for any type `α`, an index type `ι`, a measurable space over `α`, a measure `μ` on that measurable space, and a countable set `s : ι → Set α`, the measure of the union of all sets in `s` is zero if and only if the measure of each individual set in `s` is zero. In mathematical terms, it asserts that for any collection of subsets `{s_i}` in a measure space `(X, μ)`, we have `μ(⋃ s_i) = 0` if and only if `μ(s_i) = 0` for all `i`.
More concisely: For any measurable space `(X, μ)` and countable collection `{s_i}` of measurable subsets with `μ(s_i) = 0` for all `i`, we have `μ(⋃ s_i) = 0`.
|
Mathlib.MeasureTheory.Measure.MeasureSpaceDef._auxLemma.15
theorem Mathlib.MeasureTheory.Measure.MeasureSpaceDef._auxLemma.15 :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α},
μ.ae.EventuallyEq s ∅ = (↑↑μ s = 0)
This theorem states that for any type `α` with a structure of measurability, any measure `μ` on `α`, and any set `s` of type `α`, the set `s` is almost everywhere equal to the empty set (under the measure `μ`) if and only if the measure of the set `s` is zero. Here, the phrase "almost everywhere" is in the measure-theoretic sense, meaning on the complement of a negligible set.
More concisely: For any measurable type `α`, measure `μ` on `α`, and set `s` of type `α`, `s` is almost everywhere equal to the empty set under `μ` if and only if the measure of `s` is zero.
|
MeasureTheory.ae_eq_set_inter
theorem MeasureTheory.ae_eq_set_inter :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t s' t' : Set α},
μ.ae.EventuallyEq s t → μ.ae.EventuallyEq s' t' → μ.ae.EventuallyEq (s ∩ s') (t ∩ t')
This theorem is about sets and measure theory in the context of mathematics. It states that for any type `α` equipped with a `MeasurableSpace` structure and a measure `μ` on it, and for any four sets `s`, `t`, `s'`, and `t'` of type `α`, if `s` is almost everywhere equal to `t` with respect to the `μ` measure, and if `s'` is almost everywhere equal to `t'` with respect to the same `μ` measure, then the intersection of `s` and `s'` is almost everywhere equal to the intersection of `t` and `t'` with respect to measure `μ`.
In mathematical terms, this theorem asserts that if two sets are almost everywhere equal under a given measure, the same holds true for their intersections with another two sets that are also almost everywhere equal under the same measure. This property is of significant importance in measure theory, a branch of mathematics that studies notions of the size, length, volume, and generalizations.
More concisely: If sets `s`, `t`, `s'`, and `t'` in a measurable space with measure `μ` are pairwise almost equal, then their intersections `s ∩ s'` and `t ∩ t'` are almost equal with respect to `μ`.
|
Filter.EventuallyEq.measure_eq
theorem Filter.EventuallyEq.measure_eq :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α},
μ.ae.EventuallyEq s t → ↑↑μ s = ↑↑μ t
The theorem `Filter.EventuallyEq.measure_eq` states that for any given measurable space `α` and a measure `μ` on this space, if two sets `s` and `t` of type `α` are equivalent except possibly on a set of measure zero (i.e., they are equal modulo a set of measure zero), then the measures of `s` and `t` with respect to `μ` are equal. This is an alias of `MeasureTheory.measure_congr`.
More concisely: If two measurable sets have the same measure zero boundary and are equal almost everywhere, then they have equal measure.
|
MeasureTheory.ae_eq_refl
theorem MeasureTheory.ae_eq_refl :
∀ {α : Type u_1} {δ : Type u_4} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} (f : α → δ),
μ.ae.EventuallyEq f f
This theorem states that for any type `α` with a measurable space structure, any measure `μ` on `α`, and any function `f` from `α` to another type `δ`, the function `f` is equal to itself almost everywhere with respect to the measure `μ`. In other words, any discrepancies between `f` and itself only occur on a set of measure zero.
More concisely: For any measurable function `f` from a measurable space `(α, Σ, μ)` to another measurable space `(δ, τ)`, the sets `{x ∈ α | f x ≠ f x}` and `{x ∈ α | μ({x}) = 0}` have equal measure.
|
MeasureTheory.nonempty_of_measure_ne_zero
theorem MeasureTheory.nonempty_of_measure_ne_zero :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α}, ↑↑μ s ≠ 0 → s.Nonempty := by
sorry
The theorem `MeasureTheory.nonempty_of_measure_ne_zero` states that for any type `α` that has a `MeasurableSpace` instance and for any measure `μ` on `α` and any set `s` of `α`, if the measure of `s` under `μ` is not zero, then the set `s` is nonempty. In simpler terms, if a set has a non-zero measure, it must contain at least one element.
More concisely: If a measurable set in a measurable space has a non-zero measure, then it is nonempty.
|
MeasureTheory.measure_iUnion_null
theorem MeasureTheory.measure_iUnion_null :
∀ {α : Type u_1} {ι : Sort u_5} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : Countable ι]
{s : ι → Set α}, (∀ (i : ι), ↑↑μ (s i) = 0) → ↑↑μ (⋃ i, s i) = 0
The theorem `MeasureTheory.measure_iUnion_null` states that for any type `α` and an indexed type `ι`, given a measurable space over `α`, a measure `μ` on that measurable space, and a countable index set `ι`, if we have a family of sets `s : ι → Set α` such that the measure of each individual set in the family is zero, then the measure of the countable union of these sets is also zero. In mathematical terms, if for all `i` in `ι`, the measure of `s(i)` is zero, then the measure of the union over all `i` in `ι` of `s(i)` is also zero.
More concisely: If `(α, Σ, μ)` is a measurable space, `ι` is a countable index set, and for all `i ∈ ι`, `μ(s i) = 0`, then `μ(⋃ i ∈ ι s i) = 0`.
|
MeasureTheory.mem_ae_iff
theorem MeasureTheory.mem_ae_iff :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α}, s ∈ μ.ae ↔ ↑↑μ sᶜ = 0 := by
sorry
This theorem states that, for any type `α` equipped with a `MeasurableSpace` structure, a measure `μ` of type `MeasureTheory.Measure α`, and a set `s` of type `Set α`, the set `s` belongs to the filter of co-null sets of the measure `μ` (notated as `s ∈ MeasureTheory.Measure.ae μ`) if and only if the measure of the complement of `s` (notated as `μ sᶜ`) equals zero. This means that a set is almost everywhere in the measure space if the measure of its complement is zero.
More concisely: A set in a measurable space belongs to the filter of co-null sets if and only if its complement has measure zero.
|
MeasureTheory.measure_toMeasurable
theorem MeasureTheory.measure_toMeasurable :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} (s : Set α),
↑↑μ (MeasureTheory.toMeasurable μ s) = ↑↑μ s
This theorem, `MeasureTheory.measure_toMeasurable`, states that for any type `α` with a measurable space structure, any measure `μ` of type `MeasureTheory.Measure α`, and any set `s` of type `Set α`, the measure of the set obtained by applying the `MeasureTheory.toMeasurable` operation to `s` under the measure `μ` is equal to the measure of `s` under the same measure `μ`. In more informal terms, this theorem ensures that the operation `MeasureTheory.toMeasurable` does not change the measure of a set.
More concisely: For any measurable space `(α, σ)`, measure `μ : MeasureTheory.Measure α`, and set `s : Set α`, the measure of `toMeasurable s` under `μ` equals the measure of `s` under `μ`.
|
MeasureTheory.Measure.ext
theorem MeasureTheory.Measure.ext :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ₁ μ₂ : MeasureTheory.Measure α},
(∀ (s : Set α), MeasurableSet s → ↑↑μ₁ s = ↑↑μ₂ s) → μ₁ = μ₂
The theorem `MeasureTheory.Measure.ext` establishes the uniqueness of measures in a measurable space. Specifically, for a given measurable space `α`, if two measures `μ₁` and `μ₂` agree on the measure of every measurable set `s`, i.e., `μ₁ s = μ₂ s` for all `s` such that `s` is a measurable set, then the two measures `μ₁` and `μ₂` are identical, i.e., `μ₁ = μ₂`. This means that a measure is entirely determined by its values on measurable sets.
More concisely: If two measures agree on all measurable sets in a measurable space, then they are equal.
|
aemeasurable_id
theorem aemeasurable_id : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}, AEMeasurable id μ
The theorem `aemeasurable_id` states that for any type `α`, any measurable space `m` over `α`, and any measure `μ` on that measurable space, the identity function is almost everywhere measurable. In other words, the identity function coincides almost everywhere with a measurable function.
More concisely: The identity function is almost everywhere measurable with respect to any given measurable space and measure.
|
MeasureTheory.ae_iff
theorem MeasureTheory.ae_iff :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : α → Prop},
(∀ᵐ (a : α) ∂μ, p a) ↔ ↑↑μ {a | ¬p a} = 0
The theorem `MeasureTheory.ae_iff` states that for any measurable space `α` and any measure `μ` on it, a property `p` holds almost everywhere (i.e., everywhere except for a set of measure zero) if and only if the measure of the set of elements for which `p` does not hold is zero. In other words, `p` is true almost everywhere if and only if the measure of the set of exceptions is zero.
More concisely: A property holds almost everywhere in a measurable space with respect to a measure if and only if the measure of the set where the property does not hold is zero.
|
MeasureTheory.exists_measurable_superset_forall_eq
theorem MeasureTheory.exists_measurable_superset_forall_eq :
∀ {α : Type u_1} {ι : Sort u_5} [inst : MeasurableSpace α] [inst_1 : Countable ι] (μ : ι → MeasureTheory.Measure α)
(s : Set α), ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), ↑↑(μ i) t = ↑↑(μ i) s
The theorem `MeasureTheory.exists_measurable_superset_forall_eq` states that for any given set `s` and any countable collection of measures `μ i`, there exists a measurable superset `t` of `s` such that for each measure `μ i`, the measure of `t` is equal to the measure of `s`. Here, `α` is the type of the sets we are measuring, `ι` is the index type for the countable collection of measures, `MeasurableSpace α` is the structure that determines which sets in `α` are measurable, and `Countable ι` means that `ι` is a countable index set. A `MeasureTheory.Measure α` is a measure on the measurable space `α`. The ⊆ symbol denotes subset or equal to, meaning every element of `s` is also an element of `t`.
More concisely: Given any set `s` and a countable collection of measures `μ i` on the measurable space `(α, MeasurableSpace α)`, there exists a measurable superset `t` of `s` such that for all `i`, the measure `μ i(t)` equals `μ i(s)`.
|
MeasureTheory.ae_eq_set_union
theorem MeasureTheory.ae_eq_set_union :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t s' t' : Set α},
μ.ae.EventuallyEq s t → μ.ae.EventuallyEq s' t' → μ.ae.EventuallyEq (s ∪ s') (t ∪ t')
This theorem in Measure Theory, named `MeasureTheory.ae_eq_set_union`, states that for any type `α` with a `MeasurableSpace` instance and a measure `μ` of `MeasureTheory.Measure α`, and for any four sets `s`, `t`, `s'`, and `t'` of type `Set α`, if `s` is almost everywhere equal to `t` under the measure `μ`, and `s'` is almost everywhere equal to `t'` under the same measure, then the union of `s` and `s'` is also almost everywhere equal to the union of `t` and `t'` under the measure `μ`.
In more detail, "almost everywhere" is a concept in measure theory that means "everywhere except on a set of measure zero." If two sets are "almost everywhere equal," it means the set difference between them has measure zero. This theorem is then saying that if `s` and `t` differ only on a set of measure zero, and `s'` and `t'` do as well, then the union of `s` and `s'` and the union of `t` and `t'` also differ only on a set of measure zero.
More concisely: If sets `s`, `t`, `s'`, and `t` in a measurable space `α` are almost everywhere equal to each other under a measure `μ`, then the unions of `s` and `s'` and of `t` and `t'` are almost everywhere equal.
|
MeasureTheory.measure_mono_null
theorem MeasureTheory.measure_mono_null :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α},
s₁ ⊆ s₂ → ↑↑μ s₂ = 0 → ↑↑μ s₁ = 0
The theorem `MeasureTheory.measure_mono_null` states that for any type `α` that forms a measurable space, given a measure `μ` over this space and any two sets `s₁` and `s₂` of `α`, if `s₁` is a subset of `s₂` and the measure of `s₂` is zero, then the measure of `s₁` is also zero. In mathematical terms, if $s₁ \subseteq s₂$ and $\mu(s₂) = 0$ then $\mu(s₁) = 0$. It essentially provides a monotonicity property for measures in a measure space where null sets are inherited by their subsets.
More concisely: If `μ` is a measure on a measurable space `α` and `s₁ ⊆ s₂` with `μ(s₂) = 0`, then `μ(s₁) = 0`. In mathematical notation, `∀ α μ (s₁ s₂ : set α) [measurable_space α μ], s₁ ⊆ s₂ → μ s₂ = 0 → μ s₁ = 0`.
|
MeasureTheory.measure_mono
theorem MeasureTheory.measure_mono :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α},
s₁ ⊆ s₂ → ↑↑μ s₁ ≤ ↑↑μ s₂
This theorem, `MeasureTheory.measure_mono`, states that for every type `α` that forms a measurable space, given any measure `μ` from the `MeasureTheory.Measure` applied to this type, and any two sets `s₁` and `s₂` of this type, if the set `s₁` is a subset of the set `s₂` (denoted by `s₁ ⊆ s₂`), then the measure of set `s₁` (denoted by `μ s₁`) is less than or equal to the measure of set `s₂` (denoted by `μ s₂`). This theorem is fundamental to measure theory as it implies that the measure of a larger set is always greater than or equal to the measure of its subset.
More concisely: For any measurable space (α, Σ, μ), if A ⊆ B in Σ then μ(A) ≤ μ(B).
|