measurableSet_Iic
theorem measurableSet_Iic :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : OpensMeasurableSpace α]
[inst_3 : Preorder α] [inst : OrderClosedTopology α] {a : α}, MeasurableSet (Set.Iic a)
The theorem `measurableSet_Iic` states that for any type `α` which is both a topological space and a measurable space, and admits an order-closed topology and a preorder relation, the left-infinite right-closed interval, denoted as `Set.Iic a`, is a measurable set. In other words, for any given value `a` of type `α`, the set of all elements of type `α` that are less than or equal to `a` is a measurable set in the specified measure space.
More concisely: For any topological space and measurable space α with an order-closed topology and preorder relation, the left-infinite right-closed interval Set.Iic a is a measurable set.
|
MeasureTheory.Measure.ext_of_Ico
theorem MeasureTheory.Measure.ext_of_Ico :
∀ {α : Type u_7} [inst : TopologicalSpace α] {_m : MeasurableSpace α} [inst_1 : SecondCountableTopology α]
[inst_2 : ConditionallyCompleteLinearOrder α] [inst_3 : OrderTopology α] [inst_4 : BorelSpace α]
[inst_5 : NoMaxOrder α] (μ ν : MeasureTheory.Measure α) [inst : MeasureTheory.IsLocallyFiniteMeasure μ],
(∀ ⦃a b : α⦄, a < b → ↑↑μ (Set.Ico a b) = ↑↑ν (Set.Ico a b)) → μ = ν
The theorem, named `MeasureTheory.Measure.ext_of_Ico`, states that for any topological space `α` with a measure space, a second-countable topology, a conditionally complete linear order, order topology, Borel space and no maximum order, given two measures `μ` and `ν` where `μ` is a locally finite measure, if for all pairs of `a` and `b` in `α` such that `a` is less than `b`, the measures `μ` and `ν` agree on all left-closed right-open intervals (denoted by `Set.Ico a b`), then `μ` and `ν` are equal.
More concisely: If `α` is a second-countable topological space with a measure space, a conditionally complete linear order, order topology, Borel space and no maximum order, and `μ` and `ν` are locally finite measures on `α` such that `μ(Set.Ico a b) = ν(Set.Ico a b)` for all `a < b` in `α`, then `μ = ν`.
|
borel_comap
theorem borel_comap :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {t : TopologicalSpace β}, borel α = MeasurableSpace.comap f (borel β)
The theorem `borel_comap` states that for any types `α` and `β`, any function `f` mapping from `α` to `β`, and any topological space on `β`, the Borel measurable space on `α` is equal to the preimage under `f` of the Borel measurable space on `β`. In other words, the set of all measurable subsets of `α` is exactly the set of all preimages under `f` of measurable subsets of `β` that are open in the given topology on `β`. This theorem bridges the gap between the concepts of measurability and topology, showing that the Borel measurable space is precisely the one obtained by considering the preimages of open sets via a function.
More concisely: The Borel measurable subsets of a type `α` are exactly the preimages under a function `f` from `α` to a topological space `β` of Borel measurable and open subsets of `β`.
|
Measurable.isGLB_of_mem
theorem Measurable.isGLB_of_mem :
∀ {α : Type u_1} {δ : Type u_5} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
[inst_3 : MeasurableSpace δ] [inst_4 : LinearOrder α] [inst_5 : OrderTopology α]
[inst : SecondCountableTopology α] {ι : Sort u_6} [inst : Countable ι] {f : ι → δ → α} {g g' : δ → α},
(∀ (i : ι), Measurable (f i)) →
∀ {s : Set δ},
MeasurableSet s →
(∀ b ∈ s, IsGLB {a | ∃ i, f i b = a} (g b)) → Set.EqOn g g' sᶜ → Measurable g' → Measurable g
This theorem states that if we have a function `g` that is the greatest lower bound of a countable set of measurable functions `f` on a measurable set `s`, and `g` coincides with another measurable function `g'` outside of `s`, then `g` is also measurable. Specifically, for every index `i`, `f i` is a measurable function from `δ` to `α`, where `α` is a topological space equipped with a Borel measure and a linear order topology, and `δ` is a measurable space. The set `s` is a subset of `δ`, and for every element `b` in `s`, the value `g b` is the greatest lower bound of the set of values `{a | ∃ i, f i b = a}`, i.e. the set of values that `f i` takes at `b` for some `i`. On the complement of `s`, `g` is equal to `g'`, which is measurable. The theorem concludes that under these conditions, `g` is measurable.
More concisely: If `g` is the greatest lower bound of a countable set of measurable functions `f` on a measurable set `s`, and `g` coincides with a measurable function `g'` outside of `s`, then `g` is measurable.
|
exists_spanning_measurableSet_le
theorem exists_spanning_measurableSet_le :
∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → NNReal},
Measurable f →
∀ (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite μ],
∃ s, (∀ (n : ℕ), MeasurableSet (s n) ∧ ↑↑μ (s n) < ⊤ ∧ ∀ x ∈ s n, f x ≤ ↑n) ∧ ⋃ i, s i = Set.univ
The theorem `exists_spanning_measurableSet_le` states that for any measurable space `α`, given a measurable function `f : α → ℝ≥0` (from `α` to nonnegative real numbers), and a σ-finite measure `μ` on `α`, there exist measurable sets `s` with finite measure, indexed by natural numbers `n`, such that each `f x` for `x` in `s n` is bounded by `n`. Furthermore, the union of these sets `s` covers the entire space `α`, i.e., it equals the universal set. This theorem implies that we can decompose our measurable space into a collection of measurable sets of finite measure, where the function `f` is bounded on each set. The theorem also underlies the fact that any measurable function into nonnegative real numbers can be approximated from below with simple functions.
More concisely: For any measurable space with a σ-finite measure, and a measurable function to nonnegative real numbers, there exist measurable sets of finite measure, indexed by natural numbers, whose union covers the space and bounds the function.
|
measurableSet_Ioo
theorem measurableSet_Ioo :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : OpensMeasurableSpace α]
[inst_3 : LinearOrder α] [inst : OrderClosedTopology α] {a b : α}, MeasurableSet (Set.Ioo a b)
The theorem `measurableSet_Ioo` states that for any given type `α` which has a topological space structure, a measurable space structure, an opens measurable space structure, a linear order structure, and an order closed topology structure, and for any two arbitrary elements `a` and `b` of type `α`, the open interval `(a, b)` (represented as `Set.Ioo a b` in Lean) is a measurable set. In other words, the set of all elements `x` in `α` such that `a < x < b` forms a measurable set in the given measure space on `α`.
More concisely: The open interval `(a, b)` in a measurable space equipped with a topological space, measurable space, order structure, and order-closed topology is a measurable set.
|
Continuous.borel_measurable
theorem Continuous.borel_measurable :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
Continuous f → Measurable f
The theorem `Continuous.borel_measurable` states that for any function `f` from a type `α` to a type `β`, if `α` and `β` are both topological spaces and the function `f` is continuous, then `f` is also measurable. This means that for any measurable set in the codomain (`β`), the preimage of this set under the function `f` is a measurable set in the domain (`α`).
More concisely: If `f: α → β` is a continuous function between topological spaces `α` and `β`, then `f` is measurable, i.e., for any measurable set `M ∈ β`, the preimage `f⁻¹(M) ∈ α` is also measurable.
|
measurableSet_Icc
theorem measurableSet_Icc :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : OpensMeasurableSpace α]
[inst_3 : Preorder α] [inst : OrderClosedTopology α] {a b : α}, MeasurableSet (Set.Icc a b)
This theorem states that for any type `α` that has a topological space structure, a measurable space structure, an open sets measurable space structure, a preorder structure, and an order closed topology structure, and for any two elements `a` and `b` of type `α`, the set of all elements between `a` and `b` (inclusive) is a measurable set in the ambient measure space on `α`. This includes both the case where `a` is less than or equal to `b`, and where `a` is greater than or equal to `b`.
More concisely: For any type `α` endowed with topological space, measurable space, open sets measurable space, preorder, and order closed topology structures, the set of elements between any two elements `a` and `b` (inclusive) is measurable in the ambient measure space on `α`.
|
Inseparable.mem_measurableSet_iff
theorem Inseparable.mem_measurableSet_iff :
∀ {γ : Type u_3} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [inst_2 : BorelSpace γ] {x y : γ},
Inseparable x y → ∀ {s : Set γ}, MeasurableSet s → (x ∈ s ↔ y ∈ s)
The theorem `Inseparable.mem_measurableSet_iff` states that for any topological space `γ` that is also a measurable space and a Borel space, if two points `x` and `y` in `γ` are topologically inseparable (meaning the neighborhoods around `x` and `y` are identical), then for any set `s` in `γ` that is a Borel measurable set, `x` is in `s` if and only if `y` is in `s`. This implies that you cannot separate topologically inseparable points by using a Borel measurable set; if one of the points is in the set, then so is the other.
More concisely: In a topological space that is also a measurable and Borel space, two topologically inseparable points have identical membership in any Borel measurable set.
|
IsCompact.measurableSet
theorem IsCompact.measurableSet :
∀ {α : Type u_1} {s : Set α} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α]
[inst_2 : OpensMeasurableSpace α] [inst_3 : T2Space α], IsCompact s → MeasurableSet s
The theorem `IsCompact.measurableSet` asserts that for any set `s` of type `α`, under the conditions that `α` has a topological space structure, a measurable space structure, an open measurable space structure, and is a T2 space (also known as a Hausdorff space), if `s` is a compact set, then `s` is a measurable set. In other words, it guarantees measurability of compact sets in a Hausdorff topological space where the open sets are measurable.
More concisely: In a Hausdorff topological space with a measurable structure where the open sets are measurable, a compact set is measurable.
|
MeasurableSet.induction_on_open
theorem MeasurableSet.induction_on_open :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
{C : Set α → Prop},
(∀ (U : Set α), IsOpen U → C U) →
(∀ (t : Set α), MeasurableSet t → C t → C tᶜ) →
(∀ (f : ℕ → Set α),
Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C (f i)) → C (⋃ i, f i)) →
∀ ⦃t : Set α⦄, MeasurableSet t → C t
This theorem is a principle of induction on open sets in a Borel space (a measurable space derived from a topological space). Given a property `C` of sets, if `C` holds for all open sets, the complement of all measurable sets `t` for which `C` holds, and for all countable unions of pairwise disjoint measurable sets, then `C` holds for all measurable sets.
In more detail: for a given topological space `α` equipped with a Borel measurable space structure, we suppose we have a property `C` of subsets of `α`. If the following conditions are met:
1. `C` holds for all open subsets of `α`,
2. for any measurable set `t` for which `C` holds, `C` also holds for the complement of `t`, and
3. if `f` is a sequence of measurable sets which are pairwise disjoint and for which `C` holds, then `C` also holds for the countable union of the sets in the sequence,
then the conclusion is that `C` holds for every measurable subset of `α`.
More concisely: If a property `C` holds for all open sets, their complements in measurable sets, and countable unions of pairwise disjoint measurable sets in a Borel space, then `C` holds for all measurable sets.
|
measurableSet_Ici
theorem measurableSet_Ici :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : OpensMeasurableSpace α]
[inst_3 : Preorder α] [inst : OrderClosedTopology α] {a : α}, MeasurableSet (Set.Ici a)
This theorem states that for any type `α` which has a topological space structure, a measurable space structure, an ordered set structure, where the topology is generated by open intervals and the order topology is closed, and for any element `a` of type `α`, the set of all elements `x` in `α` such that `x` is greater than or equal to `a` (represented by `Set.Ici a`) is a measurable set. In other words, it's saying that the left-closed right-infinite interval on a measurable space with an order-closed topology is measurable.
More concisely: Given a type `α` with a topology generated by open intervals, an order topology that is closed, and a measurable space structure, the set `{x : α | x ≥ a}` is measurable for any `a` in `α`.
|
tendsto_measure_cthickening_of_isClosed
theorem tendsto_measure_cthickening_of_isClosed :
∀ {α : Type u_1} [inst : PseudoEMetricSpace α] [inst_1 : MeasurableSpace α] [inst_2 : OpensMeasurableSpace α]
{μ : MeasureTheory.Measure α} {s : Set α},
(∃ R > 0, ↑↑μ (Metric.cthickening R s) ≠ ⊤) →
IsClosed s → Filter.Tendsto (fun r => ↑↑μ (Metric.cthickening r s)) (nhds 0) (nhds (↑↑μ s))
This theorem states that in a pseudo emetric space with a measurable space structure and an open set measurable space structure, for a given measure and a closed set, if there exists a positive number R such that the measure of the closed R-thickening of the set is finite, then the measure of the closed r-thickenings of the set converges to the measure of the set as r tends to 0. This convergence is stated in terms of the limit of a function, where the function is the measure of the closed r-thickening of the set, and the limit is taken with respect to the neighborhood filter at 0 and the neighborhood filter at the measure of the set.
More concisely: In a pseudo metric space with measurable and open set structures, if a closed set has finite measure for some positive radius R, then the measures of the closed R-thickening of the set converge to the set's measure as R approaches 0.
|
IsClosed.measurableSet
theorem IsClosed.measurableSet :
∀ {α : Type u_1} {s : Set α} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α]
[inst_2 : OpensMeasurableSpace α], IsClosed s → MeasurableSet s
The theorem `IsClosed.measurableSet` states that for any type `α` and any set `s` of this type, if `α` is equipped with both a topological space structure and a measurable space structure, and if the measurable space structure is generated by the topology's open sets (which is what `OpensMeasurableSpace α` means), then if `s` is a closed set in the topological space, it is also a measurable set in the measure space.
In simpler terms, it asserts that every closed set in a topological space that generates a measurable space is measurable.
More concisely: If a topological space equipped with a measurable space structure, where the measurable sets are generated by the open sets, then every closed set is measurable.
|
AEMeasurable.coe_nnreal_ennreal
theorem AEMeasurable.coe_nnreal_ennreal :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → NNReal} {μ : MeasureTheory.Measure α},
AEMeasurable f μ → AEMeasurable (fun x => ↑(f x)) μ
The theorem `AEMeasurable.coe_nnreal_ennreal` states that for any type `α` with a measurable space structure, any function `f` from `α` to the nonnegative real numbers (`NNReal`), and any measure `μ` on `α`, if `f` is almost everywhere measurable with respect to `μ`, then the function obtained by applying the coercion (or embedding) from `NNReal` to the extended nonnegative real numbers (`ennreal`, represented by `↑(f x)`) is also almost everywhere measurable with respect to `μ`. In other words, measuring the function after it has been coerced doesn't lose the almost everywhere measurability property.
More concisely: If `α` is a measurable space, `f : α → ℝ⁺` is almost everywhere measurable, and `μ` is a measure on `α`, then the function `x ↦ ↑(f x)` from `α` to the extended nonnegative reals (`ennreal`) is almost everywhere measurable.
|
ENNReal.measurable_of_measurable_nnreal
theorem ENNReal.measurable_of_measurable_nnreal :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : ENNReal → α}, (Measurable fun p => f ↑p) → Measurable f
This theorem states that for any measurable space `α` and any function `f` mapping from the extended nonnegative real numbers (`ENNReal`) to `α`, if the function `f` is measurable when applied to the embedding of nonnegative real numbers (denoted as `↑p`) into `ENNReal`, then `f` is measurable. Here, a function is called measurable if the preimage of every measurable set is also measurable. Essentially, this theorem allows us to conclude that a function is measurable in the extended nonnegative reals if it is measurable in the nonnegative reals.
More concisely: If a function from the extended nonnegative real numbers to a measurable space is measurable when mapped from the nonnegative real numbers embedding, then it is measurable.
|
borel_eq_generateFrom_Iic
theorem borel_eq_generateFrom_Iic :
∀ (α : Type u_1) [inst : TopologicalSpace α] [inst_1 : SecondCountableTopology α] [inst_2 : LinearOrder α]
[inst_3 : OrderTopology α], borel α = MeasurableSpace.generateFrom (Set.range Set.Iic)
This theorem states that for any type `α` equipped with a Topological Space structure, a Second Countable Topology structure, a Linear Order structure, and an Order Topology structure, the Borel measurable space generated by the topological space structure is equivalent to the smallest measurable space containing the collection of sets that are left-infinite right-closed intervals. In other words, the Borel σ-algebra, a sigma algebra generated by the open sets in a topological space, is the same as the smallest sigma algebra that contains all sets of the form `(-∞, b]` where `b` is a real number.
More concisely: The Borel sigma-algebra of a second countable topological space equipped with a linear order is equal to the sigma-algebra generated by left-infinite right-closed intervals.
|
measurable_iInf
theorem measurable_iInf :
∀ {α : Type u_1} {δ : Type u_5} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
[inst_3 : MeasurableSpace δ] [inst_4 : ConditionallyCompleteLinearOrder α] [inst_5 : OrderTopology α]
[inst : SecondCountableTopology α] {ι : Sort u_6} [inst : Countable ι] {f : ι → δ → α},
(∀ (i : ι), Measurable (f i)) → Measurable fun b => ⨅ i, f i b
The theorem `measurable_iInf` states that for any types `α` and `δ`, if `α` is a topological space, a measurable space, and a Borel space, and `δ` is a measurable space, and `α` also satisfies the properties of being a conditionally complete linear order and an order topology, and if it also has a second countable topology, then for any sort `ι` which is countable, for any function `f` from `ι` to a function from `δ` to `α`, if every such function `f i` is measurable, then the function that maps `b` in `δ` to the infimum of `f i b` over all `i` in `ι` is also measurable. This is a statement about the measurability of the infimum function in the context of measure theory.
More concisely: If `α` is a second countable, topological, measurable, and Borel space with a conditionally complete linear order and an order topology, then the infimum function of a countable family of measurable functions from `δ` to `α` is measurable.
|
Measurable.isLUB
theorem Measurable.isLUB :
∀ {α : Type u_1} {δ : Type u_5} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
[inst_3 : MeasurableSpace δ] [inst_4 : LinearOrder α] [inst_5 : OrderTopology α]
[inst : SecondCountableTopology α] {ι : Sort u_6} [inst : Countable ι] {f : ι → δ → α} {g : δ → α},
(∀ (i : ι), Measurable (f i)) → (∀ (b : δ), IsLUB {a | ∃ i, f i b = a} (g b)) → Measurable g
This theorem states that if a function `g` is the least upper bound of a countably many measurable functions `f i` (for all indices `i` in a countable index set), then `g` is itself measurable. Here, the spaces involved are measurable spaces and topological spaces, the functions `f i` are from `δ` to `α` and `g` is from `δ` to `α`. The measurability of the functions is defined in the context of a `MeasurableSpace`, and the notion of least upper bound is defined in the context of a `Preorder`.
More concisely: If `g` is the least upper bound of the countably many measurable functions `f i` from a measurable space `(δ, Σ)` to another measurable space `(α, β)`, then `g` is measurable.
|
ClosedEmbedding.measurableEmbedding
theorem ClosedEmbedding.measurableEmbedding :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
[inst_3 : TopologicalSpace β] [inst_4 : MeasurableSpace β] [inst_5 : BorelSpace β] {f : α → β},
ClosedEmbedding f → MeasurableEmbedding f
This theorem states that for every function `f` mapping from a type `α` to a type `β`, if `f` is a closed embedding (i.e., a homeomorphism onto its image that also maps closed sets to closed sets), then `f` is a measurable embedding. This holds under the assumptions that `α` and `β` are topological spaces with measurable spaces and their corresponding Borel sigma algebras. In other words, closed embeddings respect not only the topological structure but also the measurable structure of the spaces involved.
More concisely: A closed embedding between topological spaces `α` and `β` that are also measurable spaces preserves the measurable structure, that is, it is a measurable function.
|
MeasureTheory.Measure.ext_of_Ico_finite
theorem MeasureTheory.Measure.ext_of_Ico_finite :
∀ {α : Type u_7} [inst : TopologicalSpace α] {m : MeasurableSpace α} [inst_1 : SecondCountableTopology α]
[inst_2 : LinearOrder α] [inst_3 : OrderTopology α] [inst : BorelSpace α] (μ ν : MeasureTheory.Measure α)
[inst : MeasureTheory.IsFiniteMeasure μ],
↑↑μ Set.univ = ↑↑ν Set.univ → (∀ ⦃a b : α⦄, a < b → ↑↑μ (Set.Ico a b) = ↑↑ν (Set.Ico a b)) → μ = ν
This theorem in the Lean 4 programming language, `MeasureTheory.Measure.ext_of_Ico_finite`, states that if we have two finite measures, `μ` and `ν`, on a Borel space `α` (which is a topological space with a conditionally complete linear order and no top element, and also has a second countable topology and order topology), then these two measures are equal if they agree on the measure of the universal set and on all left-closed right-open intervals (denoted by `Set.Ico a b`, where `a` and `b` are elements of `α` and `a < b`). The theorem's proof is not provided in this context. In less technical terms, this theorem proves the equality of two measures if they both provide the same measurement for the whole space and for all intervals that include the start point but exclude the end point.
More concisely: Given two finite measures `μ` and `ν` on a second countable Borel space `α` with no top element, if `μ(α) = ν(α)` and `μ(Set.Ico a b) = ν(Set.Ico a b)` for all `a < b` in `α`, then `μ = ν`.
|
OpensMeasurableSpace.borel_le
theorem OpensMeasurableSpace.borel_le :
∀ {α : Type u_6} [inst : TopologicalSpace α] [h : MeasurableSpace α] [self : OpensMeasurableSpace α], borel α ≤ h
The theorem states that for any type `α`, given a topological space structure on `α`, a measurable space structure on `α`, and the fact that the open sets of `α` are measurable, the Borel measurable space on `α` (which is generated from the topology of `α`) is a subset of, or equal to, the given measurable space structure. In other words, all Borel-measurable sets in this context are indeed measurable.
More concisely: For any type `α` endowed with a topology and a measurable structure, if the open sets of `α` are measurable, then the Borel sigma-algebra generated by the topology is included in the given measurable structure.
|
Continuous.aemeasurable
theorem Continuous.aemeasurable :
∀ {α : Type u_1} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α]
[inst_2 : OpensMeasurableSpace α] [inst_3 : TopologicalSpace γ] [inst_4 : MeasurableSpace γ]
[inst_5 : BorelSpace γ] {f : α → γ}, Continuous f → ∀ {μ : MeasureTheory.Measure α}, AEMeasurable f μ
This theorem states that for any continuous function `f` from an open measurable space `α` to a Borel space `γ`, `f` is almost everywhere measurable with respect to any measure `μ` on `α`. In other words, we can find a measurable function that coincides with `f` almost everywhere in the domain. Here, an open measurable space is a measurable space that is generated by open sets, and a Borel space is a measure space that is generated by the topology.
More concisely: Given a continuous function `f` from an open measurable space `(α, ��ößα)` to a Borel space `(γ, ��ößγ)` with respect to any measure `μ` on `α`, there exists a measurable function `g` such that `μ({x : α | f x ≠ g x}) = 0`.
|
IsCompact.measure_closure
theorem IsCompact.measure_closure :
∀ {γ : Type u_3} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [inst_2 : BorelSpace γ]
[inst_3 : R1Space γ] {K : Set γ}, IsCompact K → ∀ (μ : MeasureTheory.Measure γ), ↑↑μ (closure K) = ↑↑μ K
The theorem `IsCompact.measure_closure` states that in a topological space (denoted as `γ`) which has an R₁ structure, and is equipped with a Borel measure `μ`, the measure of the closure of a compact set `K` is equal to the measure of `K` itself. In other words, if a set `K` is compact in this space, then taking the closure of `K` does not change its measure under `μ`. An additional statement in the theorem refers to another version `MeasureTheory.Measure.OuterRegular.measure_closure_eq_of_isCompact` that does not require the σ-algebra to be Borel, but instead assumes `μ` to be outer regular.
More concisely: In a topological space with an R₁ structure and a Borel measure, the measure of a compact set is equal to the measure of its closure. (Alternatively, for a measure that is outer regular, the measure of a compact set equals the measure of its closure without requiring a Borel σ-algebra.)
|
Measurable.isLUB_of_mem
theorem Measurable.isLUB_of_mem :
∀ {α : Type u_1} {δ : Type u_5} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
[inst_3 : MeasurableSpace δ] [inst_4 : LinearOrder α] [inst_5 : OrderTopology α]
[inst : SecondCountableTopology α] {ι : Sort u_6} [inst : Countable ι] {f : ι → δ → α} {g g' : δ → α},
(∀ (i : ι), Measurable (f i)) →
∀ {s : Set δ},
MeasurableSet s →
(∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)) → Set.EqOn g g' sᶜ → Measurable g' → Measurable g
This theorem states that given a function `g` which is the least upper bound of a countable collection of measurable functions `f[i]` (indexed by `i`), if it coincides with another measurable function `g'` outside of a measurable set `s`, then the function `g` is also measurable. Here, "coincides" means that for every element not in `s`, the value of `g` at that element is equal to the value of `g'` at that same element. The least upper bound property means that for every element `b` in `s`, `g(b)` is the least upper bound of the set of values `{a | ∃ i, f i b = a}`, i.e., the values produced by applying each function `f[i]` to `b`.
More concisely: If a measurable function `g` is the least upper bound of a countable collection of measurable functions `{f[i]}` and coincides with another measurable function `g'` outside of a measurable set `s`, then `g` is measurable.
|
MeasureTheory.Measure.ext_of_Ioc'
theorem MeasureTheory.Measure.ext_of_Ioc' :
∀ {α : Type u_7} [inst : TopologicalSpace α] {m : MeasurableSpace α} [inst_1 : SecondCountableTopology α]
[inst_2 : LinearOrder α] [inst_3 : OrderTopology α] [inst : BorelSpace α] [inst : NoMinOrder α]
(μ ν : MeasureTheory.Measure α),
(∀ ⦃a b : α⦄, a < b → ↑↑μ (Set.Ioc a b) ≠ ⊤) →
(∀ ⦃a b : α⦄, a < b → ↑↑μ (Set.Ioc a b) = ↑↑ν (Set.Ioc a b)) → μ = ν
The theorem `MeasureTheory.Measure.ext_of_Ioc'` states that for any measurable space (`α`) which is equipped with a topology, a second countable topology, a linear order, an order topology, a Borel space, and has no minimum order, given two measures (`μ` and `ν`) on this measurable space, if these two measures are finite on all close-open intervals, denoted by `Set.Ioc a b` (meaning `a < x ≤ b`), and if they agree on all such intervals (meaning the measure `μ` of any such interval equals the measure `ν`), then these two measures are indeed identical.
More concisely: If `α` is a second countable, measurable space with a linear order, topology, and no minimum order, equipped with Borel sigma-algebra, and `μ` and `ν` are finite measures agreeing on all close-open intervals, then `μ = ν`.
|
Mathlib.MeasureTheory.Constructions.BorelSpace.Basic._auxLemma.22
theorem Mathlib.MeasureTheory.Constructions.BorelSpace.Basic._auxLemma.22 :
∀ {α : Type u} (x : α), (x ∈ Set.univ) = True
This theorem states that for any type `α` and any element `x` of type `α`, the statement "x is in the universal set of α" is always true. In other words, every element of a given type is contained in the universal set of that type. Here, the universal set `Set.univ` of a type `α` is defined as the set containing all elements of `α`.
More concisely: For any type `α` and element `x` of type `α`, `x` is an element of the universal set `Set.univ` of type `α`.
|
measurable_of_tendsto_ennreal'
theorem measurable_of_tendsto_ennreal' :
∀ {α : Type u_1} [inst : MeasurableSpace α] {ι : Type u_6} {f : ι → α → ENNReal} {g : α → ENNReal} (u : Filter ι)
[inst_1 : u.NeBot] [inst_2 : u.IsCountablyGenerated],
(∀ (i : ι), Measurable (f i)) → Filter.Tendsto f u (nhds g) → Measurable g
This theorem, referred to as an alias of `ENNReal.measurable_of_tendsto'`, states that if we have a sequence of measurable functions `f : ι → α → [0,∞]` tending to a function `g : α → [0,∞]` as the filter `u` over `ι` tends to a neighborhood of `g`, then `g` itself is a measurable function. Here, measurability of a function is defined as the preimage of every measurable set being measurable, and the notion of tending to a limit is defined in terms of preimages of neighborhoods. The theorem requires that the filter `u` is not bottom (i.e., not the empty filter), and that it is countably generated.
More concisely: If `f : ι → α → [0,∞]` is a sequence of measurable functions tending to the measurable function `g : α → [0,∞]` as the countably generated filter `u` over `ι` approaches a neighborhood of `g`, then `g` is measurable.
|
tendsto_measure_cthickening
theorem tendsto_measure_cthickening :
∀ {α : Type u_1} [inst : PseudoEMetricSpace α] [inst_1 : MeasurableSpace α] [inst_2 : OpensMeasurableSpace α]
{μ : MeasureTheory.Measure α} {s : Set α},
(∃ R > 0, ↑↑μ (Metric.cthickening R s) ≠ ⊤) →
Filter.Tendsto (fun r => ↑↑μ (Metric.cthickening r s)) (nhds 0) (nhds (↑↑μ (closure s)))
The theorem `tendsto_measure_cthickening` states that for any pseudo-emetric space `α` which is also a measurable and opens measurable space, and any measure `μ` and set `s` in `α`, if there exists a positive real number `R` such that the `R`-closed thickening of `s` has a finite measure, then the measure of the `r`-closed thickening of `s` converges to the measure of the closure of `s` as `r` approaches `0`. In other words, as we progressively construct smaller and smaller closed thickenings of `s`, their measures get closer and closer to the measure of the closure of `s`. This theorem links the concepts of metric thickening, measure, and topological closure in the context of pseudo-emetric spaces.
More concisely: Given a measurable and opens measurable pseudo-metric space `(α, d)` with measure `μ`, any set `s ∈ α`, and a positive real `R` such that the `R`-closed thickening of `s` has finite measure, the measure of the `r`-closed thickening of `s` converges to the measure of `s.closure` as `r` approaches `0`.
|
Measurable.ennreal_tsum
theorem Measurable.ennreal_tsum :
∀ {α : Type u_1} [inst : MeasurableSpace α] {ι : Type u_6} [inst_1 : Countable ι] {f : ι → α → ENNReal},
(∀ (i : ι), Measurable (f i)) → Measurable fun x => ∑' (i : ι), f i x
The theorem `Measurable.ennreal_tsum` states that in a measurable space `α` and for any countable type `ι`, if you have a sequence of measurable functions `f : ι → α → ENNReal` (functions from `ι` to a function from `α` to extended nonnegative real numbers), then the function which maps each element `x` of `α` to the sum over `ι` of `f i x` is also measurable. In simpler terms, it is saying that the sum of a sequence of measurable functions is itself measurable. Note that `ENNReal` denotes the extended nonnegative real numbers, usually denoted as `[0, ∞]`, which might be generalized in future versions of this lemma.
More concisely: If `α` is a measurable space and `f : ι → α → ENNReal` is a sequence of measurable functions, then the function mapping each `x` in `α` to the sum over `ι` of `f i x` is measurable.
|
measurableSet_Ico
theorem measurableSet_Ico :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : OpensMeasurableSpace α]
[inst_3 : LinearOrder α] [inst : OrderClosedTopology α] {a b : α}, MeasurableSet (Set.Ico a b)
The theorem `measurableSet_Ico` states that for all types `α` having a topological space, a measurable space, an open measurable space, a linear order, and a closed order topology, and for any two elements `a` and `b` of type `α`, the left-closed right-open interval from `a` to `b` (`Set.Ico a b`) is a measurable set (in the ambient measure space on `α`). This means that for any interval where `a` is less than or equal to some `x` and `x` is less than `b`, that interval is measurable in the given measure space.
More concisely: For any type `α` with a topological space, measurable space, open measurable space, linear order, and closed order topology, the interval `Ico a b` is a measurable set in the measure space on `α` for all `a ≤ x < b` in `α`.
|
measurableSet_le
theorem measurableSet_le :
∀ {α : Type u_1} {δ : Type u_5} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α]
[inst_2 : OpensMeasurableSpace α] [inst_3 : MeasurableSpace δ] [inst_4 : PartialOrder α]
[inst_5 : OrderClosedTopology α] [inst : SecondCountableTopology α] {f g : δ → α},
Measurable f → Measurable g → MeasurableSet {a | f a ≤ g a}
The theorem `measurableSet_le` states that for any two functions `f` and `g` from a measurable space `δ` to a topological space `α` that is also a measurable space, if `f` and `g` are both measurable functions and `α` has a partial order and a second countable topology that is closed under the order, then the set of all elements `a` from the domain for which the value of `f` at `a` is less than or equal to the value of `g` at `a` is a measurable set.
More concisely: A function from a measurable space to a second countable, order-closed topological space that preserves the order and is measurable, maps measurable sets to measurable sets. (The theorem `measurableSet_le` states that the set of elements where the function value of one function is less than or equal to that of another is such a measurable set.)
|
tendsto_measure_cthickening_of_isCompact
theorem tendsto_measure_cthickening_of_isCompact :
∀ {α : Type u_1} [inst : MetricSpace α] [inst_1 : MeasurableSpace α] [inst_2 : OpensMeasurableSpace α]
[inst_3 : ProperSpace α] {μ : MeasureTheory.Measure α} [inst_4 : MeasureTheory.IsFiniteMeasureOnCompacts μ]
{s : Set α}, IsCompact s → Filter.Tendsto (fun r => ↑↑μ (Metric.cthickening r s)) (nhds 0) (nhds (↑↑μ s))
This theorem states that for any compact set in a proper metric space, the measure of the set's closed thickenings, which are sets of points at a distance of at most `r` from the original set, tends towards the measure of the original set as `r` tends towards `0`. This is under the assumption that the measure is finite on compact sets. In other words, as we 'thicken' a compact set by an infinitesimally small radius, the measure of the 'thickened' set converges to the measure of the original set.
More concisely: For any compact set in a proper metric space with finite measure, the measure of its closed thickenings converges to the measure of the original set as the thickness approaches zero.
|
tendsto_measure_thickening
theorem tendsto_measure_thickening :
∀ {α : Type u_1} [inst : PseudoEMetricSpace α] [inst_1 : MeasurableSpace α] [inst_2 : OpensMeasurableSpace α]
{μ : MeasureTheory.Measure α} {s : Set α},
(∃ R > 0, ↑↑μ (Metric.thickening R s) ≠ ⊤) →
Filter.Tendsto (fun r => ↑↑μ (Metric.thickening r s)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (↑↑μ (closure s)))
This theorem states that in a pseudo emetric space, if a set has a certain thickening whose measure is finite, then as `r` tends to 0 through positive numbers, the measures of the `r`-thickenings of the set converge to the measure of the closure of the set. Here, a thickening of a set is defined as the collection of points that are less than a certain distance `r` from the set, and the measure of a set represents its "size" or "volume" in the space. Hence, the theorem essentially tells us how the "volume" of the thickening of a set changes as the thickening becomes smaller and smaller, converging to the "volume" of the smallest closed set that contains the original set.
More concisely: In a pseudo-metric space, the measures of the closures and the lim inf of the sequence of sets defined as the union of a set and all points within a decreasing sequence of positive radii from the set, converge.
|
Measurable.ennreal_ofReal
theorem Measurable.ennreal_ofReal :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℝ}, Measurable f → Measurable fun x => ENNReal.ofReal (f x)
The theorem `Measurable.ennreal_ofReal` states that for any type `α` that has a `MeasurableSpace` instance and any function `f` from `α` to the real numbers `ℝ`, if `f` is a measurable function, then the function that applies `ENNReal.ofReal` to the output of `f` (that is, the function `x => ENNReal.ofReal (f x)`) is also measurable. In other words, the operation of converting the output of a measurable function to its equivalent in extended non-negative real numbers (`ENNReal.ofReal`) preserves measurability.
More concisely: If `α` is a measurable space and `f : α → ℝ` is a measurable function, then the function `x => ENNReal.ofReal (f x)` is measurable.
|
MeasureTheory.Measure.ext_of_Iic
theorem MeasureTheory.Measure.ext_of_Iic :
∀ {α : Type u_7} [inst : TopologicalSpace α] {m : MeasurableSpace α} [inst_1 : SecondCountableTopology α]
[inst_2 : LinearOrder α] [inst_3 : OrderTopology α] [inst : BorelSpace α] (μ ν : MeasureTheory.Measure α)
[inst : MeasureTheory.IsFiniteMeasure μ], (∀ (a : α), ↑↑μ (Set.Iic a) = ↑↑ν (Set.Iic a)) → μ = ν
The theorem `MeasureTheory.Measure.ext_of_Iic` states that for every type `α` which is a topological space with a measurable space structure, that also has a second countable topology, a linear order, and an order topology, and is also a Borel space, every pair of finite measures `μ` and `ν` are equal if for every left-infinite right-closed interval `Set.Iic a` for any `a` from `α`, the measure `μ` of the interval is equal to the measure `ν` of the interval.
More concisely: If `α` is a second countable, Borel, topological space with a measurable structure and a linear order, endowed with the order topology, then for every finite measures `μ` and `ν` on `α`, if `μ(Set.Iic a) = ν(Set.Iic a)` for all left-infinite right-closed intervals `Set.Iic a`, then `μ = ν`.
|
borel_eq_generateFrom_Ioi
theorem borel_eq_generateFrom_Ioi :
∀ (α : Type u_1) [inst : TopologicalSpace α] [inst_1 : SecondCountableTopology α] [inst_2 : LinearOrder α]
[inst_3 : OrderTopology α], borel α = MeasurableSpace.generateFrom (Set.range Set.Ioi)
This theorem states that for any type `α` which has a topological space structure, a second countable topology structure, a linear order structure, and an order topology structure, the Borel `MeasurableSpace` on `α` is equal to the `MeasurableSpace` generated from the range of the function `Set.Ioi`. In other words, the smallest sigma algebra (measurable space) that contains all the open sets (generated by the topological space structure on `α`) is the same as the smallest sigma algebra that contains all the sets of the form "(a, +∞)", where `a` is any element of `α`. This is a fundamental result linking the concepts of measure theory and topology.
More concisely: The Borel measurable space on a type `α` with a topological space, second countable topology, linear order, and order topology structures is equal to the sigma algebra generated by the ranges of `Set.Ioi` for any element `a` in `α`.
|
measurable_coe_nnreal_ennreal
theorem measurable_coe_nnreal_ennreal : Measurable ENNReal.ofNNReal
The theorem `measurable_coe_nnreal_ennreal` states that the function `ENNReal.ofNNReal`, which coerces a non-negative real number (`ℝ≥0` or `NNReal` in Lean) to an extended non-negative real number (`ℝ≥0∞` or `ENNReal` in Lean), is a measurable function. In other words, for every measurable set in the space of extended non-negative real numbers, the preimage of the set under the function `ENNReal.ofNNReal` is also a measurable set in the space of non-negative real numbers.
More concisely: The coerction function `ENNReal.ofNNReal` from non-negative reals to extended non-negative reals is measurable.
|
Measurable.ennreal_toReal
theorem Measurable.ennreal_toReal :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ENNReal}, Measurable f → Measurable fun x => (f x).toReal := by
sorry
This theorem states that for any given measurable space `α` and a function `f` from `α` to the extended nonnegative real numbers (usually denoted [0, ∞]), if `f` is a measurable function, then the function which maps each element of `α` to the real part of its image under `f` is also measurable. In other words, the operation of taking the real part preserves measurability in this context.
More concisely: If `f` is a measurable function from a measurable space `α` to the extended nonnegative real numbers, then the function mapping each element of `α` to the real part of its image under `f` is also measurable.
|
Measurable.ennreal_toNNReal
theorem Measurable.ennreal_toNNReal :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ENNReal}, Measurable f → Measurable fun x => (f x).toNNReal
The theorem `Measurable.ennreal_toNNReal` states that for any type `α` with a measurable space structure and any function `f` from `α` to the extended nonnegative real numbers (`ENNReal`), if `f` is a measurable function, then the function that sends each element `x` in `α` to the nonnegative real part (`toNNReal`) of `f(x)` is also a measurable function. This means that the preimage of every measurable set under this new function is also measurable.
More concisely: If `α` is a measurable space and `f : α → ENNReal` is a measurable function, then the function `x ↦ toNNReal (f x)` is also measurable.
|
measurable_of_Ioi
theorem measurable_of_Ioi :
∀ {α : Type u_1} {δ : Type u_5} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
[inst_3 : MeasurableSpace δ] [inst_4 : LinearOrder α] [inst_5 : OrderTopology α]
[inst : SecondCountableTopology α] {f : δ → α}, (∀ (x : α), MeasurableSet (f ⁻¹' Set.Ioi x)) → Measurable f
The theorem `measurable_of_Ioi` states that for any type `α` with a topological space, measurable space, Borel space, linear order, order topology, and second countable topology, and any type `δ` with a measurable space, if we have a function `f` from `δ` to `α` such that the preimage of every left-open right-infinite interval `(x, ∞)` under `f` is a measurable set, then `f` itself is measurable. In other words, `f` is measurable if and only if the preimage of every interval of the form `(x, ∞)` is measurable.
More concisely: If `δ` is a measurable space and `f: δ → α` is a function with `α` being a second countable topological space, measurable space, Borel space, linearly ordered set, and having the order topology, then `f` is measurable if and only if for all `x ∈ δ`, the preimage `f⁻ⁱ((x, ∞))` is a measurable set.
|
IsOpen.measurableSet
theorem IsOpen.measurableSet :
∀ {α : Type u_1} {s : Set α} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α]
[inst_2 : OpensMeasurableSpace α], IsOpen s → MeasurableSet s
This theorem states that for any set `s` of a certain type `α`, given that `α` is equipped with a topological space structure, a measurable space structure, and the condition that every open set in the topological space is measurable (`OpensMeasurableSpace α`), if `s` is an open set in the topological space, then `s` is also a measurable set in the measurable space. In other words, open sets in the topological space are also measurable sets in the measurable space when the space has the property that all open sets are measurable.
More concisely: If `α` is a topological space where every open set is measurable, then every open set in `α` is a measurable set.
|
measurableSet_Ioc
theorem measurableSet_Ioc :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : OpensMeasurableSpace α]
[inst_3 : LinearOrder α] [inst : OrderClosedTopology α] {a b : α}, MeasurableSet (Set.Ioc a b)
The theorem `measurableSet_Ioc` states that for any given type `α` equipped with a topology, a measure space, a linear order, and an order closed topology, for any two elements `a` and `b` of type `α`, the left-open right-closed interval `Set.Ioc a b` is a measurable set. In other words, the set of all elements `x` of type `α` which are strictly greater than `a` and less than or equal to `b` is measurable in the measure space on `α`.
More concisely: For any type `α` with a measure space, topology, linear order, and order-closed topology, the left-open right-closed interval `Set.Ioc a b` is a measurable subset of `α` for all `a < b` in `α`.
|
borel_eq_top_of_discrete
theorem borel_eq_top_of_discrete :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : DiscreteTopology α], borel α = ⊤
This theorem states that for any type `α` equipped with a topological space structure and a discrete topology, the borel measurable space generated from the topological space is equal to the maximal (or top) measurable space, denoted by '⊤'. In other words, when the topology on `α` is discrete, every subset of `α` is both open and measurable, thus the borel measurable space is as large as it could possibly be.
More concisely: For any topological space `α` with a discrete topology, its Borel sigma-algebra equals the maximal measurable space.
|
MeasurableSet.nhdsWithin_isMeasurablyGenerated
theorem MeasurableSet.nhdsWithin_isMeasurablyGenerated :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : OpensMeasurableSpace α]
{s : Set α}, MeasurableSet s → ∀ (a : α), (nhdsWithin a s).IsMeasurablyGenerated
This theorem states that if `s` is a measurable set in a topological and measurable space, which is also an opens measurable space, then for every element `a` in the space, the "neighborhood within" filter (`𝓝[s] a`) is measurably generated. The "neighborhood within" filter here refers to sets that contain the intersection of `s` and a neighborhood of `a`. Note that the measurability of `s` is not an instance and hence needs to be provided explicitly. This theorem essentially ties together the concepts of topological (neighborhood) and measure (measurably generated) properties of sets.
More concisely: In a topological and measurable space, if `s` is a measurable and open set, then the "neighborhood within" filter of any element `a` in `s`, `𝓝[s] a`, is measurably generated.
|
measurable_limsup
theorem measurable_limsup :
∀ {α : Type u_1} {δ : Type u_5} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
[inst_3 : MeasurableSpace δ] [inst_4 : ConditionallyCompleteLinearOrder α] [inst_5 : OrderTopology α]
[inst : SecondCountableTopology α] {f : ℕ → δ → α},
(∀ (i : ℕ), Measurable (f i)) → Measurable fun x => Filter.limsup (fun i => f i x) Filter.atTop
The theorem `measurable_limsup` states that the limit superior (limsup) over the natural numbers is measurable. Specifically, given a topological space `α`, a measurable space `α` which is also a Borel space, a measurable space `δ`, a conditionally complete linear order structure on `α` with an order topology, and a second countable topology on `α`, the theorem asserts that if we have a function `f` mapping natural numbers and elements of `δ` to `α` such that the function `f` is measurable for every natural number, then the function that maps `x` in `δ` to the limsup of the sequence `(f i x)` as `i` goes to infinity is also measurable. In other words, taking the limsup of a sequence of functions indexed by the natural numbers preserves measurability.
More concisely: Given a measurable space `α` (Borel), a second countable topology on `α`, a measurable function `f : ℕ × δ -> α`, and a linear order structure on `α` with an order topology, the function sending `x` in `δ` to the limsup of `(f i x)` as `i` goes to infinity is measurable.
|
measurable_coe_nnreal_real
theorem measurable_coe_nnreal_real : Measurable NNReal.toReal
The theorem `measurable_coe_nnreal_real` states that the function that coerces non-negative real numbers (`ℝ≥0`, denoted `NNReal` in Lean 4) into real numbers (`ℝ`) is a measurable function. In more detail, if we take any measurable set in the space of real numbers, the preimage of this set under the function `NNReal.toReal` is a measurable set in the space of non-negative real numbers.
More concisely: The function `NNReal.toReal` that maps non-negative real numbers to real numbers is measurable, meaning the preimage of any measurable real set is a measurable non-negative real set.
|
BorelSpace.measurable_eq
theorem BorelSpace.measurable_eq :
∀ {α : Type u_6} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [self : BorelSpace α], inst_1 = borel α
This theorem states that, for any type `α` equipped with a `TopologicalSpace` structure and a `MeasurableSpace` structure, if `α` is also a `BorelSpace`, then the `MeasurableSpace` structure on `α` is exactly the `borel` measurable space generated from that topology. In other words, all the measurable sets are exactly the Borel-measurable sets. The Borel-measurable sets are generated by the open sets of the topological space, providing a bridge between the concepts of topological and measurable spaces.
More concisely: For any topological space `α` that is also a Borel space, its MeasurableSpace structure equals the Borel measurable space generated from its TopologicalSpace structure.
|
measurable_of_tendsto_nnreal'
theorem measurable_of_tendsto_nnreal' :
∀ {α : Type u_1} [inst : MeasurableSpace α] {ι : Type u_6} {f : ι → α → NNReal} {g : α → NNReal} (u : Filter ι)
[inst_1 : u.NeBot] [inst_2 : u.IsCountablyGenerated],
(∀ (i : ι), Measurable (f i)) → Filter.Tendsto f u (nhds g) → Measurable g
This theorem, also known as an alias of `NNReal.measurable_of_tendsto'`, states that if we have a sequence of measurable functions from any type `α` to the nonnegative real numbers `ℝ≥0`, indexed by another type `ι`, and these functions converge to a function `g` under a certain filter `u` on `ι`, then the limit function `g` is also measurable. The convergence is defined in the sense that for any neighborhood of `g`, the preimage under the function `f` is a neighborhood under the filter `u`. This theorem assumes that the filter `u` is not trivial, i.e., does not only contain an empty set, and it is countably generated, which means there exists a countable set such that every set in the filter contains an element of this countable set.
More concisely: If `{f_i : α -> ℝ≥0 | i ∈ ι}` is a sequence of measurable functions from `α` to the nonnegative real numbers, indexed by a countably generated, non-trivial filter `u` on `ι`, and `f_i` converges to `g` under `u`, then `g` is measurable.
|
MeasureTheory.Measure.ext_of_Ico'
theorem MeasureTheory.Measure.ext_of_Ico' :
∀ {α : Type u_7} [inst : TopologicalSpace α] {m : MeasurableSpace α} [inst_1 : SecondCountableTopology α]
[inst_2 : LinearOrder α] [inst_3 : OrderTopology α] [inst : BorelSpace α] [inst : NoMaxOrder α]
(μ ν : MeasureTheory.Measure α),
(∀ ⦃a b : α⦄, a < b → ↑↑μ (Set.Ico a b) ≠ ⊤) →
(∀ ⦃a b : α⦄, a < b → ↑↑μ (Set.Ico a b) = ↑↑ν (Set.Ico a b)) → μ = ν
The theorem `MeasureTheory.Measure.ext_of_Ico'` states that for any topological space `α`, given two measures `μ` and `ν` on this space, if both measures return finite values for all left-closed and right-open intervals (where the ordering is given by a linear order compatible with the topology), and if these measures agree on the measure of all such intervals (i.e., for any two elements `a` and `b` in the space `α` such that `a < b`, the measure of the interval from `a` to `b` under `μ` equals the measure of the same interval under `ν`), then the two measures `μ` and `ν` are equal.
More concisely: If two measures on a topological space have finite values for all left-closed and right-open intervals and agree on the measure of each such interval, then they are equal.
|
measurable_of_tendsto_nnreal
theorem measurable_of_tendsto_nnreal :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : ℕ → α → NNReal} {g : α → NNReal},
(∀ (i : ℕ), Measurable (f i)) → Filter.Tendsto f Filter.atTop (nhds g) → Measurable g
The theorem `measurable_of_tendsto_nnreal` asserts that for a measurable space `α` and a sequence of functions `f : ℕ → α → NNReal` (where `NNReal` represents nonnegative real numbers), if each function in the sequence `f` is measurable and it converges to a function `g : α → NNReal` in the limit (`→ ∞`), then the limit function `g` is also measurable. Here, the convergence is expressed in terms of filter theory, specifically saying that the function `f` tends to `g` under the filter `Filter.atTop` (which represents the limit `→ ∞`), and the neighborhood filter `nhds g` (which represents an open set around `g`).
More concisely: If `α` is a measurable space, `f : ℕ → α → NNReal` is a sequence of measurable functions, and `f` converges to the measurable function `g : α → NNReal` in the limit under the filters `Filter.atTop` and `nhds g`, then `g` is measurable.
|
measurable_of_isOpen
theorem measurable_of_isOpen :
∀ {γ : Type u_3} {δ : Type u_5} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [inst_2 : BorelSpace γ]
[inst_3 : MeasurableSpace δ] {f : δ → γ}, (∀ (s : Set γ), IsOpen s → MeasurableSet (f ⁻¹' s)) → Measurable f
The theorem `measurable_of_isOpen` states that for any types `γ` and `δ`, where `γ` is equipped with a topological space structure, a measurable space structure, and a Borel space structure, and `δ` is equipped with a measurable space structure, for any function `f` from `δ` to `γ`, if the preimage of every open set under `f` is measurable, then `f` itself is a measurable function. In mathematical terms, this means that if for all open sets `s` in `γ`, `f`−1(`s`) is a measurable set in `δ`, then `f` is measurable with respect to the given measurable spaces on `δ` and `γ`.
More concisely: If the preimage of every open set under a function from a measurable space with a Borel space structure to a topological space with a measurable space structure is measurable, then the function is measurable.
|
Measurable.isGLB
theorem Measurable.isGLB :
∀ {α : Type u_1} {δ : Type u_5} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
[inst_3 : MeasurableSpace δ] [inst_4 : LinearOrder α] [inst_5 : OrderTopology α]
[inst : SecondCountableTopology α] {ι : Sort u_6} [inst : Countable ι] {f : ι → δ → α} {g : δ → α},
(∀ (i : ι), Measurable (f i)) → (∀ (b : δ), IsGLB {a | ∃ i, f i b = a} (g b)) → Measurable g
This theorem states that for any topological space `α`, a measurable space `α` that is also a Borel space, a measurable space `δ`, a linear order on `α`, an order topology on `α`, a second countable topology on `α`, and a countable index set `ι`, if every function from `ι` to the function space from `δ` to `α` is measurable, and for every element `b` of `δ`, `g b` is the greatest lower bound of the set of all `a` such that there exists an `i` in `ι` where `f i b` equals `a`, then the function `g` from `δ` to `α` is measurable.
In simpler terms, it says that if we have a family of measurable functions indexed by a countable set, and another function `g` is the greatest lower bound of this family at each point, then `g` itself is measurable.
More concisely: If `α` is a second countable Borel space with a linear order and order topology, every countable family of measurable functions from a measurable space `δ` to `α` having the property that each element of `δ` is the greatest lower bound of the set of values of the family at some index, then the function that maps each element of `δ` to its greatest lower value is measurable.
|
Continuous.measurable
theorem Continuous.measurable :
∀ {α : Type u_1} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α]
[inst_2 : OpensMeasurableSpace α] [inst_3 : TopologicalSpace γ] [inst_4 : MeasurableSpace γ]
[inst_5 : BorelSpace γ] {f : α → γ}, Continuous f → Measurable f
The theorem states that for any continuous function `f` from a space `α` with both a topological structure and an opens-measurable structure to a space `γ` with both a topological structure and a Borel measurable structure, the function `f` is measurable. In more mathematical terms, if `α` is a topological space that is also an opens-measurable space, and `γ` is a topological space that is also a Borel space, then any continuous function `f: α → γ` is a measurable function. Measurability here is defined as the property of a function where the preimage of every measurable set is also measurable.
More concisely: A continuous function between a topological space that is also an opens-measurable space and a Borel space is measurable.
|
measure_eq_measure_preimage_add_measure_tsum_Ico_zpow
theorem measure_eq_measure_preimage_add_measure_tsum_Ico_zpow :
∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f : α → ENNReal},
Measurable f →
∀ {s : Set α},
MeasurableSet s →
∀ {t : NNReal},
1 < t →
↑↑μ s =
↑↑μ (s ∩ f ⁻¹' {0}) + ↑↑μ (s ∩ f ⁻¹' {⊤}) +
∑' (n : ℤ), ↑↑μ (s ∩ f ⁻¹' Set.Ico (↑t ^ n) (↑t ^ (n + 1)))
The theorem `measure_eq_measure_preimage_add_measure_tsum_Ico_zpow` states that for any measurable set `s` in a measurable space `α`, and a measurable function `f` from `α` to the extended nonnegative real numbers `[0, ∞]`, and for any nonnegative real number `t` that is greater than 1, the measure of the set `s` with respect to any measure `μ` is equal to the sum of the measure of the set where `f` is zero, the measure of the set where `f` is `∞`, and the infinite sum over all integers `n` of the measure of the set where `f` lies in the interval `[t^n, t^(n+1))`. This theorem provides a method to compute the measure of a set based on subsets where the function `f` does not have more than `t` fluctuation.
More concisely: For any measurable set `s` and measurable function `f` from a measurable space `α` to the extended nonnegative real numbers, the measure of `s` is equal to the sum of measures of `f` being zero, infinite, and the infinite sum over integers `n` of measures of `f` in `[t^n, t^(n+1))`.
|
measurableSet_lt'
theorem measurableSet_lt' :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : OpensMeasurableSpace α]
[inst_3 : LinearOrder α] [inst_4 : OrderClosedTopology α] [inst : SecondCountableTopology α],
MeasurableSet {p | p.1 < p.2}
The theorem `measurableSet_lt'` states that for any type `α` with an instantiated `TopologicalSpace`, `MeasurableSpace`, `OpensMeasurableSpace`, `LinearOrder`, `OrderClosedTopology`, and `SecondCountableTopology`, the set of all pairs `(p.1, p.2)` such that `p.1 < p.2` forms a measurable set. In other words, in a space satisfying these structures, we can measure the set of ordered pairs where the first element is less than the second.
More concisely: In a topological space equipped with a measurable structure, a linear order, an order topology, and a second countable topology, the set of ordered pairs with the first element strictly less than the second is a measurable set.
|
measurableSet_of_mem_nhdsWithin_Ioi
theorem measurableSet_of_mem_nhdsWithin_Ioi :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
[inst_3 : LinearOrder α] [inst_4 : OrderTopology α] [inst_5 : SecondCountableTopology α] {s : Set α},
(∀ x ∈ s, s ∈ nhdsWithin x (Set.Ioi x)) → MeasurableSet s
The theorem `measurableSet_of_mem_nhdsWithin_Ioi` states that if a set `s` in a given topological space `α` with additional structures (a measurable space, a Borel space, a linear order, an order topology, and a second countable topology) has the property that for every point `x` in `s`, `s` is in the filter of neighborhoods within the open interval `(x, ∞)` of `x`, then `s` is a measurable set. In simpler terms, if a set is a right-neighborhood of all of its points, then it is measurable.
More concisely: If a subset of a second countable, order topological space with a measurable and Borel structure is contained in the filter of neighborhoods of each of its points in the open right half-line, then it is measurable.
|
ENNReal.measurable_ofReal
theorem ENNReal.measurable_ofReal : Measurable ENNReal.ofReal
This theorem states that the function `ENNReal.ofReal`, which maps any real number to its nonnegative equivalent, or 0 if it is negative, is a measurable function. In mathematical terms, for any measurable set in the extended nonnegative real numbers, the preimage of that set under `ENNReal.ofReal` is also a measurable set in the real numbers.
More concisely: The function `ENNReal.ofReal` mapping real numbers to their nonnegative equivalents is measurable, i.e., the preimage of any measurable set in the extended nonnegative real numbers is a measurable set in the real numbers.
|
measurable_nnnorm
theorem measurable_nnnorm :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup α] [inst_2 : OpensMeasurableSpace α],
Measurable nnnorm
The theorem `measurable_nnnorm` states that for any type `α` which has a `MeasurableSpace` structure and is also a normed additive commutative group with an open measurable space structure, the non-negative real-valued norm (`nnnorm`) function is measurable. In other words, given a measurable set in the set of non-negative real numbers, the preimage under the `nnnorm` function is a measurable set in the given measurable space `α`.
More concisely: For any normed additive commutative group `α` with an open measurable space structure that is also a type with a `MeasurableSpace` structure, the non-negative real-valued norm function is measurable.
|
AEMeasurable.ennreal_toReal
theorem AEMeasurable.ennreal_toReal :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ENNReal} {μ : MeasureTheory.Measure α},
AEMeasurable f μ → AEMeasurable (fun x => (f x).toReal) μ
This theorem asserts that for any measurable space `α`, and any function `f` from `α` to the extended nonnegative real numbers (`ENNReal`), if `f` is almost everywhere measurable with respect to a measure `μ`, then the function obtained by applying the `toReal` operation to the output of `f` is also almost everywhere measurable with respect to the same measure `μ`. In simpler terms, the real part of an almost everywhere measurable function is itself almost everywhere measurable.
More concisely: The real part of an almost everywhere measurable function from a measurable space to the extended nonnegative real numbers is almost everywhere measurable with respect to the same measure.
|
Measurable.coe_nnreal_real
theorem Measurable.coe_nnreal_real :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → NNReal}, Measurable f → Measurable fun x => ↑(f x)
The theorem `Measurable.coe_nnreal_real` states that for any measurable space `α` and any measurable function `f` from `α` to the nonnegative real numbers (`NNReal`), the function that maps each element of `α` to its image under `f` and then applies the coercion from `NNReal` to the real numbers is also measurable. In other words, if you have a measurable function mapping into the nonnegative reals, taking the real part of the output of that function (via the coercion `↑`) will still give you a measurable function.
More concisely: If `f : α → NNReal` is measurable, then the function `x ↦ ↑(f x) : α → ℝ` is measurable.
|
measurable_liminf
theorem measurable_liminf :
∀ {α : Type u_1} {δ : Type u_5} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
[inst_3 : MeasurableSpace δ] [inst_4 : ConditionallyCompleteLinearOrder α] [inst_5 : OrderTopology α]
[inst : SecondCountableTopology α] {f : ℕ → δ → α},
(∀ (i : ℕ), Measurable (f i)) → Measurable fun x => Filter.liminf (fun i => f i x) Filter.atTop
The theorem `measurable_liminf` states that the limit inferior (liminf) over natural numbers of a function is measurable. More specifically, for any two types `α` and `δ` where `α` is a topological space, a measurable space, a Borel space, a conditionally complete linear order, an ordered topology, and has a second countable topology, and `δ` is a measurable space, if we have a function `f` from natural numbers to a function from `δ` to `α` such that for each natural number `i`, `f i` is measurable, then the function that maps each element `x` in `δ` to the liminf (as `i` goes to infinity) of the function `f i x` is also measurable.
More concisely: If `f` is a function from natural numbers to measurable functions from a measurable space `δ` to a topological space `α` with a second countable topology, then the function mapping each `x` in `δ` to the liminf of `f i x` as `i` goes to infinity is measurable.
|
MeasureTheory.Measure.ext_of_Ici
theorem MeasureTheory.Measure.ext_of_Ici :
∀ {α : Type u_7} [inst : TopologicalSpace α] {m : MeasurableSpace α} [inst_1 : SecondCountableTopology α]
[inst_2 : LinearOrder α] [inst_3 : OrderTopology α] [inst : BorelSpace α] (μ ν : MeasureTheory.Measure α)
[inst : MeasureTheory.IsFiniteMeasure μ], (∀ (a : α), ↑↑μ (Set.Ici a) = ↑↑ν (Set.Ici a)) → μ = ν
This theorem states that for any two finite measures (`μ` and `ν`) on a Borel space (a topological space `α` with additional properties such as having a second-countable topology, being a linear order, having an order topology, and being a Borel space), the two measures are equal if they give the same measure to all left-closed right-infinite intervals. In other words, if for every element `a` in `α`, the measure `μ` of the set of all elements greater than or equal to `a` (`Set.Ici a`) is the same as the measure `ν` of the same set, then `μ` and `ν` are equal.
More concisely: If two finite measures `μ` and `ν` on a second-countable Borel space agree on the measures of all left-closed right-infinite intervals, then they are equal.
|
measurable_liminf'
theorem measurable_liminf' :
∀ {α : Type u_1} {δ : Type u_5} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
[inst_3 : MeasurableSpace δ] [inst_4 : ConditionallyCompleteLinearOrder α] [inst_5 : OrderTopology α]
[inst : SecondCountableTopology α] {ι : Type u_6} {ι' : Type u_7} {f : ι → δ → α} {v : Filter ι},
(∀ (i : ι), Measurable (f i)) →
∀ {p : ι' → Prop} {s : ι' → Set ι},
v.HasCountableBasis p s →
(∀ (j : ι'), (s j).Countable) → Measurable fun x => Filter.liminf (fun x_1 => f x_1 x) v
The theorem `measurable_liminf'` states that the `liminf` (lower limit or limit inferior) of a function over a general filter is measurable. Here, the `liminf` of a function `u` along a filter `f` is defined as the supremum of the `a` such that, as per the filter `f`, `u x ≥ a` holds eventually. This theorem applies under several conditions: we have a topological space, a measurable space, a Borel space, another measurable space, a conditionally complete linear order, and an order topology, all over a type `α`; a second countable topology over `α`; functions `f : ι → δ → α` where for each `i : ι`, `f i` is measurable; a filter `v`; and a countable basis for `v` consisting of a function `p : ι' → Prop` and a function `s : ι' → Set ι`, where each `s j` is countable. If all these conditions are met, then the function `x => Filter.liminf (fun x_1 => f x_1 x) v` is measurable.
More concisely: If `α` is a second countable topological space with a conditionally complete linear order and an order topology, `f : ι → δ → α` is a family of measurable functions, `v` is a filter on `α` with a countable basis, then `x => Filter.liminf (fun x_1 => f x_1 x) v` is a measurable function.
|
AEMeasurable.ennreal_toNNReal
theorem AEMeasurable.ennreal_toNNReal :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ENNReal} {μ : MeasureTheory.Measure α},
AEMeasurable f μ → AEMeasurable (fun x => (f x).toNNReal) μ
The theorem `AEMeasurable.ennreal_toNNReal` states that for any measure space `α` and a function `f` from `α` to the extended nonnegative real numbers `ENNReal`, if `f` is almost everywhere measurable with respect to a measure `μ`, then the function that maps `x` in `α` to the nonnegative real number part (obtained using `toNNReal`) of `f(x)` is also almost everywhere measurable with respect to the same measure `μ`. In simple terms, if a function is almost everywhere measurable, applying a transformation that gets the nonnegative real number part of its output does not prevent it from being almost everywhere measurable.
More concisely: If a function from a measure space to extended nonnegative real numbers is almost everywhere measurable, then the function that maps each point to the non-negative real part of its value is also almost everywhere measurable.
|
Mathlib.MeasureTheory.Constructions.BorelSpace.Basic._auxLemma.56
theorem Mathlib.MeasureTheory.Constructions.BorelSpace.Basic._auxLemma.56 :
∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : β → Prop}, (∃ b, (∃ a, f a = b) ∧ p b) = ∃ a, p (f a)
This theorem states that for any two types `α` and `β`, and a function `f` from `α` to `β`, and a property `p` on `β`, the proposition that there exists a `b` in `β` such that `b` equals `f a` for some `a` in `α` and `b` satisfies `p`, is equivalent to the proposition that there exists an `a` in `α` such that `f a` satisfies `p`. This is a theorem about the interchangeability of the order of quantifiers and the function application in certain conditions.
More concisely: For any types `α` and `β`, function `f` from `α` to `β`, and property `p` on `β`, the existence of an `a` in `α` such that `f a` satisfies `p` is equivalent to the existence of a `b` in `β` such that `b` is of the form `f a` for some `a` in `α` and `b` satisfies `p`.
|
AEMeasurable.ennreal_ofReal
theorem AEMeasurable.ennreal_ofReal :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℝ} {μ : MeasureTheory.Measure α},
AEMeasurable f μ → AEMeasurable (fun x => ENNReal.ofReal (f x)) μ
This theorem states that for any type `α` that has a measurable space structure and a function `f` from `α` to the real numbers `ℝ`, along with a measure `μ` on `α`, if `f` is almost everywhere measurable with respect to the measure `μ`, then the function that maps each `x` in `α` to the extended non-negative real number corresponding to the `f` value at `x` (where the `ofReal` function returns `f(x)` if it is non-negative or `0` if it is negative) is also almost everywhere measurable with respect to the same measure `μ`.
More concisely: If `α` is a measurable space with measure `μ`, `f: α -> ℝ` is almost everywhere measurable, then the function `x => max(0, ofReal f x)` is also almost everywhere measurable.
|
ContinuousOn.measurable_piecewise
theorem ContinuousOn.measurable_piecewise :
∀ {α : Type u_1} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α]
[inst_2 : OpensMeasurableSpace α] [inst_3 : TopologicalSpace γ] [inst_4 : MeasurableSpace γ]
[inst_5 : BorelSpace γ] {f g : α → γ} {s : Set α} [inst_6 : (j : α) → Decidable (j ∈ s)],
ContinuousOn f s → ContinuousOn g sᶜ → MeasurableSet s → Measurable (s.piecewise f g)
This theorem states that, given a function that is defined piecewise by two functions, if the two functions are continuous on their respective domains and the set defining the domains is a measurable set, then the piecewise function is a measurable function. In other words, if a function `f` is continuous on a set `s` and another function `g` is continuous on the complement of `s`, and `s` is a measurable set, then the function defined piecewise by `f` and `g` over `s` and its complement respectively is a measurable function. This theorem is valid in the context of measurable and topological spaces.
More concisely: Given two continuous functions defined on measurable sets with disjoint domains, their piecewise combination is a measurable function.
|
tendsto_measure_thickening_of_isClosed
theorem tendsto_measure_thickening_of_isClosed :
∀ {α : Type u_1} [inst : PseudoEMetricSpace α] [inst_1 : MeasurableSpace α] [inst_2 : OpensMeasurableSpace α]
{μ : MeasureTheory.Measure α} {s : Set α},
(∃ R > 0, ↑↑μ (Metric.thickening R s) ≠ ⊤) →
IsClosed s → Filter.Tendsto (fun r => ↑↑μ (Metric.thickening r s)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (↑↑μ s))
The theorem states that for a closed set in a pseudo emetric space, if there exists a thickening of the set with finite measure, then the measures of the `r`-thickenings of this set converge to the measure of the set itself as `r` (representing the thickness) tends towards `0` from values greater than `0`. The term "thickening" refers to the set of points that are at a distance less than `r` from some point in the set. The thickening's measure is the "size" of the thickening in the given metric space. The measure of the set and its thickenings are considered within a measurable space structure, where the measure is defined. The convergence of the measures is described in terms of filter theory, specifically using neighborhood filters.
More concisely: Given a closed set in a pseudo metric space with a measurable structure, if there exists a thickness `r` for which the thickening has finite measure, then the measures of the thickenings converge to the set's measure as `r` approaches 0.
|
SecondCountableTopologyEither.out
theorem SecondCountableTopologyEither.out :
∀ {α : Type u_6} {β : Type u_7} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
[self : SecondCountableTopologyEither α β], SecondCountableTopology α ∨ SecondCountableTopology β
This theorem, named `SecondCountableTopologyEither.out`, states that for any two types `α` and `β`, both equipped with a topological space structure, if the `SecondCountableTopologyEither` property holds for `α` and `β`, then either `α` or `β` has the property of being a second countable topology. Here, a second countable topology is one in which the topological space has a countable base, meaning it can be covered by a countable collection of open sets.
More concisely: If types `α` and `β` each have the `SecondCountableTopologyEither` property, then one of them has a second countable topology.
|
Mathlib.MeasureTheory.Constructions.BorelSpace.Basic._auxLemma.2
theorem Mathlib.MeasureTheory.Constructions.BorelSpace.Basic._auxLemma.2 :
∀ {α : Type u} {ι : Sort v} {x : α} {s : ι → Set α}, (x ∈ ⋃ i, s i) = ∃ i, x ∈ s i
This theorem states that for any type `α`, any `ι` indexed collection of sets `s` of type `α`, and any element `x` of type `α`, the proposition that `x` belongs to the union over `ι` of the sets `s` is equivalent to the existence of an index `i` in `ι` such that `x` belongs to the set `s i`. In other words, an element is in the union of a collection of sets if and only if it is in at least one of the sets in the collection.
More concisely: For any type `α`, any `ι`-indexed collection `s` of sets of type `α`, and any `x : α`, `x ∈ ⋃i, s i` if and only if there exists `i : ι`, such that `x ∈ s i`.
|
measurableSet_lt
theorem measurableSet_lt :
∀ {α : Type u_1} {δ : Type u_5} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α]
[inst_2 : OpensMeasurableSpace α] [inst_3 : MeasurableSpace δ] [inst_4 : LinearOrder α]
[inst_5 : OrderClosedTopology α] [inst : SecondCountableTopology α] {f g : δ → α},
Measurable f → Measurable g → MeasurableSet {a | f a < g a}
The theorem `measurableSet_lt` states that for any two functions `f` and `g` from a measurable space `δ` to a linearly ordered topological space `α`, if both `f` and `g` are measurable functions, then the set of all elements `a` in `δ` such that `f(a)` is less than `g(a)` is also a measurable set. This means, in terms of properties of measurable spaces, that if we look at the set of all inputs where `f` is less than `g`, this set is nicely behaved from a measure-theoretic perspective. This result relies on `α` having a topology compatible with its linear order (i.e., it is an order-closed topology) and being second-countable, which roughly means that it has a countable base for its topology.
More concisely: If `δ` is a measurable space, `α` is a linearly ordered, second-countable topological space with an order-closed topology, and `f` and `g` are measurable functions from `δ` to `α`, then the set {`a` in `δ` | `f(a)` < `g(a)`} is a measurable subset of `δ`.
|
Mathlib.MeasureTheory.Constructions.BorelSpace.Basic._auxLemma.54
theorem Mathlib.MeasureTheory.Constructions.BorelSpace.Basic._auxLemma.54 :
∀ {α : Type u} {ι : Sort u_1} {f : ι → α} {x : α}, (x ∈ Set.range f) = ∃ y, f y = x
The theorem `Mathlib.MeasureTheory.Constructions.BorelSpace.Basic._auxLemma.54` asserts that, for any type `α`, any sort `ι`, any function `f` from `ι` to `α`, and any element `x` of `α`, the condition for `x` to be in the range of `f` is equivalent to the existence of an element `y` in `ι` such that `f(y)` equals `x`. In other words, an element is in the range of a function if and only if it is the image of some input under that function.
More concisely: For any function between types, an element is in the range if and only if there exists an input mapping to that element.
|
measurable_of_tendsto_ennreal
theorem measurable_of_tendsto_ennreal :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : ℕ → α → ENNReal} {g : α → ENNReal},
(∀ (i : ℕ), Measurable (f i)) → Filter.Tendsto f Filter.atTop (nhds g) → Measurable g
This theorem states that for any measurable space `α` and a sequence of functions `f : ℕ → α → ENNReal` (which maps natural numbers and elements of `α` to extended nonnegative real numbers) and another function `g : α → ENNReal`, if each function in the sequence `f` is measurable and the sequence `f` tends to `g` as we approach infinity (`atTop`), then the limit function `g` is also measurable. In other words, the measurability property is preserved in the limit of a sequence of measurable functions under the given conditions.
More concisely: If `α` is a measurable space, `f : ℕ → α → ENNReal` is a sequence of measurable functions, and `g : α → ENNReal` is the pointwise limit of `f`, then `g` is measurable.
|
Continuous.measurable2
theorem Continuous.measurable2 :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_5} [inst : TopologicalSpace α]
[inst_1 : MeasurableSpace α] [inst_2 : OpensMeasurableSpace α] [inst_3 : TopologicalSpace β]
[inst_4 : MeasurableSpace β] [inst_5 : OpensMeasurableSpace β] [inst_6 : TopologicalSpace γ]
[inst_7 : MeasurableSpace γ] [inst_8 : BorelSpace γ] [inst_9 : MeasurableSpace δ]
[inst_10 : SecondCountableTopologyEither α β] {f : δ → α} {g : δ → β} {c : α → β → γ},
(Continuous fun p => c p.1 p.2) → Measurable f → Measurable g → Measurable fun a => c (f a) (g a)
The theorem `Continuous.measurable2` states that for any types `α`, `β`, `γ`, and `δ` which are equipped with topological spaces, measurable spaces, and other necessary structures, if we have a continuous function `c` from the product of `α` and `β` to `γ`, and if the functions `f` and `g` from `δ` to `α` and `β`, respectively, are measurable, then the function which maps an element `a` from `δ` to `c(f(a), g(a))` in `γ` is also measurable. In other words, the composition of measurable functions and a continuous function, under certain conditions, returns a measurable function.
More concisely: If `α`, `β`, `γ`, and `δ` are topological and measurable spaces, `c : α × β → γ` is continuous, and `f : δ → α` and `g : δ → β` are measurable, then the function `x ↦ c(f(x), g(x))` from `δ` to `γ` is measurable.
|
measurable_limsup'
theorem measurable_limsup' :
∀ {α : Type u_1} {δ : Type u_5} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
[inst_3 : MeasurableSpace δ] [inst_4 : ConditionallyCompleteLinearOrder α] [inst_5 : OrderTopology α]
[inst : SecondCountableTopology α] {ι : Type u_6} {ι' : Type u_7} {f : ι → δ → α} {u : Filter ι},
(∀ (i : ι), Measurable (f i)) →
∀ {p : ι' → Prop} {s : ι' → Set ι},
u.HasCountableBasis p s →
(∀ (i : ι'), (s i).Countable) → Measurable fun x => Filter.limsup (fun i => f i x) u
The theorem `measurable_limsup'` states that for a given filter `u`, if every function `f i` (for `i` in domain type `ι`) mapping from type `δ` to a topological space `α` is measurable, then for any countable basis `{p : ι' → Prop, s : ι' → Set ι}` of `u`, where every `s i` is countable, the function that maps `x` to the limit superior (limsup) of `f i x` over the filter `u` is also measurable. Here, measurability of a function refers to the property that the preimage of every measurable set under the function is also measurable. The limit superior of a function over a filter is the infimum of those values `a` such that, eventually for the filter, `u x ≤ a` holds.
More concisely: If every function in a countable family mapping from a type to a topological space is measurable, then the function that maps a point to the limit superior of the functions' values at that point with respect to a given filter is also measurable.
|
measurableSet_Iio
theorem measurableSet_Iio :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : OpensMeasurableSpace α]
[inst_3 : LinearOrder α] [inst : OrderClosedTopology α] {a : α}, MeasurableSet (Set.Iio a)
This theorem states that for any given type `α` equipped with a topology, a measurable space, an open measurable space, a linear order, and an order closed topology, and for any given element `a` of type `α`, the left-infinite right-open interval `Set.Iio a` (which is the set of all `x` in `α` such that `x` is less than `a`) is a measurable set (in the ambient measure space on `α`).
More concisely: Given a type `α` with a topology, measurable space, an open measurable space, a linear order, and an order-closed topology, the left-infinite right-open interval `Set.Iio a` is a measurable set for any `a` in `α`.
|
nullMeasurableSet_lt
theorem nullMeasurableSet_lt :
∀ {α : Type u_1} {δ : Type u_5} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α]
[inst_2 : OpensMeasurableSpace α] [inst_3 : MeasurableSpace δ] [inst_4 : LinearOrder α]
[inst_5 : OrderClosedTopology α] [inst : SecondCountableTopology α] {μ : MeasureTheory.Measure δ} {f g : δ → α},
AEMeasurable f μ → AEMeasurable g μ → MeasureTheory.NullMeasurableSet {a | f a < g a} μ
The theorem `nullMeasurableSet_lt` states that for any types `α` and `δ`, where `α` is a topological space, a measurable space, has an order that is closed in its topology, and has a second countable topology, and `δ` is a measurable space; given a measure `μ` on `δ`, and two functions `f`, `g` from `δ` to `α` that are almost everywhere measurable with respect to `μ`, then the set of points in `δ` where `f` is strictly less than `g` is a null measurable set with respect to `μ`. In other words, this set can be approximated by a measurable set up to a set of null measure.
More concisely: Given measurable spaces `α` with a second countable topology and order topology, and `δ`, a measurable space with a measure `μ`, and almost everywhere measurable functions `f` and `g` from `δ` to `α`, the set where `f` is strictly less than `g` is a null measurable set with respect to `μ`.
|
measurable_norm
theorem measurable_norm :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup α] [inst_2 : OpensMeasurableSpace α],
Measurable norm
The theorem `measurable_norm` states that for any type `α` that is a measurable space, a normed additive commutative group, and for which all open sets are measurable, the norm function (which assigns each element in `α` its mathematical norm) is a measurable function. This means that for every measurable set in the codomain, the preimage of this set under the norm function is also a measurable set in `α`.
More concisely: If `α` is a measurable space and normed additive commutative group where all open sets are measurable, then the norm function is a measurable function.
|
MeasureTheory.Measure.ext_of_Ioc_finite
theorem MeasureTheory.Measure.ext_of_Ioc_finite :
∀ {α : Type u_7} [inst : TopologicalSpace α] {m : MeasurableSpace α} [inst_1 : SecondCountableTopology α]
[inst_2 : LinearOrder α] [inst_3 : OrderTopology α] [inst : BorelSpace α] (μ ν : MeasureTheory.Measure α)
[inst : MeasureTheory.IsFiniteMeasure μ],
↑↑μ Set.univ = ↑↑ν Set.univ → (∀ ⦃a b : α⦄, a < b → ↑↑μ (Set.Ioc a b) = ↑↑ν (Set.Ioc a b)) → μ = ν
This theorem, `MeasureTheory.Measure.ext_of_Ioc_finite`, states that for any type `α` that is a topological space with a measurable space `m`, Borel space structure, second countable topology, linear order, and order topology, if we have two finite measures `μ` and `ν` on this space, then these two measures are equal if they agree on two conditions: the measures of the universal set `Set.univ` under `μ` and `ν` are equal, and for any two elements `a` and `b` in `α` where `a` is less than `b`, the measures of the left-open right-closed interval `(a, b]` under `μ` and `ν` are equal.
In other words, if two finite measures on a Borel space agree on the measure of the entire space and on all open-closed intervals, they are the same measure. If `α` is a conditionally complete linear order with no top element, this is an extensionality lemma with weaker assumptions on `μ` and `ν`.
More concisely: If `α` is a Borel space with a second countable topology, and `μ` and `ν` are finite measures on `α` with the same values on the universal set and on all left-open right-closed intervals, then `μ = ν`.
|
measurableSet_Ioi
theorem measurableSet_Ioi :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : OpensMeasurableSpace α]
[inst_3 : LinearOrder α] [inst : OrderClosedTopology α] {a : α}, MeasurableSet (Set.Ioi a)
The theorem `measurableSet_Ioi` states that for any type `α` that has a topological space structure, a measurable space structure, an open sets measurable space structure, a linear order, and an order closed topology, and for any element `a` of type `α`, the set of all elements greater than `a` (`Set.Ioi a`), also known as the left-open right-infinite interval, is a measurable set. This means that in the context of a given measure space on `α`, the set of all elements exceeding `a` is measurable.
More concisely: In a measure space on a type `α` with topological space, measurable space, open sets measurable space, linear order, and order closed topology structures, the set `Set.Ioi a` of elements greater than `a` is measurable.
|
MeasurableEmbedding.borelSpace
theorem MeasurableEmbedding.borelSpace :
∀ {α : Type u_6} {β : Type u_7} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α]
[inst_2 : MeasurableSpace β] [inst_3 : TopologicalSpace β] [hβ : BorelSpace β] {e : α → β},
MeasurableEmbedding e → Inducing e → BorelSpace α
This theorem states that for any two types `α` and `β`, if `α` is a measurable space and a topological space, and `β` is a measurable space, a topological space and a Borel space, and there exists a function `e` from `α` to `β` which is a measurable embedding and also induces the topology of `α` from `β`, then `α` is a Borel space. In other words, if we have a measurable embedding from a space to a Borel space that also preserves the topology, then the original space is also a Borel space.
More concisely: If `α` is a measurable and topological space, and `β` is a Borel space with a measurable and topology-preserving embedding `e` from `α` to `β`, then `α` is a Borel space.
|
MeasureTheory.Measure.ext_of_Ioc
theorem MeasureTheory.Measure.ext_of_Ioc :
∀ {α : Type u_7} [inst : TopologicalSpace α] {_m : MeasurableSpace α} [inst_1 : SecondCountableTopology α]
[inst_2 : ConditionallyCompleteLinearOrder α] [inst_3 : OrderTopology α] [inst_4 : BorelSpace α]
[inst_5 : NoMinOrder α] (μ ν : MeasureTheory.Measure α) [inst : MeasureTheory.IsLocallyFiniteMeasure μ],
(∀ ⦃a b : α⦄, a < b → ↑↑μ (Set.Ioc a b) = ↑↑ν (Set.Ioc a b)) → μ = ν
This theorem states that for any type `α` equipped with a topological space, a measurable space, a second countable topology, a conditionally complete linear order, an order topology, a Borel space, and a property that there is no minimum order, consider two measures `μ` and `ν` on this type `α` where `μ` is a locally finite measure. If for all pairs of `α` values `(a, b)` where `a` is less than `b`, the measure `μ` of the left-open right-closed interval from `a` to `b` equals the measure `ν` of the same interval, then the two measures `μ` and `ν` are equal.
More concisely: If `α` is a type with a second countable topology, a conditionally complete linear order, and a property with no minimum order, and `μ` and `ν` are locally finite measures on `α` such that `μ` and `ν` agree on all left-open right-closed intervals, then `μ` and `ν` are equal.
|
Measurable.coe_nnreal_ennreal
theorem Measurable.coe_nnreal_ennreal :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → NNReal}, Measurable f → Measurable fun x => ↑(f x)
This theorem states that for any measurable space `α` and a measurable function `f` mapping `α` to nonnegative real numbers (`NNReal`), the function that maps each element `x` of `α` to the image of `f(x)` under the embedding from nonnegative real numbers to extended nonnegative real numbers (`ennreal`) is also measurable. In other words, if you have a measurable function that outputs nonnegative real numbers, the function that takes those outputs and embeds them into the extended nonnegative reals remains measurable.
More concisely: If `α` is a measurable space and `f : α → ℝADER` is a measurable function, then the function `g : α → ℝADER` defined by `g x := f x.to_ennreal` is measurable.
|
Mathlib.MeasureTheory.Constructions.BorelSpace.Basic._auxLemma.55
theorem Mathlib.MeasureTheory.Constructions.BorelSpace.Basic._auxLemma.55 :
∀ {α : Type u} {β : Type v} (f : α → β) (s : Set α) (y : β), (y ∈ f '' s) = ∃ x ∈ s, f x = y
This theorem, from the `Mathlib.MeasureTheory.Constructions.BorelSpace.Basic` section of Lean's Mathematics Library, states that for any two types `α` and `β`, a function `f` from `α` to `β`, a set `s` of type `α` and an element `y` of type `β`, the proposition that `y` is in the image of `s` under `f` is equivalent to the existence of an element `x` in `s` such that `f(x)` equals `y`. In other words, an element is in the image of a set under a function if and only if there is an element in the original set that the function maps to it.
More concisely: For any function between two types and any set and element, an element is in the image of the set under the function if and only if there exists an element in the set that maps to it.
|
IsCompact.closure_subset_measurableSet
theorem IsCompact.closure_subset_measurableSet :
∀ {γ : Type u_3} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [inst_2 : BorelSpace γ]
[inst_3 : R1Space γ] {K s : Set γ}, IsCompact K → MeasurableSet s → K ⊆ s → closure K ⊆ s
The theorem `IsCompact.closure_subset_measurableSet` states that in a topological space `γ` which is also an R₁ space and Borel space, given any compact set `K` and any measurable set `s` such that `K` is a subset of `s`, the closure of `K` is also a subset of `s`. In other words, if a set `K` is compact and is contained within a measurable set `s`, then the smallest closed set that contains `K` is also contained within `s`.
More concisely: In a topological R₁ Borel space, if a compact set is contained in a measurable set, then its closure is also contained in that measurable set.
|
measurable_iSup
theorem measurable_iSup :
∀ {α : Type u_1} {δ : Type u_5} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
[inst_3 : MeasurableSpace δ] [inst_4 : ConditionallyCompleteLinearOrder α] [inst_5 : OrderTopology α]
[inst : SecondCountableTopology α] {ι : Sort u_6} [inst : Countable ι] {f : ι → δ → α},
(∀ (i : ι), Measurable (f i)) → Measurable fun b => ⨆ i, f i b
The theorem `measurable_iSup` states that for any type `α` that is a topological space and measurable space, given that `α` also has a Borel space, a conditionally complete linear order, an order topology, and a second countable topology, and for any type `δ` that is a measurable space, and for any sort `ι` that is countable, if we have a family of functions `f : ι → δ → α`, where each function in the family is measurable, then the function that maps each `b` in `δ` to the supremum (expressed as `⨆ i, f i b`) of the set of values of `f i b` as `i` ranges over `ι` is also measurable. This means the preimage of every measurable set under this supremum function is measurable.
More concisely: Given a topological space and measurable space `α` with a Borel space, a conditionally complete linear order, an order topology, and a second countable topology, and a countable family `f` of measurable functions from `δ` to `α`, the function mapping each `b` in `δ` to the supremum of `f i b` as `i` ranges over `ι` is measurable.
|
measurable_real_toNNReal
theorem measurable_real_toNNReal : Measurable Real.toNNReal
The theorem `measurable_real_toNNReal` states that the function `Real.toNNReal`, which converts a real number to a non-negative real number (returning `0` if the original number is less than `0`), is a measurable function. In mathematical terms, a function is said to be measurable if the preimage of any measurable set under this function is also measurable. In this case, for any measurable set of non-negative real numbers, the set of real numbers that are mapped to this set by `Real.toNNReal` is measurable.
More concisely: The function `Real.toNNReal : Real → ℝ⁺` is measurable, i.e., for every measurable set `M` of non-negative real numbers, the preimage `{x : Real | Real.toNNReal x ∈ M}` is a measurable subset of the real numbers.
|
measurable_biSup
theorem measurable_biSup :
∀ {α : Type u_1} {δ : Type u_5} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
[inst_3 : MeasurableSpace δ] [inst_4 : ConditionallyCompleteLinearOrder α] [inst_5 : OrderTopology α]
[inst : SecondCountableTopology α] {ι : Type u_6} (s : Set ι) {f : ι → δ → α},
s.Countable → (∀ i ∈ s, Measurable (f i)) → Measurable fun b => ⨆ i ∈ s, f i b
This theorem, 'measurable_biSup', states that for any topological space `α` that also has a measurable space structure, a Borel space structure, a conditionally complete linear order, an order topology, and a second countable topology, and for any measurable space `δ`, if we have a countable set `s` of type `ι` and a function `f` from `ι` to a function from `δ` to `α`, where every `i` in `s` yields a measurable function from `δ` to `α` when applied to `f`, then the function that maps each `b` in `δ` to the supremum over `i` in `s` of `f i b` is also measurable.
In simpler words, it's about measurability preserved under taking the supremum over a countable set of measurable functions. If every function from a countable set to our space is measurable, then the function that takes the supremum of all these functions (for each input) is also measurable.
More concisely: If `α` is a topological space with measurable and Borel structures, a conditionally complete linear order, order topology, and second countable topology, and `f` is a countable family of measurable functions from a measurable space `δ` to `α`, then the function that maps each `b` in `δ` to the supremum of `f i b` over `i` in the countable set `s` is measurable.
|