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

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.

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 α.

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

• upgradeStandardBorel α = (fun (τ : TopologicalSpace α) (x : BorelSpace α ∧ PolishSpace α) => UpgradedStandardBorel.mk) (Classical.choose ⋯) ⋯

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 α.

instance standardBorel_of_polish {α : Type u_1} [MeasurableSpace α] [τ : TopologicalSpace α] [BorelSpace α] [PolishSpace α] : StandardBorelSpace α

Equations

• ⋯ = ⋯

instance countablyGenerated_of_standardBorel {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] : MeasurableSpace.CountablyGenerated α

Equations

• ⋯ = ⋯

instance measurableSingleton_of_standardBorel {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] : MeasurableSingletonClass α

Equations

• ⋯ = ⋯

instance StandardBorelSpace.prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] [StandardBorelSpace α] [StandardBorelSpace β] : StandardBorelSpace (α × β)

A product of two standard Borel spaces is standard Borel.

Equations

• ⋯ = ⋯

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.

Equations

• ⋯ = ⋯

Analytic sets

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

@[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 = MeasureTheory.wrapped✝.1

theorem MeasureTheory.analyticSet_empty {α : Type u_1} [TopologicalSpace α] : MeasureTheory.AnalyticSet ∅

theorem MeasureTheory.analyticSet_range_of_polishSpace {α : Type u_1} [TopologicalSpace α] {β : Type u_3} [TopologicalSpace β] [PolishSpace β] {f : β → α} (f_cont : Continuous f) : MeasureTheory.AnalyticSet (Set.range f)

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.

theorem MeasureTheory.analyticSet_iff_exists_polishSpace_range {α : Type u_1} [TopologicalSpace α] {s : Set α} : MeasureTheory.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.

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

The continuous image of an analytic set is analytic

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

theorem MeasureTheory.AnalyticSet.iInter {α : Type u_1} {ι : Type u_2} [TopologicalSpace α] [hι : Nonempty ι] [Countable ι] [T2Space α] {s : ι → Set α} (hs : ∀ (n : ι), MeasureTheory.AnalyticSet (s n)) : MeasureTheory.AnalyticSet (⋂ (n : ι), s n)

A countable intersection of analytic sets is analytic.

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

A countable union of analytic sets is analytic.

theorem IsClosed.analyticSet {α : Type u_1} [TopologicalSpace α] [PolishSpace α] {s : Set α} (hs : IsClosed s) : MeasureTheory.AnalyticSet s

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.

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.

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.

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.

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

Preimage of an analytic set is an analytic set.

Separating sets with measurable sets

def MeasureTheory.MeasurablySeparable {α : Type u_3} [MeasurableSpace α] (s : Set α) (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

theorem MeasureTheory.MeasurablySeparable.iUnion {ι : Type u_2} [Countable ι] {α : Type u_3} [MeasurableSpace α] {s : ι → Set α} {t : ι → Set α} (h : ∀ (m n : ι), MeasureTheory.MeasurablySeparable (s m) (t n)) : MeasureTheory.MeasurablySeparable (⋃ (n : ι), s n) (⋃ (m : ι), t m)

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)) : MeasureTheory.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 ℕ → ℕ.

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

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

theorem MeasureTheory.AnalyticSet.measurableSet_of_compl {α : Type u_1} [TopologicalSpace α] [T2Space α] [MeasurableSpace α] [OpensMeasurableSpace α] {s : Set α} (hs : MeasureTheory.AnalyticSet s) (hsc : MeasureTheory.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

theorem Measurable.measurableSet_preimage_iff_of_surjective {X : Type u_3} {Z : Type u_5} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Z] [HasCountableSeparatingOn Z MeasurableSet Set.univ] {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.

theorem Measurable.map_measurableSpace_eq {X : Type u_3} {Z : Type u_5} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Z] [HasCountableSeparatingOn Z MeasurableSet Set.univ] {f : X → Z} (hf : Measurable f) (hsurj : Function.Surjective f) : MeasurableSpace.map f inst✝³ = inst✝¹

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

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

theorem Measurable.measurableSet_preimage_iff_preimage_val {X : Type u_3} {Z : Type u_5} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Z] {f : X → Z} [HasCountableSeparatingOn (↑(Set.range f)) MeasurableSet Set.univ] (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.

theorem Measurable.measurableSet_preimage_iff_inter_range {X : Type u_3} {Z : Type u_5} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Z] {f : X → Z} [HasCountableSeparatingOn (↑(Set.range f)) MeasurableSet Set.univ] (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 intesection with Set.range f is measurable.

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} [HasCountableSeparatingOn (↑(Set.range f)) MeasurableSet Set.univ] (hf : Measurable f) {g : Z → β} : Measurable (g ∘ f) ↔ Measurable (Set.restrict (Set.range f) 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.

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] [HasCountableSeparatingOn Z MeasurableSet Set.univ] {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.

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

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

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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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.

Equations

• ⋯ = ⋯

instance QuotientAddGroup.borelSpace {G : Type u_3} [TopologicalSpace G] [PolishSpace G] [AddGroup G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] {N : AddSubgroup G} [AddSubgroup.Normal N] [IsClosed ↑N] : BorelSpace (G ⧸ N)

Equations

• ⋯ = ⋯

instance QuotientGroup.borelSpace {G : Type u_3} [TopologicalSpace G] [PolishSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] {N : Subgroup G} [Subgroup.Normal N] [IsClosed ↑N] : BorelSpace (G ⧸ N)

Equations

• ⋯ = ⋯

Injective images of Borel sets

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.

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)

