# 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 standard Borel spaces.

- A `StandardBorelSpace α` is a typeclass for measurable spaces which arise as the Borel sets of some Polish topology.

Next, we define the class of analytic sets and establish its basic properties.

- `MeasureTheory.AnalyticSet 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 `ℕ → ℕ`.
- `MeasureTheory.AnalyticSet.image_of_continuous`: a continuous image of an analytic set is analytic.
- `MeasurableSet.analyticSet`: 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.

- `MeasurablySeparable s t` states that there exists a measurable set containing `s` and disjoint from `t`.
- `AnalyticSet.measurablySeparable` shows that two disjoint analytic sets are separated by a Borel set.

We then 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.

- `MeasurableSet.image_of_continuousOn_injOn` asserts that, if `s` is a Borel measurable set in a Polish space, then the image of `s` under a continuous injective map is still Borel measurable.
- `Continuous.measurableEmbedding` states that a continuous injective map on a Polish space is a measurable embedding for the Borel sigma-algebra.
- `ContinuousOn.measurableEmbedding` is the same result for a map restricted to a measurable set on which it is continuous.
- `Measurable.measurableEmbedding` states that a measurable injective map from a standard Borel space to a second-countable topological space is a measurable embedding.
- `isClopenable_iff_measurableSet`: 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.

We use this to prove several versions of the Borel isomorphism theorem.

- `PolishSpace.measurableEquivOfNotCountable` : Any two uncountable standard Borel spaces are Borel isomorphic.
- `PolishSpace.Equiv.measurableEquiv` : Any two standard Borel spaces of the same cardinality are Borel isomorphic.

### Standard Borel Spaces #

source
class StandardBorelSpace (α : Type u_1) [MeasurableSpace α] :
Prop

A standard Borel space is a measurable space arising as the Borel sets of some Polish topology. This is useful in situations where a space has no natural topology or the natural topology in a space is non-Polish.

To endow a standard Borel space `α` with a compatible Polish topology, use `letI := upgradeStandardBorel α`. One can then use `eq_borel_upgradeStandardBorel α` to rewrite the `MeasurableSpace α` instance to `borel α t`, where `t` is the new topology.

- polish : ∃ (x : TopologicalSpace α), BorelSpace α ∧ PolishSpace α

  There exists a compatible Polish topology.

Instances

source
class UpgradedStandardBorel (α : Type u_1) extends MeasurableSpace α, TopologicalSpace α, BorelSpace α, PolishSpace α :
Type u_1

A convenience class similar to `UpgradedPolishSpace`. No instance should be registered. Instead one should use `letI := upgradeStandardBorel α`.

- MeasurableSet' : Set α → Prop
- measurableSet_empty : MeasurableSet' self.toMeasurableSpace ∅
- measurableSet_compl (s : Set α) : MeasurableSet' self.toMeasurableSpace s → MeasurableSet' self.toMeasurableSpace s ᶜ
- measurableSet_iUnion (f : ℕ → Set α) : (∀ (i : ℕ), MeasurableSet' self.toMeasurableSpace (f i)) → MeasurableSet' self.toMeasurableSpace (⋃ (i : ℕ), f i)
- IsOpen : Set α → Prop
- isOpen_univ : TopologicalSpace.IsOpen Set.univ
- isOpen_inter (s t : Set α) : TopologicalSpace.IsOpen s → TopologicalSpace.IsOpen t → TopologicalSpace.IsOpen (s ∩ t)
- isOpen_sUnion (s : Set (Set α)) : (∀ t ∈ s, TopologicalSpace.IsOpen t) → TopologicalSpace.IsOpen (⋃₀ s)
- measurable_eq : self.toMeasurableSpace = borel α
- is_open_generated_countable : ∃ (b : Set (Set α)), b.Countable ∧ self.toTopologicalSpace = TopologicalSpace.generateFrom b
- complete : ∃ (m : MetricSpace α), PseudoMetricSpace.toUniformSpace.toTopologicalSpace = self.toTopologicalSpace ∧ CompleteSpace α

Instances

source
noncomputable def upgradeStandardBorel (α : Type u_1) [MeasurableSpace α] [h : StandardBorelSpace α] :
UpgradedStandardBorel α

Use as `letI := upgradeStandardBorel α` to endow a standard Borel space `α` with a compatible Polish topology.

Warning: following this with `borelize α` will cause an error. Instead, one can rewrite with `eq_borel_upgradeStandardBorel α`. TODO: fix the corresponding bug in `borelize`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem eq_borel_upgradeStandardBorel (α : Type u_1) [MeasurableSpace α] [StandardBorelSpace α] :
inst✝ = borel α

The `MeasurableSpace α` instance on a `StandardBorelSpace` `α` is equal to the Borel sets of `upgradeStandardBorel α`.

source
@[instance 100]
instance standardBorel_of_polish {α : Type u_1} [MeasurableSpace α] [τ : TopologicalSpace α] [BorelSpace α] [PolishSpace α] :
StandardBorelSpace α
source
@[instance 100]
instance standardBorelSpace_of_discreteMeasurableSpace {α : Type u_1} [MeasurableSpace α] [DiscreteMeasurableSpace α] [Countable α] :
StandardBorelSpace α
source
@[instance 100]
instance countablyGenerated_of_standardBorel {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] :
MeasurableSpace.CountablyGenerated α
source
@[instance 100]
instance measurableSingleton_of_standardBorel {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] :
MeasurableSingletonClass α
source
instance StandardBorelSpace.prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] [StandardBorelSpace α] [StandardBorelSpace β] :
StandardBorelSpace (α × β)

A product of two standard Borel spaces is standard Borel.

source
instance StandardBorelSpace.pi_countable {ι : Type u_3} [Countable ι] {α : ι → Type u_4} [(n : ι) → MeasurableSpace (α n)] [∀ (n : ι), StandardBorelSpace (α n)] :
StandardBorelSpace ((n : ι) → α n)

A product of countably many standard Borel spaces is standard Borel.

### Analytic sets #

source
theorem MeasureTheory.AnalyticSet_def {α : Type u_3} [TopologicalSpace α] (s : Set α) :
AnalyticSet s = (s = ∅ ∨ ∃ (f : (ℕ → ℕ) → α), Continuous f ∧ Set.range f = s)
source
@[irreducible]
def MeasureTheory.AnalyticSet {α : Type u_3} [TopologicalSpace α] (s : Set α) :
Prop

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 `analyticSet_iff_exists_polishSpace_range`.

Warning: these are analytic sets in the context of descriptive set theory (which is why they are registered in the namespace `MeasureTheory`). They have nothing to do with analytic sets in the context of complex analysis.

Equations

- MeasureTheory.AnalyticSet s = (s = ∅ ∨ ∃ (f : (ℕ → ℕ) → α), Continuous f ∧ Set.range f = s)

Instances For

source
theorem MeasureTheory.analyticSet_empty {α : Type u_1} [TopologicalSpace α] :
AnalyticSet ∅
source
theorem MeasureTheory.analyticSet_range_of_polishSpace {α : Type u_1} [TopologicalSpace α] {β : Type u_3} [TopologicalSpace β] [PolishSpace β] {f : β → α} (f_cont : Continuous f) :
AnalyticSet (Set.range f)
source
theorem IsOpen.analyticSet_image {α : Type u_1} [TopologicalSpace α] {β : Type u_3} [TopologicalSpace β] [PolishSpace β] {s : Set β} (hs : IsOpen s) {f : β → α} (f_cont : Continuous f) :
MeasureTheory.AnalyticSet (f '' s)

The image of an open set under a continuous map is analytic.

source
theorem MeasureTheory.analyticSet_iff_exists_polishSpace_range {α : Type u_1} [TopologicalSpace α] {s : Set α} :
AnalyticSet s ↔ ∃ (β : Type) (h : TopologicalSpace β) (_ : PolishSpace β) (f : β → α), Continuous f ∧ Set.range f = s

A set is analytic if and only if it is the continuous image of some Polish space.

source
theorem MeasureTheory.AnalyticSet.image_of_continuousOn {α : Type u_1} [TopologicalSpace α] {β : Type u_3} [TopologicalSpace β] {s : Set α} (hs : AnalyticSet s) {f : α → β} (hf : ContinuousOn f s) :
AnalyticSet (f '' s)

The continuous image of an analytic set is analytic

source
theorem MeasureTheory.AnalyticSet.image_of_continuous {α : Type u_1} [TopologicalSpace α] {β : Type u_3} [TopologicalSpace β] {s : Set α} (hs : AnalyticSet s) {f : α → β} (hf : Continuous f) :
AnalyticSet (f '' s)
source
theorem MeasureTheory.AnalyticSet.iInter {α : Type u_1} {ι : Type u_2} [TopologicalSpace α] [hι : Nonempty ι] [Countable ι] [T2Space α] {s : ι → Set α} (hs : ∀ (n : ι), AnalyticSet (s n)) :
AnalyticSet (⋂ (n : ι), s n)

A countable intersection of analytic sets is analytic.

source
theorem MeasureTheory.AnalyticSet.iUnion {α : Type u_1} {ι : Type u_2} [TopologicalSpace α] [Countable ι] {s : ι → Set α} (hs : ∀ (n : ι), AnalyticSet (s n)) :
AnalyticSet (⋃ (n : ι), s n)

A countable union of analytic sets is analytic.

source
theorem IsClosed.analyticSet {α : Type u_1} [TopologicalSpace α] [PolishSpace α] {s : Set α} (hs : IsClosed s) :
MeasureTheory.AnalyticSet s
source
theorem MeasurableSet.isClopenable {α : Type u_1} [TopologicalSpace α] [PolishSpace α] [MeasurableSpace α] [BorelSpace α] {s : Set α} (hs : MeasurableSet s) :
PolishSpace.IsClopenable s

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 `isClopenable_iff_measurableSet`.

source
theorem MeasurableSet.analyticSet {α : Type u_3} [t : TopologicalSpace α] [PolishSpace α] [MeasurableSpace α] [BorelSpace α] {s : Set α} (hs : MeasurableSet s) :
MeasureTheory.AnalyticSet s

A Borel-measurable set in a Polish space is analytic.

source
theorem Measurable.exists_continuous {α : Type u_3} {β : Type u_4} [t : TopologicalSpace α] [PolishSpace α] [MeasurableSpace α] [BorelSpace α] [tβ : TopologicalSpace β] [MeasurableSpace β] [OpensMeasurableSpace β] {f : α → β} [SecondCountableTopology ↑(Set.range f)] (hf : Measurable f) :
∃ t' ≤ t, Continuous f ∧ PolishSpace α

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.

source
theorem MeasurableSet.analyticSet_image {X : Type u_3} {Y : Type u_4} [MeasurableSpace X] [StandardBorelSpace X] [TopologicalSpace Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] {f : X → Y} [SecondCountableTopology ↑(Set.range f)] {s : Set X} (hs : MeasurableSet s) (hf : Measurable f) :
MeasureTheory.AnalyticSet (f '' s)

The image of a measurable set in a standard Borel space under a measurable map is an analytic set.

source
theorem MeasureTheory.AnalyticSet.preimage {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [PolishSpace X] [T2Space Y] {s : Set Y} (hs : AnalyticSet s) {f : X → Y} (hf : Continuous f) :
AnalyticSet (f ⁻¹' s)

Preimage of an analytic set is an analytic set.

### Separating sets with measurable sets #

source
def MeasureTheory.MeasurablySeparable {α : Type u_3} [MeasurableSpace α] (s t : Set α) :
Prop

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

- MeasureTheory.MeasurablySeparable s t = ∃ (u : Set α), s ⊆ u ∧ Disjoint t u ∧ MeasurableSet u

Instances For

source
theorem MeasureTheory.MeasurablySeparable.iUnion {ι : Type u_2} [Countable ι] {α : Type u_3} [MeasurableSpace α] {s t : ι → Set α} (h : ∀ (m n : ι), MeasurablySeparable (s m) (t n)) :
MeasurablySeparable (⋃ (n : ι), s n) (⋃ (m : ι), t m)
source
theorem MeasureTheory.measurablySeparable_range_of_disjoint {α : Type u_1} [TopologicalSpace α] [T2Space α] [MeasurableSpace α] [OpensMeasurableSpace α] {f g : (ℕ → ℕ) → α} (hf : Continuous f) (hg : Continuous g) (h : Disjoint (Set.range f) (Set.range g)) :
MeasurablySeparable (Set.range f) (Set.range g)

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 `AnalyticSet.measurablySeparable`). Here, we prove this when our analytic sets are the ranges of functions from `ℕ → ℕ`.

source
theorem MeasureTheory.AnalyticSet.measurablySeparable {α : Type u_1} [TopologicalSpace α] [T2Space α] [MeasurableSpace α] [OpensMeasurableSpace α] {s t : Set α} (hs : AnalyticSet s) (ht : AnalyticSet t) (h : Disjoint s t) :
MeasurablySeparable s t

The Lusin separation theorem: if two analytic sets are disjoint, then they are contained in disjoint Borel sets.

source
theorem MeasureTheory.AnalyticSet.measurableSet_of_compl {α : Type u_1} [TopologicalSpace α] [T2Space α] [MeasurableSpace α] [OpensMeasurableSpace α] {s : Set α} (hs : AnalyticSet s) (hsc : AnalyticSet s ᶜ) :
MeasurableSet s

Suslin's Theorem: in a Hausdorff topological space, an analytic set with an analytic complement is measurable.

### Measurability of preimages under measurable maps #

source
theorem Measurable.measurableSet_preimage_iff_of_surjective {X : Type u_3} {Z : Type u_5} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Z] [MeasurableSpace.CountablySeparated Z] {f : X → Z} (hf : Measurable f) (hsurj : Function.Surjective f) {s : Set Z} :
MeasurableSet (f ⁻¹' s) ↔ MeasurableSet s

If `f : X → Z` is a surjective Borel measurable map from a standard Borel space to a countably separated measurable space, then the preimage of a set `s` is measurable if and only if the set is measurable. One implication is the definition of measurability, the other one heavily relies on `X` being a standard Borel space.

source
theorem Measurable.map_measurableSpace_eq {X : Type u_3} {Z : Type u_5} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Z] [MeasurableSpace.CountablySeparated Z] {f : X → Z} (hf : Measurable f) (hsurj : Function.Surjective f) :
MeasurableSpace.map f inst✝ = inst✝¹
source
theorem Measurable.map_measurableSpace_eq_borel {X : Type u_3} {Y : Type u_4} [MeasurableSpace X] [StandardBorelSpace X] [TopologicalSpace Y] [T0Space Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] [SecondCountableTopology Y] {f : X → Y} (hf : Measurable f) (hsurj : Function.Surjective f) :
MeasurableSpace.map f inst✝ = borel Y
source
theorem Measurable.borelSpace_codomain {X : Type u_3} {Y : Type u_4} [MeasurableSpace X] [StandardBorelSpace X] [TopologicalSpace Y] [T0Space Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] [SecondCountableTopology Y] {f : X → Y} (hf : Measurable f) (hsurj : Function.Surjective f) :
BorelSpace Y
source
theorem Measurable.measurableSet_preimage_iff_preimage_val {X : Type u_3} {Z : Type u_5} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Z] {f : X → Z} [MeasurableSpace.CountablySeparated ↑(Set.range f)] (hf : Measurable f) {s : Set Z} :
MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (Subtype.val ⁻¹' s)

If `f : X → Z` is a Borel measurable map from a standard Borel space to a countably separated measurable space then the preimage of a set `s` is measurable if and only if the set is measurable in `Set.range f`.

source
theorem Measurable.measurableSet_preimage_iff_inter_range {X : Type u_3} {Z : Type u_5} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Z] {f : X → Z} [MeasurableSpace.CountablySeparated ↑(Set.range f)] (hf : Measurable f) (hr : MeasurableSet (Set.range f)) {s : Set Z} :
MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ Set.range f)

If `f : X → Z` is a Borel measurable map from a standard Borel space to a countably separated measurable space and the range of `f` is measurable, then the preimage of a set `s` is measurable if and only if the intersection with `Set.range f` is measurable.

source
theorem Measurable.measurable_comp_iff_restrict {X : Type u_3} {Z : Type u_5} {β : Type u_6} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace β] [MeasurableSpace Z] {f : X → Z} [MeasurableSpace.CountablySeparated ↑(Set.range f)] (hf : Measurable f) {g : Z → β} :
Measurable (g ∘ f) ↔ Measurable ((Set.range f).restrict g)

If `f : X → Z` is a Borel measurable map from a standard Borel space to a countably separated measurable space, then for any measurable space `β` and `g : Z → β`, the composition `g ∘ f` is measurable if and only if the restriction of `g` to the range of `f` is measurable.

source
theorem Measurable.measurable_comp_iff_of_surjective {X : Type u_3} {Z : Type u_5} {β : Type u_6} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace β] [MeasurableSpace Z] [MeasurableSpace.CountablySeparated Z] {f : X → Z} (hf : Measurable f) (hsurj : Function.Surjective f) {g : Z → β} :
Measurable (g ∘ f) ↔ Measurable g

If `f : X → Z` is a surjective Borel measurable map from a standard Borel space to a countably separated measurable space, then for any measurable space `α` and `g : Z → α`, the composition `g ∘ f` is measurable if and only if `g` is measurable.

source
theorem Continuous.map_eq_borel {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [T0Space Y] [SecondCountableTopology Y] {f : X → Y} (hf : Continuous f) (hsurj : Function.Surjective f) :
MeasurableSpace.map f inst✝ = borel Y
source
theorem Continuous.map_borel_eq {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [PolishSpace X] [TopologicalSpace Y] [T0Space Y] [SecondCountableTopology Y] {f : X → Y} (hf : Continuous f) (hsurj : Function.Surjective f) :
MeasurableSpace.map f (borel X) = borel Y
source
instance Quotient.borelSpace {X : Type u_3} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] {s : Setoid X} [T0Space (Quotient s)] [SecondCountableTopology (Quotient s)] :
BorelSpace (Quotient s)
source
instance CosetSpace.borelSpace {G : Type u_3} [TopologicalSpace G] [PolishSpace G] [Group G] [MeasurableSpace G] [BorelSpace G] {N : Subgroup G} [T2Space (G ⧸ N)] [SecondCountableTopology (G ⧸ N)] :
BorelSpace (G ⧸ N)

When the subgroup `N < G` is not necessarily `Normal`, we have a `CosetSpace` as opposed to `QuotientGroup` (the next `instance`). TODO: typeclass inference should normally find this, but currently doesn't. E.g., `MeasurableSMul G (G ⧸ Γ)` fails to synthesize, even though `G ⧸ Γ` is the quotient of `G` by the action of `Γ`; it seems unable to pick up the `BorelSpace` instance.

source
instance AddCosetSpace.borelSpace {G : Type u_3} [TopologicalSpace G] [PolishSpace G] [AddGroup G] [MeasurableSpace G] [BorelSpace G] {N : AddSubgroup G} [T2Space (G ⧸ N)] [SecondCountableTopology (G ⧸ N)] :
BorelSpace (G ⧸ N)
source
instance QuotientGroup.borelSpace {G : Type u_3} [TopologicalSpace G] [PolishSpace G] [Group G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] {N : Subgroup G} [N.Normal] [IsClosed ↑N] :
BorelSpace (G ⧸ N)
source
instance QuotientAddGroup.borelSpace {G : Type u_3} [TopologicalSpace G] [PolishSpace G] [AddGroup G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] {N : AddSubgroup G} [N.Normal] [IsClosed ↑N] :
BorelSpace (G ⧸ N)

### Injective images of Borel sets #

source
theorem MeasureTheory.measurableSet_range_of_continuous_injective {γ : Type u_3} {β : Type u_4} [TopologicalSpace γ] [PolishSpace γ] [TopologicalSpace β] [T2Space β] [MeasurableSpace β] [OpensMeasurableSpace β] {f : γ → β} (f_cont : Continuous f) (f_inj : Function.Injective f) :
MeasurableSet (Set.range f)

The Lusin-Souslin theorem: the range of a continuous injective function defined on a Polish space is Borel-measurable.

source
theorem IsClosed.measurableSet_image_of_continuousOn_injOn {γ : Type u_3} [TopologicalSpace γ] [PolishSpace γ] {β : Type u_4} [TopologicalSpace β] [T2Space β] [MeasurableSpace β] [OpensMeasurableSpace β] {s : Set γ} (hs : IsClosed s) {f : γ → β} (f_cont : ContinuousOn f s) (f_inj : Set.InjOn f s) :
MeasurableSet (f '' s)
source
theorem MeasurableSet.image_of_continuousOn_injOn {γ : Type u_3} {β : Type u_5} [MeasurableSpace β] [tβ : TopologicalSpace β] [T2Space β] {s : Set γ} {f : γ → β} [OpensMeasurableSpace β] [tγ : TopologicalSpace γ] [PolishSpace γ] [MeasurableSpace γ] [BorelSpace γ] (hs : MeasurableSet s) (f_cont : ContinuousOn f s) (f_inj : Set.InjOn f s) :
MeasurableSet (f '' s)

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.

source
theorem MeasurableSet.image_of_measurable_injOn {γ : Type u_3} {α : Type u_4} [MeasurableSpace α] {s : Set γ} {f : γ → α} [MeasurableSpace.CountablySeparated α] [MeasurableSpace γ] [StandardBorelSpace γ] (hs : MeasurableSet s) (f_meas : Measurable f) (f_inj : Set.InjOn f s) :
MeasurableSet (f '' s)

The Lusin-Souslin theorem: if `s` is Borel-measurable in a standard Borel space, then its image under a measurable injective map taking values in a countably separate measurable space is also Borel-measurable.

source
theorem Continuous.measurableEmbedding {γ : Type u_3} {β : Type u_5} [MeasurableSpace β] [tβ : TopologicalSpace β] [T2Space β] {f : γ → β} [BorelSpace β] [TopologicalSpace γ] [PolishSpace γ] [MeasurableSpace γ] [BorelSpace γ] (f_cont : Continuous f) (f_inj : Function.Injective f) :
MeasurableEmbedding f

An injective continuous function on a Polish space is a measurable embedding.

source
theorem ContinuousOn.measurableEmbedding {γ : Type u_3} {β : Type u_5} [MeasurableSpace β] [tβ : TopologicalSpace β] [T2Space β] {s : Set γ} {f : γ → β} [BorelSpace β] [TopologicalSpace γ] [PolishSpace γ] [MeasurableSpace γ] [BorelSpace γ] (hs : MeasurableSet s) (f_cont : ContinuousOn f s) (f_inj : Set.InjOn f s) :
MeasurableEmbedding (s.restrict f)

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.

source
theorem Measurable.measurableEmbedding {γ : Type u_3} {α : Type u_4} [MeasurableSpace α] {f : γ → α} [MeasurableSpace.CountablySeparated α] [MeasurableSpace γ] [StandardBorelSpace γ] (f_meas : Measurable f) (f_inj : Function.Injective f) :
MeasurableEmbedding f

An injective measurable function from a standard Borel space to a countably separated measurable space is a measurable embedding.

source
theorem MeasureTheory.borel_eq_borel_of_le {γ : Type u_3} {t t' : TopologicalSpace γ} (ht : PolishSpace γ) (ht' : PolishSpace γ) (hle : t ≤ t') :
borel γ = borel γ

If one Polish topology on a type refines another, they have the same Borel sets.

source
theorem MeasureTheory.isClopenable_iff_measurableSet {γ : Type u_3} {s : Set γ} [tγ : TopologicalSpace γ] [PolishSpace γ] [MeasurableSpace γ] [BorelSpace γ] :
PolishSpace.IsClopenable s ↔ MeasurableSet s

In a Polish space, a set is clopenable if and only if it is Borel-measurable.

source
theorem MeasurableSet.image_of_monotoneOn_of_continuousOn {α : Type u_6} {β : Type u_7} {t : Set α} {g : α → β} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [LinearOrder α] [OrderTopology α] [PolishSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] [LinearOrder β] [OrderTopology β] (ht : MeasurableSet t) (hg : MonotoneOn g t) (h'g : ContinuousOn g t) :
MeasurableSet (g '' t)
source
theorem MeasurableSet.image_of_monotoneOn {α : Type u_6} {β : Type u_7} {t : Set α} {g : α → β} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [LinearOrder α] [OrderTopology α] [PolishSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] [LinearOrder β] [OrderTopology β] [SecondCountableTopology β] (ht : MeasurableSet t) (hg : MonotoneOn g t) :
MeasurableSet (g '' t)

The image of a measurable set under a monotone map is measurable.

source
theorem MeasurableSet.image_of_antitoneOn {α : Type u_6} {β : Type u_7} {t : Set α} {g : α → β} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [LinearOrder α] [OrderTopology α] [PolishSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] [LinearOrder β] [OrderTopology β] [SecondCountableTopology β] (ht : MeasurableSet t) (hg : AntitoneOn g t) :
MeasurableSet (g '' t)

The image of a measurable set under an antitone map is measurable.

source
theorem MeasureTheory.measurableSet_tendsto_fun {ι : Type u_2} {γ : Type u_3} {β : Type u_5} [MeasurableSpace β] [MeasurableSpace γ] [Countable ι] {l : Filter ι} [l.IsCountablyGenerated] [TopologicalSpace γ] [SecondCountableTopology γ] [TopologicalSpace.PseudoMetrizableSpace γ] [OpensMeasurableSpace γ] {f : ι → β → γ} (hf : ∀ (i : ι), Measurable (f i)) {g : β → γ} (hg : Measurable g) :
MeasurableSet {x : β | Filter.Tendsto (fun (n : ι) => f n x) l (nhds (g x))}

The set of points for which a sequence of measurable functions converges to a given function is measurable.

source
theorem MeasureTheory.measurableSet_exists_tendsto {ι : Type u_2} {γ : Type u_3} {β : Type u_5} [MeasurableSpace β] [TopologicalSpace γ] [PolishSpace γ] [MeasurableSpace γ] [hγ : OpensMeasurableSpace γ] [Countable ι] {l : Filter ι} [l.IsCountablyGenerated] {f : ι → β → γ} (hf : ∀ (i : ι), Measurable (f i)) :
MeasurableSet {x : β | ∃ (c : γ), Filter.Tendsto (fun (n : ι) => f n x) l (nhds c)}

The set of points for which a measurable sequence of functions converges is measurable.

source
theorem MeasurableSet.isClopenable' {α : Type u_4} [MeasurableSpace α] [StandardBorelSpace α] {s : Set α} (hs : MeasurableSet s) :
∃ (x : TopologicalSpace α), BorelSpace α ∧ PolishSpace α ∧ IsClosed s ∧ IsOpen s

If `s` is a measurable set in a standard Borel space, there is a compatible Polish topology making `s` clopen.

source
theorem MeasurableSet.standardBorel {α : Type u_4} [MeasurableSpace α] [StandardBorelSpace α] {s : Set α} (hs : MeasurableSet s) :
StandardBorelSpace ↑s

A measurable subspace of a standard Borel space is standard Borel.

### The Borel Isomorphism Theorem #

source
noncomputable def PolishSpace.borelSchroederBernstein {α : Type u_4} {β : Type u_6} [MeasurableSpace α] [MeasurableSpace β] [StandardBorelSpace α] [StandardBorelSpace β] {f : α → β} {g : β → α} (fmeas : Measurable f) (finj : Function.Injective f) (gmeas : Measurable g) (ginj : Function.Injective g) :
α ≃ᵐ β

If two standard Borel spaces admit Borel measurable injections to one another, then they are Borel isomorphic.

Equations

- PolishSpace.borelSchroederBernstein fmeas finj gmeas ginj = ⋯.schroederBernstein ⋯

Instances For

source
noncomputable def PolishSpace.measurableEquivNatBoolOfNotCountable {α : Type u_4} [MeasurableSpace α] [StandardBorelSpace α] (h : ¬Countable α) :
α ≃ᵐ (ℕ → Bool)

Any uncountable standard Borel space is Borel isomorphic to the Cantor space `ℕ → Bool`.

Equations

- PolishSpace.measurableEquivNatBoolOfNotCountable h = ⋯.some

Instances For

source
noncomputable def PolishSpace.measurableEquivOfNotCountable {α : Type u_4} {β : Type u_6} [MeasurableSpace α] [MeasurableSpace β] [StandardBorelSpace α] [StandardBorelSpace β] (hα : ¬Countable α) (hβ : ¬Countable β) :
α ≃ᵐ β

The Borel Isomorphism Theorem: Any two uncountable standard Borel spaces are Borel isomorphic.

Equations

- PolishSpace.measurableEquivOfNotCountable hα hβ = (PolishSpace.measurableEquivNatBoolOfNotCountable hα).trans (PolishSpace.measurableEquivNatBoolOfNotCountable hβ).symm

Instances For

source
noncomputable def PolishSpace.Equiv.measurableEquiv {α : Type u_4} {β : Type u_6} [MeasurableSpace α] [MeasurableSpace β] [StandardBorelSpace α] [StandardBorelSpace β] (e : α ≃ β) :
α ≃ᵐ β

The Borel Isomorphism Theorem: If two standard Borel spaces have the same cardinality, they are Borel isomorphic.

Equations

- PolishSpace.Equiv.measurableEquiv e = if h : Countable α then { toEquiv := e, measurable_toFun := ⋯, measurable_invFun := ⋯ } else PolishSpace.measurableEquivOfNotCountable h ⋯

Instances For