MeasureTheory.Ioi_ae_eq_Ici
theorem MeasureTheory.Ioi_ae_eq_Ici :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.NoAtoms μ]
[inst : PartialOrder α] {a : α}, μ.ae.EventuallyEq (Set.Ioi a) (Set.Ici a)
This theorem states that for every type `α`, measurable space `m0`, measure `μ`, and element `a` of type `α`, where `μ` has no atoms and `α` is partially ordered, the left-open right-infinite interval greater than `a` (denoted as `Set.Ioi a`) is almost everywhere equal (under the measure `μ`) to the left-closed right-infinite interval starting at `a` (denoted as `Set.Ici a`). Here, "almost everywhere" means except on a set of measure zero.
More concisely: For every measurable space `(α, Σ, μ)` without atoms, and every element `a` of a partially ordered type `α`, `Set.Ioi a = Set.Ici a` almost everywhere.
|
MeasureTheory.measure_ne_top
theorem MeasureTheory.measure_ne_top :
∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.IsFiniteMeasure μ]
(s : Set α), ↑↑μ s ≠ ⊤
This theorem states that for any given type `α`, any measurable space `m0` of type `α`, any measure `μ` of the measurable space `α`, and any set `s` of type `α`, the double coercion (or measure) of `μ s` is not equal to positive infinity. In other words, if `μ` is a finite measure, then the measure of any set `s` under this measure `μ` is also finite.
More concisely: For any finite measure μ on measurable space α, the measure μ(s) of any set s in α is finite.
|
Set.Infinite.meas_eq_top
theorem Set.Infinite.meas_eq_top :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasurableSingletonClass α]
{s : Set α}, s.Infinite → (∃ ε, ε ≠ 0 ∧ ∀ x ∈ s, ε ≤ ↑↑μ {x}) → ↑↑μ s = ⊤
The theorem `Set.Infinite.meas_eq_top` states that for any type `α`, given a measurable space `m0` on `α` and a measure `μ` on the measurable space, and for any set `s` of type `α`, if `s` is infinite and there exists a positive real number `ε` such that for every element `x` in `s`, `ε` is less than or equal to the measure of the singleton set `{x}`, then the measure of the set `s` is infinite. This essentially means that if all elements of an infinite set have measure uniformly separated from zero, then the set has infinite measure.
More concisely: If `α` is a type, `m0` is a measurable space on `α`, `μ` is a measure on `m0`, and `s ⊆ α` is an infinite set such that for all `x ∈ s`, the measure `μ({x})` is bounded below by a positive real number, then the measure `μ(s)` is infinite.
|
IsCompact.exists_open_superset_measure_lt_top'
theorem IsCompact.exists_open_superset_measure_lt_top' :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α},
IsCompact s → (∀ x ∈ s, μ.FiniteAtFilter (nhds x)) → ∃ U ⊇ s, IsOpen U ∧ ↑↑μ U < ⊤
The theorem `IsCompact.exists_open_superset_measure_lt_top'` states that if you have a compact set `s` in a topological space, and for every element `x` in `s`, a measure `μ` is finite at the neighborhood of `x`, then there exists an open set `U` that contains `s` such that the measure of `U` is finite. The measure of a set being finite is equivalent to saying that it is not equal to infinity.
More concisely: If every point in a compact set has finite measure in a given topological space, then there exists an open set containing the compact set with finite measure.
|
MeasureTheory.Measure.measure_toMeasurable_inter_of_sum
theorem MeasureTheory.Measure.measure_toMeasurable_inter_of_sum :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
MeasurableSet s →
∀ {t : Set α} {m : ℕ → MeasureTheory.Measure α},
(∀ (n : ℕ), ↑↑(m n) t ≠ ⊤) →
μ = MeasureTheory.Measure.sum m → ↑↑μ (MeasureTheory.toMeasurable μ t ∩ s) = ↑↑μ (t ∩ s)
This theorem states that given a measure space `α` with a measure `μ`, a measurable set `s`, a set `t`, and a sequence of measures `mₙ`, if the measure `μ` is the sum of the measures `mₙ` and the measure of the set `t` under each `mₙ` is finite, then the measure of the intersection of the set `t`'s measurable superset (`toMeasurable μ t`) and `s` under the measure `μ` equals to the measure of the intersection of `t` and `s` under the measure `μ`. In other words, when these conditions are met, the measure of the intersections involving the set `t` and its measurable superset remains the same.
More concisely: Given a measure space `α` with a measure `μ`, a measurable set `s`, a set `t`, and a sequence of finite measures `mₙ` such that `μ = ∑mₙ`, then `μ(t ∩ s) = μ(toMeasurable μ t ∩ s)`.
|
IsCompact.measure_lt_top
theorem IsCompact.measure_lt_top :
∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : TopologicalSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : MeasureTheory.IsFiniteMeasureOnCompacts μ] ⦃K : Set α⦄, IsCompact K → ↑↑μ K < ⊤
This theorem states that for any given type `α` that is a measurable space and a topological space, and any measure `μ` that is finite on compact subsets, if `K` is a compact subset of `α`, then the measure of `K` under `μ` is less than infinity. In simpler terms, it states that a compact subset always has a finite measure when the measure is finite on compact subsets. This highlights a fundamental property of measures in topological spaces, and is an important result in measure theory.
More concisely: If `α` is a measurable and topological space, `μ` is a finite measure on compact subsets of `α`, and `K` is a compact subset of `α`, then the measure of `K` under `μ` is finite.
|
MeasureTheory.ae_iff_measure_eq
theorem MeasureTheory.ae_iff_measure_eq :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.IsFiniteMeasure μ]
{p : α → Prop},
MeasureTheory.NullMeasurableSet {a | p a} μ → ((∀ᵐ (a : α) ∂μ, p a) ↔ ↑↑μ {a | p a} = ↑↑μ Set.univ)
This theorem, `MeasureTheory.ae_iff_measure_eq`, states that for any type `α` with an associated measurable space `m0` and a finite measure `μ`, and any property `p` that elements of `α` might have, if the set of elements satisfying `p` is a null measurable set (i.e., a set that can be approximated by a measurable set up to a set of null measure), then the property `p` holds almost everywhere (i.e., everywhere except on a set of measure zero) if and only if the measure of the set of elements satisfying `p` is the same as the measure of the entire universal set. In other words, if we can approximate the set of elements satisfying `p` well enough, then `p` holds almost everywhere exactly when the set of elements satisfying `p` takes up the whole space in terms of measure.
More concisely: For any measurable space `(α, m0)` with finite measure `μ`, a property `p` on `α` holds almost everywhere if and only if the measure of `{x : α | p x} = μ α`.
|
MeasureTheory.prob_compl_eq_one_sub₀
theorem MeasureTheory.prob_compl_eq_one_sub₀ :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
[inst : MeasureTheory.IsProbabilityMeasure μ], MeasureTheory.NullMeasurableSet s μ → ↑↑μ sᶜ = 1 - ↑↑μ s
This theorem, `MeasureTheory.prob_compl_eq_one_sub₀`, states that for any type `α` with a measurable space structure `m0` and a measure `μ` (that is a probability measure), and any set `s` of type `α` that is a null measurable set with respect to the measure `μ`, the measure of the complement of `s` is equal to `1` minus the measure of `s`. Note, however, that the measure takes values in the extended non-negative real numbers `ℝ≥0∞`, so the subtraction involved is the truncated subtraction of `ℝ≥0∞`, not the standard subtraction operation in `ℝ`.
More concisely: For any measurable space `(α, m0)` with probability measure `μ`, if `s ⊆ α` is a null set, then `μ(compl(s)) = 1 - μ(s)` in the extended non-negative real numbers.
|
MeasureTheory.isProbabilityMeasure_map
theorem MeasureTheory.isProbabilityMeasure_map :
∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
[inst_1 : MeasureTheory.IsProbabilityMeasure μ] {f : α → β},
AEMeasurable f μ → MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map f μ)
The theorem `MeasureTheory.isProbabilityMeasure_map` states that for any types `α` and `β`, given a measurable space on `α`, a measurable space on `β`, a probability measure `μ` on the measurable space of `α`, and a function `f` from `α` to `β` that is almost everywhere measurable, the pushforward measure of `μ` under the function `f` is also a probability measure. This essentially means that if a function is almost everywhere measurable, then transforming a probability measure via this function will still result in a probability measure.
More concisely: Given measurable spaces (α, Σα) and (β, Σβ), a probability measure μ on (α, Σα), a measurable function f : α → β, and ν = μ ∘ f, then ν is a probability measure.
|
MeasureTheory.sfinite_sum_of_countable
theorem MeasureTheory.sfinite_sum_of_countable :
∀ {α : Type u_1} {ι : Type u_4} {m0 : MeasurableSpace α} [inst : Countable ι] (m : ι → MeasureTheory.Measure α)
[inst : ∀ (n : ι), MeasureTheory.IsFiniteMeasure (m n)], MeasureTheory.SFinite (MeasureTheory.Measure.sum m)
This theorem states that a countable sum of finite measures is sigma-finite. More specifically, if we have a measurable space `α`, a countable index set `ι`, and for each index in `ι` we have a finite measure on `α`, then the sum of these measures (obtained via the function `MeasureTheory.Measure.sum`) is a sigma-finite measure on `α`. This theorem is a specialization of a more general result, which is why it is marked as being superseded by the instance below.
More concisely: The sum of a countable collection of finite measures on a measurable space is a sigma-finite measure.
|
MeasureTheory.prob_compl_eq_zero_iff₀
theorem MeasureTheory.prob_compl_eq_zero_iff₀ :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
[inst : MeasureTheory.IsProbabilityMeasure μ], MeasureTheory.NullMeasurableSet s μ → (↑↑μ sᶜ = 0 ↔ ↑↑μ s = 1)
The theorem `MeasureTheory.prob_compl_eq_zero_iff₀` states that for any type `α` equipped with a measurable space `m0` and a probability measure `μ`, and for any set `s` of type `α`, given the condition that `s` is a null-measurable set under measure `μ`, the measure of the complement of `s` is zero if and only if the measure of `s` is one. In other words, if we have a probability measure, and `s` is a set that can be approximated by a measurable set up to a set of null measure, then `s` takes up the entire measure (has measure one) precisely when its complement has no measure (has measure zero).
More concisely: For any measurable set `s` of type `α` in a measurable space `(α, m0)` with probability measure `μ`, `μ(s)^2 + μ(s∘����_* complement)_ = μ(∅)` if and only if `s` has measure one.
|
MeasureTheory.iUnion_spanningSets
theorem MeasureTheory.iUnion_spanningSets :
∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite μ],
⋃ i, MeasureTheory.spanningSets μ i = Set.univ
The theorem `MeasureTheory.iUnion_spanningSets` states that for any type `α` and a measurable space `m0` defined on it, along with a measure `μ` that is sigma finite, the union of the spanning sets of `μ` indexed by all natural numbers equals the universal set. In other words, if we construct a sequence of sets using `MeasureTheory.spanningSets μ i` for all `i ∈ ℕ`, then the union of all these sets encompasses the entire universe of the type `α`. This theorem is a critical step in demonstrating that we can cover the whole space using sets with finite measure, an important concept in measure theory.
More concisely: For any measurable space `(α, m0)` with a sigma-finite measure `μ`, the union of the spanning sets of `μ` is equal to the universal set of `α`.
|
MeasureTheory.ext_of_generate_finite
theorem MeasureTheory.ext_of_generate_finite :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (C : Set (Set α)),
m0 = MeasurableSpace.generateFrom C →
IsPiSystem C →
∀ [inst : MeasureTheory.IsFiniteMeasure μ], (∀ s ∈ C, ↑↑μ s = ↑↑ν s) → ↑↑μ Set.univ = ↑↑ν Set.univ → μ = ν
The theorem `MeasureTheory.ext_of_generate_finite` states that for any type `α`, given a measurable space `m0` on `α` and two finite measures `μ` and `ν` defined on this measurable space, if `m0` is generated from a set `C` and `C` forms a π-system (a collection of subsets that are closed under binary intersection of non-disjoint sets), then if `μ` and `ν` agree on all sets in `C` and on the universal set (the set containing all elements of `α`), then `μ` and `ν` must be equal. This shows that two finite measures on a measurable space generated from a π-system are determined by their values on the set forming the π-system and the universal set.
More concisely: If a measurable space is generated by a π-system `C` and two finite measures agree on all sets in `C` and the universal set, then they are equal.
|
IsCompact.exists_open_superset_measure_lt_top
theorem IsCompact.exists_open_superset_measure_lt_top :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {s : Set α},
IsCompact s →
∀ (μ : MeasureTheory.Measure α) [inst_2 : MeasureTheory.IsLocallyFiniteMeasure μ],
∃ U ⊇ s, IsOpen U ∧ ↑↑μ U < ⊤
The theorem `IsCompact.exists_open_superset_measure_lt_top` states that for any type `α` that is a topological space and a measurable space, and for any set `s` of type `α` that is compact, given a measure `μ` on `α` that is locally finite, there exists an open superset `U` of `s` such that the measure `μ` of `U` is finite. In other words, in a given topological and measurable space, any compact set admits an open superset of finite measure under a locally finite measure.
More concisely: In a locally finite measure on a compact subset of a topological and measurable space, there exists an open superset with finite measure.
|
MeasureTheory.mem_spanningSetsIndex
theorem MeasureTheory.mem_spanningSetsIndex :
∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite μ]
(x : α), x ∈ MeasureTheory.spanningSets μ (MeasureTheory.spanningSetsIndex μ x)
The theorem `MeasureTheory.mem_spanningSetsIndex` states that for any given measurable space `α` and any sigma-finite measure `μ` on this space, for any element `x` in `α`, `x` belongs to the spanning set indexed by the `spanningSetsIndex` of `x`.
In other words, this theorem states that the `spanningSetsIndex` function correctly identifies the least index of the finite spanning set, in a monotone collection of sets that span the universe and have finite measure, that contains a given element `x`.
More concisely: For any measurable space `α` and sigma-finite measure `μ`, and for any `x` in `α`, there exists an index `i` such that `x` is in the i-th set of the finite, monotone collection `spanningSetsIndex μ x`.
|
MeasureTheory.Measure.forall_measure_inter_spanningSets_eq_zero
theorem MeasureTheory.Measure.forall_measure_inter_spanningSets_eq_zero :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : MeasureTheory.SigmaFinite μ]
(s : Set α), (∀ (n : ℕ), ↑↑μ (s ∩ MeasureTheory.spanningSets μ n) = 0) ↔ ↑↑μ s = 0
This theorem states that for a set in a σ-finite measure space, the set is of zero measure if and only if its intersection with each member of the countable family of finite measure spanning sets is of zero measure. In other words, a set has zero measure if it does not overlap with any of the spanning sets of finite measure, or equivalently, if its intersection with every such spanning set has measure zero. This is an important property that connects the measure of a set with the measure of its intersections with a collection of spanning sets.
More concisely: A set in a σ-finite measure space has zero measure if and only if its intersection with every spanning set of finite measure has zero measure.
|
MeasureTheory.Ioo_ae_eq_Ioc
theorem MeasureTheory.Ioo_ae_eq_Ioc :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.NoAtoms μ]
[inst : PartialOrder α] {a b : α}, μ.ae.EventuallyEq (Set.Ioo a b) (Set.Ioc a b)
This theorem states that for any type `α` equipped with a `MeasurableSpace` structure `m0` and a measure `μ` that has no atoms, and a `PartialOrder` structure, the set of all elements `x` between `a` and `b` (exclusive) is equal "almost everywhere" (according to the measure `μ`) to the set of all elements `x` between `a` and `b` where `x` can be equal to `b`. In mathematical terms, this means that the left-open right-open interval $(a, b)$ is almost everywhere equal to the left-open right-closed interval $(a, b]$ with respect to the measure `μ`.
More concisely: For any measurable space `(α, m0)` with no atomic measure `μ`, the sets $(a, b) \neq (a, b]$ differ in measure `μ` by a set of measure 0.
|
MeasureTheory.Measure.countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top
theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top :
∀ {α : Type u_1} {ι : Type u_5} {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) {As : ι → Set α},
(∀ (i : ι), MeasurableSet (As i)) →
Pairwise (Disjoint on As) → ↑↑μ (⋃ i, As i) ≠ ⊤ → {i | 0 < ↑↑μ (As i)}.Countable
This theorem states that if we have a collection of measurable sets (sets which can be measured in the context of an ambient measure space) that are pairwise disjoint, meaning that any two distinct sets from the collection do not share elements, and the union of these sets has finite measure (the total measure is not infinity), then there can only be countably many sets in this collection whose measure is strictly positive. In other words, if we have a finite measure space pieced together from disjoint measurable sets, then only countably many of these pieces can have a positive measure. In the context of measure theory, this theorem helps to characterize the structure of measurable sets in finite measure spaces.
More concisely: In a finite measure space, the number of pairwise disjoint measurable sets with positive measure is countable.
|
MeasureTheory.Measure.exists_isOpen_measure_lt_top
theorem MeasureTheory.Measure.exists_isOpen_measure_lt_top :
∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : TopologicalSpace α] (μ : MeasureTheory.Measure α)
[inst_1 : MeasureTheory.IsLocallyFiniteMeasure μ] (x : α), ∃ s, x ∈ s ∧ IsOpen s ∧ ↑↑μ s < ⊤
This theorem states that for any type `α` with a measurable space structure `m0` and a topological space structure, given a measure `μ` on `α` which is locally finite, for any point `x` in `α`, there exists a set `s` such that `x` belongs to `s`, `s` is an open set in the topological space, and the measure of `s` under `μ` is finite (strictly less than infinity).
More concisely: For any measurable and locally finite measure `μ` on a type `α` with both measurable space and topological space structures, for every point `x` in `α`, there exists an open set `s` containing `x` with finite measure under `μ`.
|
MeasureTheory.Measure.countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀
theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀ :
∀ {α : Type u_1} {ι : Type u_5} {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) {As : ι → Set α},
(∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ) →
Pairwise (MeasureTheory.AEDisjoint μ on As) → ↑↑μ (⋃ i, As i) ≠ ⊤ → {i | 0 < ↑↑μ (As i)}.Countable
This theorem states that if we have a collection of sets, each of which is null-measurable with respect to a given measure, and these sets are almost-everywhere (a.e.) disjoint under the same measure, then if the measure of the union of all these sets is finite (i.e., not equal to infinity), it follows that the number of these sets whose measure is positive must be countable. Here, a set is null-measurable if it can be approximated by a measurable set up to a set of null measure, and two sets are a.e. disjoint if their intersection has measure zero.
More concisely: If a collection of null-measurable sets with finite measure and almost-everywhere disjoint intersections has a countable subcollection with positive measure, then the entire collection has a countable number of sets with positive measure.
|
MeasureTheory.Measure.FiniteAtFilter.exists_mem_basis
theorem MeasureTheory.Measure.FiniteAtFilter.exists_mem_basis :
∀ {α : Type u_1} {ι : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α},
μ.FiniteAtFilter f → ∀ {p : ι → Prop} {s : ι → Set α}, f.HasBasis p s → ∃ i, p i ∧ ↑↑μ (s i) < ⊤
The theorem `MeasureTheory.Measure.FiniteAtFilter.exists_mem_basis` states that for any type `α` and `ι`, a measurable space `m0` on `α`, a measure `μ` of that measurable space, and a filter `f` on `α`, if the measure `μ` is finite at the filter `f`, then for any property `p` on `ι` and any function `s` from `ι` to the set of `α`, if the filter `f` has a basis characterized by the property `p` and the function `s`, there exists an element `i` in `ι` such that the property `p` holds for `i` and the measure of `s(i)` is finite.
This means that when a measure is finite at a filter, it is also finite at some element of any basis of that filter, as long as the basis satisfies certain conditions. This is a statement about the connection between measure theory and filter bases in mathematical analysis.
More concisely: Given a measurable space `(α, m0)`, measure `μ`, filter `f`, property `p` on `ι`, and function `s` from `ι` to `α`, if `μ` is finite at `f` and `f` has a basis characterized by `p` and `s`, then there exists an `i` in `ι` such that `p(i)` holds and `μ(s(i))` is finite.
|
MeasureTheory.Measure.FiniteAtFilter.of_inf_ae
theorem MeasureTheory.Measure.FiniteAtFilter.of_inf_ae :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α},
μ.FiniteAtFilter (f ⊓ μ.ae) → μ.FiniteAtFilter f
This theorem, `MeasureTheory.Measure.FiniteAtFilter.of_inf_ae` in Lean 4, states that for any type `α`, any measurable space `m0` on `α`, any measure `μ` in that space, and any filter `f` on `α`, if the measure `μ` is finite at the intersection of the filter `f` and the almost-everywhere filter of `μ` (i.e., the set of elements for which `μ` isn't zero), then `μ` is also finite at the filter `f`. Essentially, it's a way to conclude that a measure is finite at a particular filter given that it's finite at the intersection of that filter with the measure's almost-everywhere filter.
More concisely: If a measure `μ` on a measurable space `(α, m0)` is finite almost everywhere and finite on the intersection of any filter `f` with the almost-everywhere filter, then `μ` is finite on `f`.
|
MeasureTheory.Ioo_ae_eq_Icc
theorem MeasureTheory.Ioo_ae_eq_Icc :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.NoAtoms μ]
[inst : PartialOrder α] {a b : α}, μ.ae.EventuallyEq (Set.Ioo a b) (Set.Icc a b)
This theorem states that for any type `α`, given a measurable space `m0` over `α`, a measure `μ` on `α` that has no atoms, and a partial order on `α`, for any two elements `a` and `b` of `α` the left-open right-open interval `(a, b)` is equal "almost everywhere" (according to the measure `μ`) to the left-closed right-closed interval `[a, b]`. In other words, apart from a set of measure zero (which may contain countably many points), the open interval `(a, b)` and the closed interval `[a, b]` are the same.
More concisely: For any measurable space, measure without atoms, and partial order on a type `α`, the left-open right-open interval `(a, b)` and the left-closed right-closed interval `[a, b]` differ only on a set of measure zero.
|
MeasureTheory.Measure.measure_toMeasurable_inter_of_cover
theorem MeasureTheory.Measure.measure_toMeasurable_inter_of_cover :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
MeasurableSet s →
∀ {t : Set α} {v : ℕ → Set α},
t ⊆ ⋃ n, v n → (∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤) → ↑↑μ (MeasureTheory.toMeasurable μ t ∩ s) = ↑↑μ (t ∩ s)
The theorem `MeasureTheory.Measure.measure_toMeasurable_inter_of_cover` states that for any type `α` with a measurable space `m0` and a measure `μ`, if a set `t` is covered by a countable family of finite measure sets `v`, then its measurable superset `toMeasurable μ t` (which has the same measure as `t`) satisfies an equality for any measurable set `s`. Specifically, the measure of the intersection of `toMeasurable μ t` and `s` is the same as the measure of the intersection of `t` and `s`. Here, `≠ ⊤` indicates that the measures are finite.
More concisely: For any measurable space `(α, m0)` and measure `μ` on `α`, if `t` is a set with finite measure and is covered by a countable family of measurable sets `v` with finite measure, then `toMeasurable μ t` intersect `s` has the same finite measure as `t` intersect `s`, for any measurable set `s`.
|
Set.Countable.measure_zero
theorem Set.Countable.measure_zero :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α},
s.Countable → ∀ (μ : MeasureTheory.Measure α) [inst : MeasureTheory.NoAtoms μ], ↑↑μ s = 0
The theorem `Set.Countable.measure_zero` states that for any type `α`, any measurable space `m0` over `α`, any set `s` of the type `α`, and any measure `μ` in the measure theory over `α`, if the set `s` is countable, then under the assumption that the measure `μ` has no atoms, the measure `μ` of the set `s` is always zero. This essentially means that countable sets have measure zero in a measure space where the measure has no atoms.
More concisely: If `μ` is a measure on a countable measurable set `s` in a measure space without atoms, then `μ(s) = 0`.
|
MeasureTheory.Measure.finite_const_le_meas_of_disjoint_iUnion₀
theorem MeasureTheory.Measure.finite_const_le_meas_of_disjoint_iUnion₀ :
∀ {α : Type u_1} {ι : Type u_5} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {ε : ENNReal},
0 < ε →
∀ {As : ι → Set α},
(∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ) →
Pairwise (MeasureTheory.AEDisjoint μ on As) → ↑↑μ (⋃ i, As i) ≠ ⊤ → {i | ε ≤ ↑↑μ (As i)}.Finite
The theorem `MeasureTheory.Measure.finite_const_le_meas_of_disjoint_iUnion₀` states that if a family of almost everywhere (a.e.) disjoint null-measurable sets forms a union with finite measure, then there can only be finitely many sets in this family that have a measure exceeding a given positive number. This is under the assumption that the measure of the union of these sets is not infinite and that the given positive number is greater than zero.
In other words, given a measure space and a sequence of sets that are null-measurable and pairwise almost everywhere disjoint, if the measure of the union of these sets is finite and a positive threshold exists, then the number of sets with a measure greater than or equal to this threshold is finite.
More concisely: If a family of null-measurable, a.e. disjoint sets has finite union measure, then there are only finitely many sets with measure exceeding a given positive number.
|
MeasureTheory.prob_compl_eq_one_sub
theorem MeasureTheory.prob_compl_eq_one_sub :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
[inst : MeasureTheory.IsProbabilityMeasure μ], MeasurableSet s → ↑↑μ sᶜ = 1 - ↑↑μ s
The theorem `MeasureTheory.prob_compl_eq_one_sub` states that for any type `α`, given a measurable space `m0` over `α`, a measure `μ` under the measure theory structure, and a set `s` of type `α`, if `μ` is a probability measure, and `s` is a measurable set, then the measure of the complement of `s` is equal to `1` minus the measure of `s`. Note that the measure values are in the nonnegative extended real numbers `ℝ≥0∞`, which means the subtraction involved is the truncated subtraction of `ℝ≥0∞`, not the standard subtraction of `ℝ`.
More concisely: For any measurable space `(α, m0)`, measurable set `s` of type `α`, and probability measure `μ` on `m0`, we have `μ(s.complement) = 1 - μ(s)`.
|
MeasureTheory.isFiniteMeasure_of_le
theorem MeasureTheory.isFiniteMeasure_of_le :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {ν : MeasureTheory.Measure α} (μ : MeasureTheory.Measure α)
[inst : MeasureTheory.IsFiniteMeasure μ], ν ≤ μ → MeasureTheory.IsFiniteMeasure ν
This theorem states that for any type `α`, given a measurable space `m0` over `α` and two measure theories `ν` and `μ` over `α`, if `μ` is a finite measure and `ν` is less than or equal to `μ`, then `ν` is also a finite measure. In mathematical terms, if `μ` is a finite measure (i.e., the measure of the entire space is finite) and `ν` is a measure such that for all measurable sets `A`, `ν(A) ≤ μ(A)`, then `ν` is also a finite measure.
More concisely: If `μ` is a finite measure over a measurable space `α` and `ν` is a measure over `α` with `ν(A) ≤ μ(A)` for all measurable sets `A`, then `ν` is also a finite measure.
|
MeasureTheory.measurable_spanningSets
theorem MeasureTheory.measurable_spanningSets :
∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite μ]
(i : ℕ), MeasurableSet (MeasureTheory.spanningSets μ i)
This theorem states that for any measure space `α` with a measurable space structure `m0` and a sigma finite measure `μ`, and for any natural number `i`, the `i`-th set in the sequence of sets that spans the entire space `α` and have finite measure (obtained by `MeasureTheory.spanningSets μ i`) is a measurable set. In other words, every set in this sequence of spanning sets is measurable.
More concisely: For any measure space `(α, m0, μ)` and natural number `i`, the `i`-th set in the sequence of measurable sets with finite measure spanning `α` (obtained by `MeasureTheory.spanningSets μ i`) is measurable.
|
MeasureTheory.Measure.FiniteSpanningSetsIn.sigmaFinite
theorem MeasureTheory.Measure.FiniteSpanningSetsIn.sigmaFinite :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {C : Set (Set α)},
μ.FiniteSpanningSetsIn C → MeasureTheory.SigmaFinite μ
This theorem states that if a measure `μ`, defined on a measurable space `α`, has finite spanning sets in a collection of measurable sets `C`, then `μ` is `σ`-finite. This means that it can be decomposed into a countable union of sets with finite measure. The theorem is a property in the field of measure theory, which is a branch of mathematics that studies concepts such as length, area, and volume in a more general and abstract way than traditional geometry and calculus.
More concisely: If a measure μ on a measurable space α has finite spanning sets for every countable collection of measurable sets, then μ is σ-finite.
|
MeasureTheory.Measure.FiniteAtFilter.filter_mono
theorem MeasureTheory.Measure.FiniteAtFilter.filter_mono :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : Filter α},
f ≤ g → μ.FiniteAtFilter g → μ.FiniteAtFilter f
This theorem states that for any measurable space `α` and measure `μ` on `α`, and any two filters `f` and `g` on `α`, if `f` is a sub-filter of `g` (denoted as `f ≤ g`), then if the measure `μ` is finite at filter `g`, it must also be finite at filter `f`. In other words, if a measure is finite for a large filter, it's also finite for any smaller filter contained within the larger filter.
More concisely: If `μ` is a finite measure on a measurable space `α`, and `f` is a sub-filter of `g` on `α`, then `μ` is also finite at filter `f`.
|
Bornology.IsBounded.measure_lt_top
theorem Bornology.IsBounded.measure_lt_top :
∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : PseudoMetricSpace α] [inst_1 : ProperSpace α]
{μ : MeasureTheory.Measure α} [inst_2 : MeasureTheory.IsFiniteMeasureOnCompacts μ] ⦃s : Set α⦄,
Bornology.IsBounded s → ↑↑μ s < ⊤
The theorem `Bornology.IsBounded.measure_lt_top` states that for any type `α` that forms a measurable space, is a pseudometric space, and is a proper space with a given measure `μ` that is finite on compact sets and for any set `s` of type `α`, if `s` is bounded relative to the ambient bornology on `α`, then the measure of `s` is less than infinity. In other words, in a proper space, a bounded subset's measure is finite for a measure which is finite on compact sets.
More concisely: In a proper measurable space with a finite-on-compacts measure, a bounded set has finite measure.
|
MeasureTheory.Measure.exists_measure_inter_spanningSets_pos
theorem MeasureTheory.Measure.exists_measure_inter_spanningSets_pos :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : MeasureTheory.SigmaFinite μ]
(s : Set α), (∃ n, 0 < ↑↑μ (s ∩ MeasureTheory.spanningSets μ n)) ↔ 0 < ↑↑μ s
This theorem states that for a set in a sigma-finite measurable space, the set has positive measure if and only if there is a positive measure when intersecting the set with some member of the countable family of finite measure spanning sets. In other words, if a set has positive measure in the sigma-finite space, there must exist an index such that when this set intersects with the finite measure spanning set at that index, the resulting set also has positive measure. Conversely, if such an index exists, then the original set must have had positive measure.
More concisely: A set in a sigma-finite measurable space has positive measure if and only if there exists a finite measure spanning set index such that the intersection of the set with that spanning set has positive measure.
|
MeasureTheory.SigmaFinite.out
theorem MeasureTheory.SigmaFinite.out :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α},
MeasureTheory.SigmaFinite μ → Nonempty (μ.FiniteSpanningSetsIn Set.univ)
The theorem `MeasureTheory.SigmaFinite.out` states that for any type `α`, given a measurable space `m0` on `α` and a measure `μ` on this measurable space, if the measure `μ` is sigma-finite, then there exists a nonempty set of finite spanning sets in the universal set of `α` with respect to this measure `μ`. In simpler words, if a measure is sigma-finite (i.e., it can be partitioned into a countable union of sets with finite measure), then we can find a nonempty collection of finite spanning sets that cover the entire space.
More concisely: Given a sigma-finite measure `μ` on a measurable space `(α, m0)`, there exists a countable collection `{S_i}` of finite sets in `α` such that `α = ⋃i (S_i)`.
|
MeasureTheory.measure_spanningSets_lt_top
theorem MeasureTheory.measure_spanningSets_lt_top :
∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite μ]
(i : ℕ), ↑↑μ (MeasureTheory.spanningSets μ i) < ⊤
This theorem states that for any measurable space `α`, associated measure `μ`, and natural number `i`, the measure of the `i-th` spanning set is less than infinity. Here, the spanning sets are created from a monotone collection of sets that span the entire universe and have finite measure. This holds true for all sigma-finite measures, which are measures where the entire space can be partitioned into a countable collection of sets with finite measure.
More concisely: For any sigma-finite measure space `(α, Σ, μ)` and monotone, finite-measure cover `{A_i}` of `α`, the sum `μ(⋃i:ℕ. A_i)` is finite.
|
MeasureTheory.Measure.le_of_add_le_add_left
theorem MeasureTheory.Measure.le_of_add_le_add_left :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν₁ ν₂ : MeasureTheory.Measure α}
[inst : MeasureTheory.IsFiniteMeasure μ], μ + ν₁ ≤ μ + ν₂ → ν₁ ≤ ν₂
The theorem `MeasureTheory.Measure.le_of_add_le_add_left` states that for any measurable space `α` and any three measures `μ`, `ν₁`, and `ν₂` on this space (where `μ` is finite), if the sum of `μ` and `ν₁` is less than or equal to the sum of `μ` and `ν₂`, then `ν₁` must be less than or equal to `ν₂`. This theorem is typically applicable to the mathematical structure `OrderedCancelAddCommMonoid`, but it also holds true for measures under the additional assumption that `μ` is finite.
More concisely: If `μ` is a finite measurable function on the measurable space `α` and `μ + ν₁ ≤ mu + ν₂`, then `ν₁ ≤ ν₂`.
|
MeasureTheory.Measure.add_right_inj
theorem MeasureTheory.Measure.add_right_inj :
∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ ν₁ ν₂ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite μ],
μ + ν₁ = μ + ν₂ ↔ ν₁ = ν₂
This theorem states that for any type 'α', given a measurable space 'm0' over 'α', and three measures 'μ', 'ν₁' and 'ν₂' on this space, if 'μ' is a sigma-finite measure, then the equality of the sum of 'μ' and 'ν₁' with the sum of 'μ' and 'ν₂' implies the equality of 'ν₁' and 'ν₂'. In other words, if two sums of measures are equal, and one measure in both sums is the same and sigma-finite, then the other measures in the sums must be equal.
More concisely: If 'μ' is a sigma-finite measure on measurable space '(α, m0)', and 'ν₁' and 'ν₂' are measures on '(α, m0)', then 'ν₁ = ν₂' given 'μ + ν₁ = μ + ν₂'.
|
MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict'
theorem MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict' :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (ν : MeasureTheory.Measure α)
[inst : MeasureTheory.SigmaFinite μ] [inst : MeasureTheory.SigmaFinite ν] (P : α → Prop),
(∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ↑↑ν s < ⊤ → ∀ᵐ (x : α) ∂μ.restrict s, P x) → ∀ᵐ (x : α) ∂μ, P x
This theorem, `MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict'`, states that for any type `α` with a measurable space `m0`, and any two sigma-finite measures `μ` and `ν` on this measurable space, if a property `P` holds almost everywhere (except possibly on a set of measure zero) with respect to the measure `μ` restricted to any measurable set `s` such that both the measures `μ` and `ν` of `s` are finite, then the property `P` also holds almost everywhere with respect to the measure `μ` on the entire space.
In other words, if for all measurable sets `s` with finite measures under `μ` and `ν`, a property `P` holds for almost all elements in `s` (with respect to the measure `μ`), then `P` holds for almost all elements in the entire measurable space (with respect to the measure `μ`).
More concisely: If a property holds almost everywhere with respect to the restriction of two sigma-finite measures `μ` and `ν` on a measurable space `α` for all measurable sets `s` with finite measures under both `μ` and `ν`, then the property holds almost everywhere with respect to `μ` on the entire measurable space `α`.
|
MeasureTheory.Measure.exists_subset_measure_lt_top
theorem MeasureTheory.Measure.exists_subset_measure_lt_top :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
[inst : MeasureTheory.SigmaFinite μ] {r : ENNReal},
MeasurableSet s → r < ↑↑μ s → ∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < ↑↑μ t ∧ ↑↑μ t < ⊤
This theorem states that in a sigma-finite measure space, given a measurable set whose measure is greater than a real number 'r', there exists a measurable subset whose measure is greater than 'r' but less than infinity.
In simpler terms, if you have a large measurable set (of size greater than 'r') in a space where all sets can be broken down into countably many finite pieces, you can always find a smaller measurable subset within it that's still larger than 'r' in size, but not infinitely large.
More concisely: In a sigma-finite measure space, given a measurable set with positive finite measure, there exists a measurable subset with strictly greater positive measure.
|
MeasureTheory.Measure.finite_const_le_meas_of_disjoint_iUnion
theorem MeasureTheory.Measure.finite_const_le_meas_of_disjoint_iUnion :
∀ {α : Type u_1} {ι : Type u_5} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {ε : ENNReal},
0 < ε →
∀ {As : ι → Set α},
(∀ (i : ι), MeasurableSet (As i)) →
Pairwise (Disjoint on As) → ↑↑μ (⋃ i, As i) ≠ ⊤ → {i | ε ≤ ↑↑μ (As i)}.Finite
The theorem `MeasureTheory.Measure.finite_const_le_meas_of_disjoint_iUnion` states that if we have a collection of disjoint measurable sets (denoted by `As : ι → Set α`) and the measure of their union (under a measure `μ`) is finite, then given any positive real number `ε` (from the extended nonnegative real numbers, `ENNReal`), the set of indices `i` for which the measure of `As i` is greater than or equal to `ε` is finite. That is, there are only finitely many sets in the collection whose measure exceeds `ε`. This holds true for every measure space `α` and index type `ι`.
More concisely: Given a finite measure space `α` with index type `ι`, if `As : ι → Set α` is a family of disjoint measurable sets and `μ(⋃i:ι. As i)` is finite, then for every `ε > 0` in the extended nonnegative reals `ENNReal`, the set `{ i : ι | μ(As i) ≥ ε }` is finite.
|
MeasureTheory.Measure.measure_toMeasurable_inter_of_sFinite
theorem MeasureTheory.Measure.measure_toMeasurable_inter_of_sFinite :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SFinite μ]
{s : Set α}, MeasurableSet s → ∀ (t : Set α), ↑↑μ (MeasureTheory.toMeasurable μ t ∩ s) = ↑↑μ (t ∩ s)
The theorem `MeasureTheory.Measure.measure_toMeasurable_inter_of_sFinite` states that for any measurable space `α` with a measure `μ` that is s-finite (s-finite measures are a subset of σ-finite measures), for any measurable set `s` and any set `t`, the measure of the intersection of the measurable superset `toMeasurable μ t` of `t` (which has the same measure as `t`) and `s` is equal to the measure of the intersection of `t` and `s`. This theorem requires that the measure `μ` is s-finite. There is an alternative version of this theorem that doesn't require this assumption, but does require that `t` has finite measure, named `measure_toMeasurable_inter`.
More concisely: For an s-finite measurable space with measure μ, the measure of the intersection of any measurable sets t and s is equal to the measure of their intersection in the measurable superset toMeasurable μ t of t.
|
measure_Icc_lt_top
theorem measure_Icc_lt_top :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [inst_2 : CompactIccSpace α]
{m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ] {a b : α},
↑↑μ (Set.Icc a b) < ⊤
This theorem states that for any given type `α`, with a pre-order relation, a topology, and a condition that every interval `[a, b]` is compact, and given a measurable space over `α` and a measure `μ` on it which is locally finite, then the measure of any closed interval `[a, b]` is strictly less than infinity. In other words, the measure of any closed interval in such a space is always finite.
More concisely: For any type `α` with a pre-order relation, a topology, and the property that every interval is compact; if we have a measurable space over `α` with a locally finite measure `μ`, then the measure of any closed interval is finite.
|
MeasureTheory.Ioc_ae_eq_Icc
theorem MeasureTheory.Ioc_ae_eq_Icc :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.NoAtoms μ]
[inst : PartialOrder α] {a b : α}, μ.ae.EventuallyEq (Set.Ioc a b) (Set.Icc a b)
The theorem `MeasureTheory.Ioc_ae_eq_Icc` states that for any measurable space `α`, any measure `μ` on `α` which has no atoms (single-point sets with positive measure), and any partial order on `α`, the left-open right-closed interval from `a` to `b` (denoted `Set.Ioc a b`) is almost everywhere equal to the left-closed right-closed interval from `a` to `b` (denoted `Set.Icc a b`) with respect to the measure `μ`. In other words, the set of points where these two intervals differ has measure zero.
More concisely: For any measurable space `(α, Σ, μ)` with no atoms, and any `a < b` in `α`, the sets `Set.Ioc a b` and `Set.Icc a b` have equal measure.
|
MeasureTheory.monotone_spanningSets
theorem MeasureTheory.monotone_spanningSets :
∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite μ],
Monotone (MeasureTheory.spanningSets μ)
The theorem `MeasureTheory.monotone_spanningSets` states that for any measurable space `α` and any sigma-finite measure `μ` on that space, the function `MeasureTheory.spanningSets μ` is monotone. In other words, if `i ≤ j` for two natural numbers `i` and `j`, then the set spanned by the sigma-finite measure `μ` up to the `i`-th step is a subset of or equal to the set spanned by the sigma-finite measure `μ` up to the `j`-th step. This is important because it guarantees that as we consider more steps in the construction of our spanning sets, we only ever add to our sets and never remove from them.
More concisely: For any measurable space and sigma-finite measure, the sequence of sets obtained by successively increasing the steps in the construction of their spanning sets forms a monotonic sequence.
|
MeasureTheory.Measure.finiteAt_nhdsWithin
theorem MeasureTheory.Measure.finiteAt_nhdsWithin :
∀ {α : Type u_1} [inst : TopologicalSpace α] {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α)
[inst_1 : MeasureTheory.IsLocallyFiniteMeasure μ] (x : α) (s : Set α), μ.FiniteAtFilter (nhdsWithin x s)
The theorem `MeasureTheory.Measure.finiteAt_nhdsWithin` states that for any type `α` with a topological and measurable space structure, any measure `μ` that is locally finite, any element `x` of type `α`, and any set `s` of type `α`, the measure `μ` is finite at the filter `nhdsWithin x s`. Here, `nhdsWithin x s` represents the "neighborhood within" filter, which includes sets containing the intersection of `s` and a neighborhood of `x`. In other words, the measure of the neighborhood of `x` within the set `s` is finite.
More concisely: For any locally finite measure `μ` on a topological and measurable space `(α, τ, μ)`, `μ` is finite on the filter of neighborhoods of a point `x` in a set `s`, i.e., `μ(nhdsWithin x s) < ∞`.
|
MeasureTheory.Ioo_ae_eq_Ico
theorem MeasureTheory.Ioo_ae_eq_Ico :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.NoAtoms μ]
[inst : PartialOrder α] {a b : α}, μ.ae.EventuallyEq (Set.Ioo a b) (Set.Ico a b)
This theorem states that for any type `α` that has a measurable space structure, a measure `μ` with no atoms, and a partial order, and for any two elements `a` and `b` in `α`, the left-open right-open interval from `a` to `b` is "almost everywhere" equal to the left-closed right-open interval from `a` to `b` with respect to the measure `μ`. Here "almost everywhere" means except on a set of measure zero. In other words, the set of elements that are strictly greater than `a` and strictly less than `b` (denoted as `Set.Ioo a b`) is the same as the set of elements that are greater than or equal to `a` and strictly less than `b` (denoted as `Set.Ico a b`) except possibly for a set of measure zero.
More concisely: For any measurable space `(α, Σ, μ)` with no atoms, for all `a < b` in `α`, the sets `Set.Ioo a b` and `Set.Ico a b` differ only in a set of measure zero.
|
MeasureTheory.Measure.countable_meas_pos_of_disjoint_iUnion₀
theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_iUnion₀ :
∀ {α : Type u_1} {ι : Type u_5} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : MeasureTheory.SFinite μ] {As : ι → Set α},
(∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ) →
Pairwise (MeasureTheory.AEDisjoint μ on As) → {i | 0 < ↑↑μ (As i)}.Countable
The theorem states that in a sigma-finite measure space, among a collection of disjoint null-measurable sets, only a countable number of them can have positive measure. This means that if you have a measurable space and a measure on it which is sigma-finite (i.e., it can be decomposed into a countable union of finite measure sets), and if you have a collection of sets such that each is null-measurable and any two of them are almost everywhere disjoint (i.e., their intersection has measure zero), then the set of indices for which the corresponding set has positive measure is countable.
More concisely: In a sigma-finite measure space, the number of disjoint null-measurable sets with positive measure is countable.
|
MeasureTheory.IsProbabilityMeasure.ne_zero
theorem MeasureTheory.IsProbabilityMeasure.ne_zero :
∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α)
[inst : MeasureTheory.IsProbabilityMeasure μ], μ ≠ 0
In natural language, this theorem states that for any type `α` and any measurable space 'm0' over `α`, if `μ` is a probability measure, then `μ` is not equal to zero. In other words, all probability measures are non-zero in the context of the measurable space.
More concisely: For any measurable space (α, m\_,) and probability measure μ on (α, m\_), μ ≠ 0.
|
MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict
theorem MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SigmaFinite μ]
(P : α → Prop),
(∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∀ᵐ (x : α) ∂μ.restrict s, P x) → ∀ᵐ (x : α) ∂μ, P x
The theorem `MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict` states that for any type `α`, measurable space `m0`, measure `μ` that is σ-finite, and a property `P` that is defined for `α`, if for every measurable set `s` with the measure less than infinity, the property `P` holds almost everywhere in the measure space restricted to `s`, then `P` holds almost everywhere in the original measure space.
In simpler terms, if a property is true almost everywhere in all measurable subsets with finite measure of a space, then that property is true almost everywhere in the entire space.
More concisely: If a property holds almost everywhere in every measurable subset of a σ-finite measure space with finite measure, then it holds almost everywhere in the entire measure space.
|
MeasureTheory.Measure.finiteAt_nhds
theorem MeasureTheory.Measure.finiteAt_nhds :
∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : TopologicalSpace α] (μ : MeasureTheory.Measure α)
[inst_1 : MeasureTheory.IsLocallyFiniteMeasure μ] (x : α), μ.FiniteAtFilter (nhds x)
This theorem states that for any type `α`, given a measurable space `m0` and a topological space instance on `α`, for any measure `μ` (which is a locally finite measure) and for any element `x` of `α`, the measure `μ` is finite at the neighborhood filter of `x`. In other words, there exists some neighborhood of `x` where the measure `μ` is finite. Note that a neighborhood of `x` is a set containing an open set around `x` and a measure is considered finite at a filter if it's finite at some set within the filter.
More concisely: For any measurable space, topological space instance, locally finite measure, and element in the space, there exists a finite measure value at some open neighborhood of that element.
|
MeasureTheory.measure_lt_top
theorem MeasureTheory.measure_lt_top :
∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.IsFiniteMeasure μ]
(s : Set α), ↑↑μ s < ⊤
This theorem states that for any type `α` and a given measurable space `m0` over `α`, any set `s` in this space, and a measure `μ` which is finite, the measure `μ` of set `s` is always less than infinity (`⊤`). Essentially, it ensures that, within a finite measure, the measure of any particular set is also finite.
More concisely: For any measurable space `(α, m0)`, finite measure `μ` over `α`, and measurable set `s` in `α`, we have `μ(s) < ⊤`.
|
MeasureTheory.Iio_ae_eq_Iic
theorem MeasureTheory.Iio_ae_eq_Iic :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.NoAtoms μ]
[inst : PartialOrder α] {a : α}, μ.ae.EventuallyEq (Set.Iio a) (Set.Iic a)
This theorem states that for any type `α`, a measurable space `m0` over `α`, a measure `μ` on the measurable space that has no atoms, and a partial order on `α`, for any element `a` of `α`, the left-infinite right-open interval (Set.Iio a) is 'almost everywhere' equal to the left-infinite right-closed interval (Set.Iic a) under the measure `μ`. Here, 'almost everywhere' means that the set difference of these two intervals has measure zero. In other words, except possibly on a set of measure zero, every element that is strictly less than `a` (from Set.Iio a) is also less than or equal to `a` (from Set.Iic a).
More concisely: For any measurable space `(α, m0)`, measure `μ` with no atoms, and partial order on `α`, the left-infinite right-open and left-infinite right-closed intervals of any element `a` in `α` have measure-theoretic equality (i.e., their symmetric difference has measure zero).
|
MeasureTheory.Measure.countable_meas_pos_of_disjoint_iUnion
theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_iUnion :
∀ {α : Type u_1} {ι : Type u_5} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : MeasureTheory.SFinite μ] {As : ι → Set α},
(∀ (i : ι), MeasurableSet (As i)) → Pairwise (Disjoint on As) → {i | 0 < ↑↑μ (As i)}.Countable
This theorem declares that in a sigma-finite measure space, among a collection of disjoint measurable sets, only a countable number of them can have positive measure. Here, "sigma-finite" means the entire space can be partitioned into a countable union of measurable sets with finite measure. The measurable sets are parameterized by an index type `ι` and are represented as a function `As : ι → Set α`. This theorem assumes that each set `As i` is measurable and that all the sets `As i` and `As j` are disjoint for `i ≠ j`. Under these conditions, the theorem guarantees that the set of indices `i` such that the measure of `As i` is positive is countable.
More concisely: In a sigma-finite measure space, the number of disjoint measurable sets among a collection parameterized by an index type `ι` with positive measure is countable.
|
MeasureTheory.sum_sFiniteSeq
theorem MeasureTheory.sum_sFiniteSeq :
∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [h : MeasureTheory.SFinite μ],
MeasureTheory.Measure.sum (MeasureTheory.sFiniteSeq μ) = μ
This theorem, `MeasureTheory.sum_sFiniteSeq`, states that for any measurable space `α` and any measure `μ` on that space, if `μ` is sigma-finite (that is, it can be decomposed into a countable union of sets with finite measure), then the sum of the sequence of finite measures `sFiniteSeq μ` is equal to `μ` itself. In other words, a sigma-finite measure can be broken down into a sequence of finite measures that, when summed, reconstruct the original measure.
More concisely: For any sigma-finite measure `μ` on a measurable space `α`, the sum of the sequence of its finite measure decompositions equals `μ`.
|
MeasureTheory.null_of_locally_null
theorem MeasureTheory.null_of_locally_null :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace α]
[inst_1 : SecondCountableTopology α] (s : Set α), (∀ x ∈ s, ∃ u ∈ nhdsWithin x s, ↑↑μ u = 0) → ↑↑μ s = 0
This theorem states that if for every point in a certain set, there exists a neighborhood within that set around the point that has zero measure, then the whole set itself has zero measure, provided that the space is second-countable. Here, a measure provides a way to assign a number to subsets of a space which can be thought of as their 'size' or 'volume'. A second-countable space is a topological space where there exists a countable basis for the topology. The neighborhood within a point in a set is the intersection of the set with some open set containing the point.
More concisely: If a second-countable set has the property that every point has a neighborhood with zero measure, then the entire set has zero measure.
|
MeasureTheory.prob_le_one
theorem MeasureTheory.prob_le_one :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
[inst : MeasureTheory.IsProbabilityMeasure μ], ↑↑μ s ≤ 1
This theorem states that for any type `α`, any measurable space `m0` of type `α`, any measure `μ` of the measurable space `α`, and any set `s` of type `α`, if `μ` is a probability measure, then the measure `μ(s)` of the set `s` is less than or equal to one. In mathematical terms, if `μ` is a probability measure on a measurable space, then for any set `s` in that space, the measure of `s` (denoted as `μ(s)`) is bounded by 1.
More concisely: For any probability measure `μ` on a measurable space `(α, m0)`, the measure of any set `s` in `α` satisfies `μ(s) ≤ 1`.
|
MeasureTheory.ext_on_measurableSpace_of_generate_finite
theorem MeasureTheory.ext_on_measurableSpace_of_generate_finite :
∀ {α : Type u_5} (m₀ : MeasurableSpace α) {μ ν : MeasureTheory.Measure α} [inst : MeasureTheory.IsFiniteMeasure μ]
(C : Set (Set α)),
(∀ s ∈ C, ↑↑μ s = ↑↑ν s) →
∀ {m : MeasurableSpace α},
m ≤ m₀ →
m = MeasurableSpace.generateFrom C →
IsPiSystem C → ↑↑μ Set.univ = ↑↑ν Set.univ → ∀ {s : Set α}, MeasurableSet s → ↑↑μ s = ↑↑ν s
This theorem states that if two finite measures, μ and ν, assign the same mass to the entire space and agree on a π-system made of measurable sets, then they will agree on all sets in the σ-algebra generated by the π-system. Here, a π-system is defined as a set of subsets of `α` closed under binary intersection of non-disjoint sets, and a σ-algebra is the smallest measurable space containing a collection of basic sets. The condition that the measures coincide on the π-system is expressed as ∀ s ∈ C, μ s = ν s, and the condition that they give the same mass to the full set is expressed as μ Set.univ = ν Set.univ. The theorem then asserts that for any set `s` in the measurable space, if `s` is a measurable set, then μ s = ν s.
More concisely: If two finite measures μ and ν assign the same mass to the entire space and agree on all sets in a π-system, then they agree on all sets in the σ-algebra generated by that π-system.
|
MeasureTheory.Measure.FiniteSpanningSetsIn.ext
theorem MeasureTheory.Measure.FiniteSpanningSetsIn.ext :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {C : Set (Set α)},
m0 = MeasurableSpace.generateFrom C →
IsPiSystem C → μ.FiniteSpanningSetsIn C → (∀ s ∈ C, ↑↑μ s = ↑↑ν s) → μ = ν
This theorem states that for any type `α` and any measurable space `m0` over `α`, if we have two measures `μ` and `ν` over `α`, and a set `C` of subsets of `α`, under the conditions where `m0` is generated from `C`, `C` is a π-system, and `μ` spans `C` finitely, if for every subset `s` in `C` the measure `μ` of `s` is equal to the measure `ν` of `s`, then `μ` and `ν` are the same measure. In mathematical terms, this is a type of extensionality for measures, establishing that two measures are identical if they assign the same measure to all subsets in a finite spanning set that forms a π-system.
More concisely: If `m0` is a measure generator over `α`, `C` is a π-system of `α` that finitely spans `m0`, and for all `s` in `C`, `μ(s) = ν(s)`, then `μ = ν`.
|