The Borel sigma-algebra on Polish spaces #
We discuss several results pertaining to the relationship between the topology and the Borel structure on Polish spaces.
Main definitions and results #
First, we define the class of analytic sets and establish its basic properties.
measure_theory.analytic_set s
: a set in a topological space is analytic if it is the continuous image of a Polish space. Equivalently, it is empty, or the image ofℕ → ℕ
.measure_theory.analytic_set.image_of_continuous
: a continuous image of an analytic set is analytic.measurable_set.analytic_set
: in a Polish space, any Borel-measurable set is analytic.
Then, we show Lusin's theorem that two disjoint analytic sets can be separated by Borel sets.
measurably_separable s t
states that there exists a measurable set containings
and disjoint fromt
.analytic_set.measurably_separable
shows that two disjoint analytic sets are separated by a Borel set.
Finally, we prove the Lusin-Souslin theorem that a continuous injective image of a Borel subset of a Polish space is Borel. The proof of this nontrivial result relies on the above results on analytic sets.
measurable_set.image_of_continuous_on_inj_on
asserts that, ifs
is a Borel measurable set in a Polish space, then the image ofs
under a continuous injective map is still Borel measurable.continuous.measurable_embedding
states that a continuous injective map on a Polish space is a measurable embedding for the Borel sigma-algebra.continuous_on.measurable_embedding
is the same result for a map restricted to a measurable set on which it is continuous.measurable.measurable_embedding
states that a measurable injective map from a Polish space to a second-countable topological space is a measurable embedding.is_clopenable_iff_measurable_set
: in a Polish space, a set is clopenable (i.e., it can be made open and closed by using a finer Polish topology) if and only if it is Borel-measurable.
Analytic sets #
An analytic set is a set which is the continuous image of some Polish space. There are several
equivalent characterizations of this definition. For the definition, we pick one that avoids
universe issues: a set is analytic if and only if it is a continuous image of ℕ → ℕ
(or if it
is empty). The above more usual characterization is given
in analytic_set_iff_exists_polish_space_range
.
Warning: these are analytic sets in the context of descriptive set theory (which is why they are
registered in the namespace measure_theory
). They have nothing to do with analytic sets in the
context of complex analysis.
The image of an open set under a continuous map is analytic.
A set is analytic if and only if it is the continuous image of some Polish space.
The continuous image of an analytic set is analytic
A countable intersection of analytic sets is analytic.
A countable union of analytic sets is analytic.
Given a Borel-measurable set in a Polish space, there exists a finer Polish topology making
it clopen. This is in fact an equivalence, see is_clopenable_iff_measurable_set
.
Given a Borel-measurable function from a Polish space to a second-countable space, there exists a finer Polish topology on the source space for which the function is continuous.
Separating sets with measurable sets #
Two sets u
and v
in a measurable space are measurably separable if there
exists a measurable set containing u
and disjoint from v
.
This is mostly interesting for Borel-separable sets.
Equations
- measure_theory.measurably_separable s t = ∃ (u : set α), s ⊆ u ∧ disjoint t u ∧ measurable_set u
The hard part of the Lusin separation theorem saying that two disjoint analytic sets are
contained in disjoint Borel sets (see the full statement in analytic_set.measurably_separable
).
Here, we prove this when our analytic sets are the ranges of functions from ℕ → ℕ
.
The Lusin separation theorem: if two analytic sets are disjoint, then they are contained in disjoint Borel sets.
Injective images of Borel sets #
The Lusin-Souslin theorem: the range of a continuous injective function defined on a Polish space is Borel-measurable.
The Lusin-Souslin theorem: if s
is Borel-measurable in a Polish space, then its image under
a continuous injective map is also Borel-measurable.
The Lusin-Souslin theorem: if s
is Borel-measurable in a Polish space, then its image under
a measurable injective map taking values in a second-countable topological space
is also Borel-measurable.
An injective continuous function on a Polish space is a measurable embedding.
If s
is Borel-measurable in a Polish space and f
is continuous injective on s
, then
the restriction of f
to s
is a measurable embedding.
An injective measurable function from a Polish space to a second-countable topological space is a measurable embedding.
In a Polish space, a set is clopenable if and only if it is Borel-measurable.
The set of points for which a measurable sequence of functions converges is measurable.