theorem MeasurableSet.image_of_continuousOn_injOn {γ : Type u_3} {β : Type u_5} [tβ : TopologicalSpace β] [T2Space β] [MeasurableSpace β] {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.

theorem MeasurableSet.image_of_measurable_injOn {γ : Type u_3} {α : Type u_4} [MeasurableSpace α] {s : Set γ} {f : γ → α} [HasCountableSeparatingOn α MeasurableSet Set.univ] [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.

theorem Continuous.measurableEmbedding {γ : Type u_3} {β : Type u_5} [tβ : TopologicalSpace β] [T2Space β] [MeasurableSpace β] {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.

theorem ContinuousOn.measurableEmbedding {γ : Type u_3} {β : Type u_5} [tβ : TopologicalSpace β] [T2Space β] [MeasurableSpace β] {s : Set γ} {f : γ → β} [BorelSpace β] [TopologicalSpace γ] [PolishSpace γ] [MeasurableSpace γ] [BorelSpace γ] (hs : MeasurableSet s) (f_cont : ContinuousOn f s) (f_inj : Set.InjOn f s) : MeasurableEmbedding (Set.restrict s 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.

theorem Measurable.measurableEmbedding {γ : Type u_3} {α : Type u_4} [MeasurableSpace α] {f : γ → α} [HasCountableSeparatingOn α MeasurableSet Set.univ] [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.

theorem MeasureTheory.borel_eq_borel_of_le {γ : Type u_3} {t : TopologicalSpace γ} {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.

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.

theorem MeasureTheory.measurableSet_tendsto_fun {ι : Type u_2} {γ : Type u_3} {β : Type u_5} [MeasurableSpace β] [MeasurableSpace γ] [Countable ι] {l : Filter ι} [Filter.IsCountablyGenerated l] [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.

theorem MeasureTheory.measurableSet_exists_tendsto {ι : Type u_2} {γ : Type u_3} {β : Type u_5} [MeasurableSpace β] [TopologicalSpace γ] [PolishSpace γ] [MeasurableSpace γ] [hγ : OpensMeasurableSpace γ] [Countable ι] {l : Filter ι} [Filter.IsCountablyGenerated l] {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.

theorem MeasurableSet.isClopenable' {α : Type u_1} [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.

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

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

The Borel Isomorphism Theorem

noncomputable def PolishSpace.borelSchroederBernstein {α : Type u_1} {β : Type u_3} [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 = MeasurableEmbedding.schroederBernstein ⋯ ⋯

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

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

Equations

• PolishSpace.measurableEquivNatBoolOfNotCountable h = Nonempty.some ⋯

noncomputable def PolishSpace.measurableEquivOfNotCountable {α : Type u_1} {β : Type u_3} [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

noncomputable def PolishSpace.Equiv.measurableEquiv {α : Type u_1} {β : Type u_3} [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 ⋯

theorem MeasureTheory.exists_nat_measurableEquiv_range_coe_fin_of_finite (α : Type u_1) [MeasurableSpace α] [StandardBorelSpace α] [Finite α] : ∃ (n : ℕ), Nonempty (α ≃ᵐ ↑(Set.range fun (x : Fin n) => ↑↑x))

theorem MeasureTheory.measurableEquiv_range_coe_nat_of_infinite_of_countable (α : Type u_1) [MeasurableSpace α] [StandardBorelSpace α] [Infinite α] [Countable α] : Nonempty (α ≃ᵐ ↑(Set.range Nat.cast))

theorem MeasureTheory.exists_subset_real_measurableEquiv (α : Type u_1) [MeasurableSpace α] [StandardBorelSpace α] : ∃ (s : Set ℝ), MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)

Any standard Borel space is measurably equivalent to a subset of the reals.

theorem MeasureTheory.exists_measurableEmbedding_real (α : Type u_1) [MeasurableSpace α] [StandardBorelSpace α] : ∃ (f : α → ℝ), MeasurableEmbedding f

Any standard Borel space embeds measurably into the reals.

noncomputable def MeasureTheory.embeddingReal (Ω : Type u_3) [MeasurableSpace Ω] [StandardBorelSpace Ω] : Ω → ℝ

A measurable embedding of a standard Borel space into ℝ.

Equations

• MeasureTheory.embeddingReal Ω = Exists.choose ⋯

theorem MeasureTheory.measurableEmbedding_embeddingReal (Ω : Type u_3) [MeasurableSpace Ω] [StandardBorelSpace Ω] : MeasurableEmbedding (MeasureTheory.embeddingReal Ω)