Measurable.exists_continuous
theorem Measurable.exists_continuous :
∀ {α : Type u_3} {β : Type u_4} [t : TopologicalSpace α] [inst : PolishSpace α] [inst : MeasurableSpace α]
[inst_1 : BorelSpace α] [tβ : TopologicalSpace β] [inst_2 : MeasurableSpace β] [inst_3 : OpensMeasurableSpace β]
{f : α → β} [inst_4 : SecondCountableTopology ↑(Set.range f)],
Measurable f → ∃ t' ≤ t, Continuous f ∧ PolishSpace α
The theorem `Measurable.exists_continuous` states that for every Borel-measurable function from a Polish space to a second-countable space, there exists a finer Polish topology on the source space such that the function is continuous. Here, a Polish space is a separable completely metrizable topological space, a second-countable space is a topological space whose topology has a countable base, and a Borel-measurable function is a function whose inverse image of any Borel set is measurable. The theorem ensures that we can refine the topology of the domain such that the given function becomes continuous and the domain remains a Polish space.
More concisely: For every Borel-measurable function from a Polish space to a second-countable space, there exists a finer Polish topology on the domain making the function continuous.
|
Measurable.measurable_comp_iff_of_surjective
theorem Measurable.measurable_comp_iff_of_surjective :
∀ {X : Type u_3} {Z : Type u_5} {β : Type u_6} [inst : MeasurableSpace X] [inst_1 : StandardBorelSpace X]
[inst_2 : MeasurableSpace β] [inst_3 : MeasurableSpace Z]
[inst_4 : HasCountableSeparatingOn Z MeasurableSet Set.univ] {f : X → Z},
Measurable f → Function.Surjective f → ∀ {g : Z → β}, Measurable (g ∘ f) ↔ Measurable g
The theorem states that given a surjective Borel measurable map `f` from a standard Borel space `X` to a countably separated measurable space `Z`, for any measurable space `α` and a function `g : Z → α`, the composition `g ∘ f` is measurable if and only if `g` itself is measurable.
This theorem is essentially attributing the measurability of the composition `g ∘ f` to the measurability of the function `g`. It is stipulating that if `f` is a surjective Borel measurable map, then the measurability of `g` is a necessary and sufficient condition for the measurability of the composition `g ∘ f`.
More concisely: A surjective Borel measurable function `f` from a standard Borel space `X` to a countably separated measurable space `Z` makes the composition `g ∘ f` measurable if and only if `g` itself is measurable for any measurable function `g` from `Z` to a measurable space `α`.
|
MeasureTheory.AnalyticSet.iInter
theorem MeasureTheory.AnalyticSet.iInter :
∀ {α : Type u_1} {ι : Type u_2} [inst : TopologicalSpace α] [hι : Nonempty ι] [inst_1 : Countable ι]
[inst_2 : T2Space α] {s : ι → Set α},
(∀ (n : ι), MeasureTheory.AnalyticSet (s n)) → MeasureTheory.AnalyticSet (⋂ n, s n)
The theorem `MeasureTheory.AnalyticSet.iInter` states that for any type `α` equipped with a topology and any index set `ι` that is both nonempty and countable, if each set in a collection of sets `{s n : n ∈ ι}` is analytic, then their countable intersection is also an analytic set. Here, an analytic set is a concept from measure theory that generalizes the notion of a Borel set. The theorem asserts that the property of being analytic is preserved under countable intersections.
More concisely: If every set in a countable collection of analytic sets (over a topological space) is analytic, then their countable intersection is also an analytic set.
|
MeasurableSet.isClopenable
theorem MeasurableSet.isClopenable :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : PolishSpace α] [inst_2 : MeasurableSpace α]
[inst_3 : BorelSpace α] {s : Set α}, MeasurableSet s → PolishSpace.IsClopenable s
This theorem states that for any given Borel-measurable set in a Polish space (a completely metrizable, separable topological space), there always exists a finer topology that is still a Polish space, in which the given set is both open and closed (clopen). This theorem is actually one side of an equivalency, as referenced by `isClopenable_iff_measurableSet`. The latter suggests that a set being Borel-measurable is equivalent to the condition that there exists a finer Polish topology making it clopen.
More concisely: For any Borel-measurable set in a Polish space, there exists a finer Polish topology making the set both open and closed (clopen).
|
Measurable.map_measurableSpace_eq
theorem Measurable.map_measurableSpace_eq :
∀ {X : Type u_3} {Z : Type u_5} [inst : MeasurableSpace X] [inst_1 : StandardBorelSpace X]
[inst_2 : MeasurableSpace Z] [inst_3 : HasCountableSeparatingOn Z MeasurableSet Set.univ] {f : X → Z},
Measurable f → Function.Surjective f → MeasurableSpace.map f inst = inst_2
This theorem states that for any two types `X` and `Y`, where `X` is a measurable space and a standard Borel space, and `Y` is a topological space, a T2 space, a measurable space, an open measurable space, and a second countable topology, for any surjective function `f` from `X` to `Y` that is measurable, the forward image of the measurable space `X` under the function `f` is the same as the measurable space of `Y`. In simpler terms, if we map the measurable space `X` to `Y` using a surjective and measurable function, we get the same measurable space as `Y`.
More concisely: For any surjective, measurable function from a measurable and standard Borel space `X` to a second countable T2 topological space `Y`, the image of `X` under `f` is a measurable subspace of `Y` that is equal to `Y`.
|
Measurable.measurable_comp_iff_restrict
theorem Measurable.measurable_comp_iff_restrict :
∀ {X : Type u_3} {Z : Type u_5} {β : Type u_6} [inst : MeasurableSpace X] [inst_1 : StandardBorelSpace X]
[inst_2 : MeasurableSpace β] [inst_3 : MeasurableSpace Z] {f : X → Z}
[inst_4 : HasCountableSeparatingOn (↑(Set.range f)) MeasurableSet Set.univ],
Measurable f → ∀ {g : Z → β}, Measurable (g ∘ f) ↔ Measurable ((Set.range f).restrict g)
The theorem `Measurable.measurable_comp_iff_restrict` states that for any given Borel measurable function `f` mapping from a standard Borel space `X` to a countably separated measurable space `Z`, and any measurable space `β` with a function `g` mapping from `Z` to `β`, the composition of `g` and `f` (i.e., `g ∘ f`) is measurable if and only if the function `g` restricted to the range of `f` is also measurable. Here, the range of `f` refers to the set of all possible output values of `f`, and restricting `g` to this range means considering only those inputs to `g` that are in the range of `f`.
More concisely: A Borel measurable function `f: X → Z` from a standard Borel space `X` to a countably separated measurable space `Z`, and a measurable function `g: Z → β` to a measurable space `β`, have composable measurable functions if and only if `g` restricted to the range of `f` is measurable.
|
MeasurableSet.analyticSet_image
theorem MeasurableSet.analyticSet_image :
∀ {X : Type u_3} {Y : Type u_4} [inst : MeasurableSpace X] [inst_1 : StandardBorelSpace X]
[inst_2 : TopologicalSpace Y] [inst_3 : MeasurableSpace Y] [inst_4 : OpensMeasurableSpace Y] {f : X → Y}
[inst_5 : SecondCountableTopology ↑(Set.range f)] {s : Set X},
MeasurableSet s → Measurable f → MeasureTheory.AnalyticSet (f '' s)
This theorem states that for any two types `X` and `Y`, where `X` is a measurable space and a standard Borel space, and `Y` is a topological space, measurable space, and open set measurable space, if a function `f` maps from `X` to `Y`, and the topology of the range of `f` is second countable, then for any measurable set `s` of type `X`, if `f` is measurable and `s` is a measurable set, the image of `s` under `f` is an analytic set in the measure theory sense. In other words, the image of a measurable set in a standard Borel space under a measurable map is an analytic set.
More concisely: If `f` is a measurable function from a standard Borel space `X` to a second countable topological space `Y`, then the image of any measurable set `s` in `X` under `f` is an analytic set in `Y`.
|
MeasureTheory.AnalyticSet.measurablySeparable
theorem MeasureTheory.AnalyticSet.measurablySeparable :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : T2Space α] [inst_2 : MeasurableSpace α]
[inst_3 : OpensMeasurableSpace α] {s t : Set α},
MeasureTheory.AnalyticSet s →
MeasureTheory.AnalyticSet t → Disjoint s t → MeasureTheory.MeasurablySeparable s t
The Lusin separation theorem states that, for any two analytical sets in a topological space that is also a T2 space and a measurable space, if the sets are disjoint, meaning there is no element that belongs to both sets, then they can be contained in two disjoint Borel sets. Here, a Borel set is a set that can be constructed from open sets through the operations of countable union, countable intersection, and relative complement. "Measurably separable" indicates that there exists a measurable set which contains one of the analytic sets and is disjoint from the other.
More concisely: In a T2 topological space and measurable space, two disjoint analytic sets can be separated by disjoint Borel sets.
|
Measurable.measurableSet_preimage_iff_of_surjective
theorem Measurable.measurableSet_preimage_iff_of_surjective :
∀ {X : Type u_3} {Z : Type u_5} [inst : MeasurableSpace X] [inst_1 : StandardBorelSpace X]
[inst_2 : MeasurableSpace Z] [inst_3 : HasCountableSeparatingOn Z MeasurableSet Set.univ] {f : X → Z},
Measurable f → Function.Surjective f → ∀ {s : Set Z}, MeasurableSet (f ⁻¹' s) ↔ MeasurableSet s
This theorem states that if there exists a surjective (one-to-one onto) Borel measurable function `f` mapping from a standard Borel space `X` to a topological space `Y` with a second countable topology, then the pre-image of a set `s` in `Y` under the function `f` is measurable if and only if the set `s` itself is measurable. This theorem is fundamental in measure theory and relies heavily on the property of `X` being a standard Borel space. One direction of the statement is the definition of measurability, while the other direction requires more detailed justification based on the properties of Borel spaces.
More concisely: A surjective Borel measurable function from a standard Borel space to a second countable topological space preserves measurability: the preimage of any measurable set is measurable.
|
MeasureTheory.AnalyticSet.iUnion
theorem MeasureTheory.AnalyticSet.iUnion :
∀ {α : Type u_1} {ι : Type u_2} [inst : TopologicalSpace α] [inst_1 : Countable ι] {s : ι → Set α},
(∀ (n : ι), MeasureTheory.AnalyticSet (s n)) → MeasureTheory.AnalyticSet (⋃ n, s n)
The theorem `MeasureTheory.AnalyticSet.iUnion` states that for any types `α` and `ι`, given a topological space on `α` and assuming that `ι` is countable, for any function `s` that maps from `ι` to a set of `α`, if every set `s(n)` for `n` in `ι` is an analytic set, then the countable union of these sets (i.e., the union over all `n` of `s(n)`) is also an analytic set. In other words, it says that the property of being analytic is closed under countable unions.
More concisely: Given a topological space on a countable type `α`, if every set in the countable family of analytic subsets of `α` is analytic, then their countable union is also an analytic subset of `α`.
|
MeasureTheory.AnalyticSet.measurableSet_of_compl
theorem MeasureTheory.AnalyticSet.measurableSet_of_compl :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : T2Space α] [inst_2 : MeasurableSpace α]
[inst_3 : OpensMeasurableSpace α] {s : Set α},
MeasureTheory.AnalyticSet s → MeasureTheory.AnalyticSet sᶜ → MeasurableSet s
**Suslin's Theorem**: In the context of a Hausdorff topological space, which is a type of topological space that satisfies the T2 axiom (i.e., any two distinct points in the space can be separated by disjoint neighborhoods), a set is considered measurable if it is both analytic and its complement is also analytic. Here, an analytic set refers to a specific type of set that can be represented in a certain way in terms of Borel sets (a concept from measure theory). This theorem is part of the measure theory and is important in the study of topological spaces and sets.
More concisely: In a Hausdorff space, a set is measurable if and only if it and its complement are both analytic.
|
IsOpen.analyticSet_image
theorem IsOpen.analyticSet_image :
∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_3} [inst_1 : TopologicalSpace β] [inst_2 : PolishSpace β]
{s : Set β}, IsOpen s → ∀ {f : β → α}, Continuous f → MeasureTheory.AnalyticSet (f '' s)
The theorem `IsOpen.analyticSet_image` states that for any two types `α` and `β`, both of which have topological space structures, and where `β` also has a Polish space structure, if `s` is an open set in `β` and `f` is a continuous function from `β` to `α`, then the image of `s` under `f` is an analytic set. In mathematical terms, this theorem says that if `s` is a set in a Polish space that is open with respect to the topological structure, and `f` is a continuous function mapping from the Polish space to some other topological space, then the image of `s` under `f` is an analytic set.
More concisely: If `s` is an open subset of a Polish space `β` and `f` is a continuous function from `β` to a topological space `α`, then the image `f''s` is an analytic set in `α`.
|
MeasureTheory.AnalyticSet_def
theorem MeasureTheory.AnalyticSet_def :
∀ {α : Type u_3} [inst : TopologicalSpace α] (s : Set α),
MeasureTheory.AnalyticSet s = (s = ∅ ∨ ∃ f, Continuous f ∧ Set.range f = s)
The theorem `MeasureTheory.AnalyticSet_def` states that for any set `s` of a certain type `α` in a topological space, `s` is an analytic set if and only if `s` is either an empty set or there exists a continuous function `f` such that its range is `s`. Here, topological space refers to a set endowed with the structure that allows the definition of continuity of functions, and continuous function is a function where small changes in the input result in small changes in the output. The range of a function is the set of all possible output values.
More concisely: A set in a topological space is analytic if and only if it is empty or the range of a continuous function.
|
MeasureTheory.isClopenable_iff_measurableSet
theorem MeasureTheory.isClopenable_iff_measurableSet :
∀ {γ : Type u_3} {s : Set γ} [tγ : TopologicalSpace γ] [inst : PolishSpace γ] [inst : MeasurableSpace γ]
[inst_1 : BorelSpace γ], PolishSpace.IsClopenable s ↔ MeasurableSet s
The theorem `MeasureTheory.isClopenable_iff_measurableSet` states that, within a Polish space (a complete, separable metric space), a set is clopenable if and only if it is Borel-measurable. A set is considered clopenable if there exists a finer Polish topology on the space where this set is both open and closed. Meanwhile, a set is considered Borel-measurable if it belongs to the smallest σ-algebra containing all open sets, which is the Borel σ-algebra, under the ambient measure space on the set.
More concisely: In a Polish space, a set is clopen if and only if it is Borel-measurable.
|
Measurable.measurableSet_preimage_iff_inter_range
theorem Measurable.measurableSet_preimage_iff_inter_range :
∀ {X : Type u_3} {Z : Type u_5} [inst : MeasurableSpace X] [inst_1 : StandardBorelSpace X]
[inst_2 : MeasurableSpace Z] {f : X → Z}
[inst_3 : HasCountableSeparatingOn (↑(Set.range f)) MeasurableSet Set.univ],
Measurable f →
MeasurableSet (Set.range f) → ∀ {s : Set Z}, MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ Set.range f)
The theorem `Measurable.measurableSet_preimage_iff_inter_range` states that if we have a Borel measurable mapping `f` from a standard Borel space `X` to a countably separated measurable space `Z`, and if the range of `f` is measurable, then a set `s` in `Z` has a measurable preimage under `f` if and only if the intersection of `s` with the range of `f` is measurable. In other words, the measurability of the preimage of a set under this mapping is equivalent to the measurability of the intersection of that set with the range of the mapping.
More concisely: A Borel measurable function from a standard Borel space to a countably separated measurable space with measurable range preserves measurability of sets under preimages, that is, for any set in the codomain, its measurability is equivalent to the measurability of its intersection with the range.
|
ContinuousOn.measurableEmbedding
theorem ContinuousOn.measurableEmbedding :
∀ {γ : Type u_3} {β : Type u_5} [tβ : TopologicalSpace β] [inst : T2Space β] [inst : MeasurableSpace β] {s : Set γ}
{f : γ → β} [inst_1 : BorelSpace β] [inst_2 : TopologicalSpace γ] [inst_3 : PolishSpace γ]
[inst_4 : MeasurableSpace γ] [inst_5 : BorelSpace γ],
MeasurableSet s → ContinuousOn f s → Set.InjOn f s → MeasurableEmbedding (s.restrict f)
The theorem states that for a set `s` in a Polish space `γ` and a function `f` mapping from `γ` to a T2 and Borel-measurable space `β`, if `s` is Borel-measurable, `f` is continuous on `s`, and `f` is injective on `s` (meaning the restriction of `f` to `s` is injective), then the restriction of `f` to `s` is a measurable embedding. In mathematical terms, if `s` is a Borel set in a Polish space, and `f:γ→β` is a continuous, injective function on `s`, where `β` is a Hausdorff and Borel space, then the restriction of `f` to `s` is a measurable embedding. A measurable embedding is a function that preserves the measurable structures between two measurable spaces.
More concisely: If `s` is a Borel set in a Polish space and `f:γ→β` is a continuous, injective function on `s`, where `β` is a Hausdorff and Borel space, then the restriction of `f` to `s` is a measurable embedding.
|
MeasurableSet.image_of_measurable_injOn
theorem MeasurableSet.image_of_measurable_injOn :
∀ {γ : Type u_3} {α : Type u_4} [inst : MeasurableSpace α] {s : Set γ} {f : γ → α}
[inst_1 : HasCountableSeparatingOn α MeasurableSet Set.univ] [inst_2 : MeasurableSpace γ]
[inst_3 : StandardBorelSpace γ], MeasurableSet s → Measurable f → Set.InjOn f s → MeasurableSet (f '' s)
The Lusin-Souslin theorem states that if a set `s` is Borel-measurable in a standard Borel space (a measurable space generated by open sets), then the image of this set under an injective (one-to-one) measurable function `f` that maps into a countably separated measurable space (a space where all measurable sets are separated by countably many points) is also Borel-measurable. In other words, measurability and injectivity of a function are preserved under the operation of image formation in the context of standard Borel and countably separated measurable spaces.
More concisely: If `s` is a Borel-measurable set in a standard Borel space and `f` is an injective, measurable function into a countably separated measurable space, then `f''s` is Borel-measurable.
|
Measurable.measurableEmbedding
theorem Measurable.measurableEmbedding :
∀ {γ : Type u_3} {α : Type u_4} [inst : MeasurableSpace α] {f : γ → α}
[inst_1 : HasCountableSeparatingOn α MeasurableSet Set.univ] [inst_2 : MeasurableSpace γ]
[inst_3 : StandardBorelSpace γ], Measurable f → Function.Injective f → MeasurableEmbedding f
This theorem states that for any injective measurable function `f` from a standard Borel space type `γ` to a countably separated measurable space type `α` (which is equipped with a measurable space structure), `f` is a measurable embedding. Here, a space is called countably separated if there exists a countable set such that any two distinct points in the space can be separated by a measurable set in this countable collection. A function is a measurable embedding if the function is measurable and the preimage of every measurable set is measurable. A standard Borel space is a measurable space that is generated by open subsets of a topological space.
More concisely: A injective measurable function from a standard Borel space to a countably separated measurable space is a measurable embedding.
|
Continuous.measurableEmbedding
theorem Continuous.measurableEmbedding :
∀ {γ : Type u_3} {β : Type u_5} [tβ : TopologicalSpace β] [inst : T2Space β] [inst : MeasurableSpace β] {f : γ → β}
[inst_1 : BorelSpace β] [inst_2 : TopologicalSpace γ] [inst_3 : PolishSpace γ] [inst_4 : MeasurableSpace γ]
[inst_5 : BorelSpace γ], Continuous f → Function.Injective f → MeasurableEmbedding f
The theorem states that for any types `γ` and `β`, where `β` is a topological space with a T2 separation axiom (also known as a Hausdorff space), and both `β` and `γ` are measurable spaces with Borel σ-algebra, if `f` is a function from `γ` to `β` and `γ` is a Polish space (a complete, separable metric space) such that `f` is a continuous and injective function, then `f` is a measurable embedding. A measurable embedding is a function that preserves the measurability of sets, i.e., the preimage of every measurable set under `f` is also measurable.
More concisely: If `γ` is a Polish space, `β` is a T2 topological space with a Borel σ-algebra, `f: γ → β` is a continuous and injective function, then `f` is a measurable embedding.
|
MeasureTheory.AnalyticSet.preimage
theorem MeasureTheory.AnalyticSet.preimage :
∀ {X : Type u_3} {Y : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : PolishSpace X]
[inst_3 : T2Space Y] {s : Set Y},
MeasureTheory.AnalyticSet s → ∀ {f : X → Y}, Continuous f → MeasureTheory.AnalyticSet (f ⁻¹' s)
This theorem states that the preimage of an analytic set is an analytic set. More specifically, for every pair of types `X` and `Y`, if `X` is a Polish space and `Y` is a T2 space, then for every set `s` of type `Y`, if `s` is an analytic set, then for any continuous function `f` from `X` to `Y`, the preimage of `s` under `f` is also an analytic set.
Here, a Polish space is a complete separable metric space, a T2 space (also known as a Hausdorff space) is a topological space in which distinct points have disjoint neighborhoods, and an analytic set is a set that can be written as the continuous image of a Polish space. The preimage of a set under a function is the set of all inputs which map to a member of the original set.
More concisely: If `X` is a Polish space, `Y` is a T2 space, `s` is an analytic set in `Y`, and `f` is a continuous function from `X` to `Y`, then the preimage `f⁻¹(s)` is an analytic set in `X`.
|
MeasurableSet.standardBorel
theorem MeasurableSet.standardBorel :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : StandardBorelSpace α] {s : Set α},
MeasurableSet s → StandardBorelSpace ↑s
This theorem states that, for any type `α` that is a measurable space and a standard Borel space, any measurable set `s` within this type is also a standard Borel space. In mathematical terms, if we have a standard Borel space `α` and a set `s` in `α` which is measurable, then the subspace induced by `s` is also a standard Borel space.
More concisely: If `α` is a standard Borel space and `s` is a measurable subset of `α`, then `s` is also a standard Borel space.
|
MeasureTheory.measurablySeparable_range_of_disjoint
theorem MeasureTheory.measurablySeparable_range_of_disjoint :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : T2Space α] [inst_2 : MeasurableSpace α]
[inst_3 : OpensMeasurableSpace α] {f g : (ℕ → ℕ) → α},
Continuous f →
Continuous g →
Disjoint (Set.range f) (Set.range g) → MeasureTheory.MeasurablySeparable (Set.range f) (Set.range g)
This theorem is a detailed step in proving the Lusin separation theorem. It states that if we have two disjoint analytic sets that are the ranges of functions from the natural numbers to natural numbers, then these sets are contained in separate Borel sets. More formally, for any topological space that is also a T2 space and a measurable space, and for any two continuous functions `f` and `g` mapping from the set of functions from the natural numbers to natural numbers to this topological space, if the range of `f` and the range of `g` are disjoint, then there exists a measurable set that contains the range of `f` and is disjoint from the range of `g`. This measurable set is a Borel set, demonstrating the principle of measurably separable sets.
More concisely: In a T2 topological space and measurable space, if two continuous functions mapping natural numbers to natural numbers have disjoint ranges, then there exists a measurable (Borel) set containing the range of one function and disjoint from the range of the other.
|
MeasurableSet.analyticSet
theorem MeasurableSet.analyticSet :
∀ {α : Type u_3} [t : TopologicalSpace α] [inst : PolishSpace α] [inst : MeasurableSpace α] [inst_1 : BorelSpace α]
{s : Set α}, MeasurableSet s → MeasureTheory.AnalyticSet s
The theorem `MeasurableSet.analyticSet` states that for any type `α` that is equipped with a `TopologicalSpace` structure, a `PolishSpace` structure, a `MeasurableSpace` structure, and a `BorelSpace` structure, any Borel-measurable set `s` of type `α` is also an analytic set. In other words, if a set in a Polish space (a complete separable metric space) is measurable in the Borel sense (measurable with respect to the Borel sigma algebra, which is generated by open sets), then that set is also an analytic set (a continuous image of a Borel set).
More concisely: In a Polish space equipped with a Borel, Measurable, and Polish topology, every Borel-measurable set is an analytic set.
|
MeasureTheory.measurableSet_range_of_continuous_injective
theorem MeasureTheory.measurableSet_range_of_continuous_injective :
∀ {γ : Type u_3} {β : Type u_4} [inst : TopologicalSpace γ] [inst_1 : PolishSpace γ] [inst_2 : TopologicalSpace β]
[inst_3 : T2Space β] [inst_4 : MeasurableSpace β] [inst_5 : OpensMeasurableSpace β] {f : γ → β},
Continuous f → Function.Injective f → MeasurableSet (Set.range f)
The Lusin-Souslin theorem states that the image (or range) of a continuous and injective function, which is defined on a Polish space (a separable completely metrizable topological space), is a Borel-measurable set. In other words, if you have a function that is continuous, one-to-one, and its domain is a Polish space, then the set of all its possible outcomes (i.e., its image or range) can be measured in the sense of Borel measure theory. This theorem is formulated in the Lean 4 Theorem Prover language.
More concisely: A continuous and injective function from a Polish space to a metric space maps Polish sets to Borel sets.
|
MeasureTheory.exists_measurableEmbedding_real
theorem MeasureTheory.exists_measurableEmbedding_real :
∀ (α : Type u_1) [inst : MeasurableSpace α] [inst_1 : StandardBorelSpace α], ∃ f, MeasurableEmbedding f
This theorem states that, given any standard Borel space (a topological space whose sigma algebra of measurable sets is generated by its open sets), there exists a measurable embedding into the real numbers. In other words, we can always find a function `f` that embeds the Borel space in such a way that the function itself is measurable.
More concisely: Every standard Borel space admits a Borel embedding into the real numbers.
|
Measurable.measurableSet_preimage_iff_preimage_val
theorem Measurable.measurableSet_preimage_iff_preimage_val :
∀ {X : Type u_3} {Z : Type u_5} [inst : MeasurableSpace X] [inst_1 : StandardBorelSpace X]
[inst_2 : MeasurableSpace Z] {f : X → Z}
[inst_3 : HasCountableSeparatingOn (↑(Set.range f)) MeasurableSet Set.univ],
Measurable f → ∀ {s : Set Z}, MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (Subtype.val ⁻¹' s)
The theorem `Measurable.measurableSet_preimage_iff_preimage_val` states that for a Borel measurable function `f` from a standard Borel space `X` to a countably separated measurable space `Z`, the preimage of a set `s` under `f` is measurable if and only if the set `s` itself is measurable in the range of `f`. This is to say, the measurability of the preimage of a set under `f` is equivalent to the measurability of the preimage of the set under Subtype.val (which extracts the underlying element of a subtype), given the condition that `f` is measurable and the spaces `X` and `Z` satisfy certain properties.
More concisely: A Borel measurable function from a standard Borel space to a countably separated measurable space maps measurable sets in the range to measurable preimages.
|
MeasurableSet.isClopenable'
theorem MeasurableSet.isClopenable' :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : StandardBorelSpace α] {s : Set α},
MeasurableSet s → ∃ x, BorelSpace α ∧ PolishSpace α ∧ IsClosed s ∧ IsOpen s
The theorem `MeasurableSet.isClopenable'` states that for every measurable set `s` in a standard Borel space `α`, there exists a topology compatible with the Borel structure on `α` that makes `s` both closed and open (clopen). In this context, a set is measurable if it can be measured in the ambient measure space on `α`, a standard Borel space is a measurable space that can be generated by open sets, and a Polish space is a separable completely metrizable topological space.
More concisely: Given a measurable set `s` in a standard Borel space `α`, there exists a topology making `s` both closed and open (clopen) in `α`.
|
MeasureTheory.analyticSet_iff_exists_polishSpace_range
theorem MeasureTheory.analyticSet_iff_exists_polishSpace_range :
∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α},
MeasureTheory.AnalyticSet s ↔ ∃ β h, ∃ (_ : PolishSpace β), ∃ f, Continuous f ∧ Set.range f = s
This theorem states that for any type `α` equipped with a topology, and any set `s` of type `α`, `s` is an analytic set if and only if there exists some Polish space `β` and a continuous function `f` from `β` to `α` such that the range of `f` is exactly `s`. In other words, a set is defined to be analytic if it can be obtained as the continuous image of a Polish space, where a Polish space is a separable completely metrizable topological space.
More concisely: A set in a topological space is analytic if and only if it is the continuous image of a Polish space.
|
MeasureTheory.borel_eq_borel_of_le
theorem MeasureTheory.borel_eq_borel_of_le :
∀ {γ : Type u_3} {t t' : TopologicalSpace γ}, PolishSpace γ → PolishSpace γ → t ≤ t' → borel γ = borel γ
The theorem `MeasureTheory.borel_eq_borel_of_le` states that for any type `γ` and two Polish topologies `t` and `t'` on `γ`, if `t` refines `t'` (that is, `t` is finer than `t'` or every open set in `t'` is also an open set in `t`), then the Borel sets generated by these two topologies are the same. This theorem bridges the relationship between the refinement of topologies and the Borel sets associated with them.
More concisely: For Polish spaces `γ` and refined Polish topologies `t` and `t'` on `γ`, the generated Borel `σ`-algebras are equal: `BorelSet t = BorelSet t'`.
|
eq_borel_upgradeStandardBorel
theorem eq_borel_upgradeStandardBorel :
∀ (α : Type u_1) [inst : MeasurableSpace α] [inst_1 : StandardBorelSpace α], inst = borel α
This theorem states that for any type `α` which is a `StandardBorelSpace` and has a `MeasurableSpace` structure, this `MeasurableSpace` structure is identical to the Borel sets generated by the topology of `α`, a process denoted as `borel α`. In other words, the `MeasurableSpace` instance on a `StandardBorelSpace` `α` is equivalent to the `MeasurableSpace` structure generated by the borel sets of the upgraded standard Borel space of `α`.
More concisely: For any `StandardBorelSpace` `α`, the measurable sets form the same collection as the Borel sets generated by the topology of `α`.
|
MeasureTheory.AnalyticSet.image_of_continuousOn
theorem MeasureTheory.AnalyticSet.image_of_continuousOn :
∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_3} [inst_1 : TopologicalSpace β] {s : Set α},
MeasureTheory.AnalyticSet s → ∀ {f : α → β}, ContinuousOn f s → MeasureTheory.AnalyticSet (f '' s)
This theorem in natural language states: "The continuous image of an analytic set is analytic". More specifically, for any two types `α` and `β` with respective topological space structures, and for any set `s` of type `α`, if `s` is an analytic set, then for any function `f` from `α` to `β` which is continuous on `s`, the image of `s` under `f` is also an analytic set. In this context, a set is considered analytic if it can be represented as a countable union of closed sets, and a function is considered continuous if the pre-image of every open set is open.
More concisely: The image of an analytic set under a continuous function is an analytic set.
|
MeasureTheory.measurableSet_exists_tendsto
theorem MeasureTheory.measurableSet_exists_tendsto :
∀ {ι : Type u_2} {γ : Type u_3} {β : Type u_5} [inst : MeasurableSpace β] [inst_1 : TopologicalSpace γ]
[inst_2 : PolishSpace γ] [inst_3 : MeasurableSpace γ] [hγ : OpensMeasurableSpace γ] [inst_4 : Countable ι]
{l : Filter ι} [inst_5 : l.IsCountablyGenerated] {f : ι → β → γ},
(∀ (i : ι), Measurable (f i)) → MeasurableSet {x | ∃ c, Filter.Tendsto (fun n => f n x) l (nhds c)}
This theorem, named `MeasureTheory.measurableSet_exists_tendsto`, states that the set of points where a sequence of measurable functions converges is also measurable. More specifically, for any types `ι`, `γ`, and `β`, and given the measurable space structure on `β`, the topological space structure on `γ`, a Polish space structure on `γ`, a measurable space structure on `γ`, an open measurable space structure on `γ`, and a countable `ι`. Further given a filter `l` on `ι` which is countably generated and a sequence of functions `f` from `ι` to `β` to `γ`, where each function `f i` is measurable for each `i` in `ι`. Under these conditions, the theorem asserts that the set of all `x` in `β` for which there exists a `c` in `γ` such that the sequence `f n x` tends to `c` as `n` tends to infinity along `l`, is a measurable set. The tendency of the sequence is defined in terms of the neighborhood filter at `c`.
More concisely: Given a Polish space γ with measurable structures, a countably generated filter l on a countable index set ι, and a sequence of measurable functions f : ι -> β -> γ, the set of points x in β such that there exists a limit c in γ for the sequence f i x as i tends to infinity according to filter l, is a measurable subset of β.
|
MeasureTheory.analyticSet_range_of_polishSpace
theorem MeasureTheory.analyticSet_range_of_polishSpace :
∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_3} [inst_1 : TopologicalSpace β] [inst_2 : PolishSpace β]
{f : β → α}, Continuous f → MeasureTheory.AnalyticSet (Set.range f)
This theorem states that for any two types `α` and `β` which have topological space structures, where `β` additionally is a Polish space, and given a function `f` from `β` to `α` that is continuous, the range of `f` (the set of all possible outputs of `f`) is an analytic set. Here, a Polish space is a complete, separable metric space, and an analytic set in a topological space is a projection of a Borel set in a higher-dimensional space.
More concisely: Given two topological spaces `α` and `β` where `β` is a Polish space, and a continuous function `f` from `β` to `α`, the range of `f` is an analytic subset of `α`.
|
MeasurableSet.image_of_continuousOn_injOn
theorem MeasurableSet.image_of_continuousOn_injOn :
∀ {γ : Type u_3} {β : Type u_5} [tβ : TopologicalSpace β] [inst : T2Space β] [inst : MeasurableSpace β] {s : Set γ}
{f : γ → β} [inst_1 : OpensMeasurableSpace β] [tγ : TopologicalSpace γ] [inst_2 : PolishSpace γ]
[inst_3 : MeasurableSpace γ] [inst_4 : BorelSpace γ],
MeasurableSet s → ContinuousOn f s → Set.InjOn f s → MeasurableSet (f '' s)
The Lusin-Souslin theorem states that if a set `s` is Borel-measurable in a Polish space (a complete, separable metric space), then the image of `s` under a continuous, injective function is also Borel-measurable. This theorem is applicable for any set `s` in a topological space `γ` and function `f` from `γ` to another topological space `β`. The conditions are that `s` must be measurable, the function `f` must be continuous on `s`, and `f` must be injective on `s`. The theorem then concludes that the image of `s` under `f` is also a measurable set.
More concisely: If `s` is a Borel-measurable subset of a Polish space and `f` is a continuous, injective function, then the image `f(s)` is a Borel-measurable subset of the range space.
|
StandardBorelSpace.polish
theorem StandardBorelSpace.polish :
∀ {α : Type u_1} [inst : MeasurableSpace α] [self : StandardBorelSpace α], ∃ x, BorelSpace α ∧ PolishSpace α := by
sorry
This theorem states that for every type `α` that has both a `MeasurableSpace` and a `StandardBorelSpace` structure, there exists a topology that is both a `BorelSpace` and a `PolishSpace`. In the context of mathematical analysis, this theorem is asserting that for any given standard Borel space - a measurable space that can be generated from open sets - we can always find a compatible Polish topology, i.e., a topology that is separable and completely metrizable. This fact is fundamental in descriptive set theory and the study of measure theory on infinite-dimensional spaces.
More concisely: Given any type `α` with both `MeasurableSpace` and `StandardBorelSpace` structures, there exists a unique topology making it both a `BorelSpace` and a `PolishSpace`.
|
MeasureTheory.exists_subset_real_measurableEquiv
theorem MeasureTheory.exists_subset_real_measurableEquiv :
∀ (α : Type u_1) [inst : MeasurableSpace α] [inst_1 : StandardBorelSpace α],
∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)
The theorem `MeasureTheory.exists_subset_real_measurableEquiv` states that for any type `α`, given that `α` is equipped with a measurable space structure and also has the property of being a standard Borel space, there exists a subset `s` which is a measurable set and there exists a measurable equivalence between `α` and this subset of real numbers. In other words, any standard Borel space can be mapped onto a subset of real numbers in a way that preserves the structure of measurable sets.
More concisely: Given any standard Borel space `α`, there exists a measurable subset `s` of real numbers and a measurable equivalence from `α` to `s`.
|