If X is a Borel space then it is measurable iso to R

Stream: new members

[Lars Ericson]

I am trying to figure out how to set up the sketch for a proof of the assertion "If X is a Borel space then it is measurable isomorphic to (0,1)" in Lean. I don't know if it's true or not. Baby steps, I am trying to make the most mathlib-compliant sketch. Here is my first pass:

import measure_theory.lebesgue_measure
import tactic

noncomputable theory

open measure_theory

universes u₁ u₂

#check measurable_space : measurable_space : Type u_1 → Type u_1

/- A measurable function is a function between the underlying sets of two measurable spaces that preserves
the structure of the spaces: the preimage of any measurable set is measurable.
In probability theory, a measurable function on a probability space is known as a random variable.
https://en.wikipedia.org/wiki/Measurable_function -/

#check @measurable
/- measurable :
  Π {α : Type u_1} {β : Type u_2} [_inst_1 : measurable_space α] [_inst_2 : measurable_space β],
    (α → β) → Prop  -/

/- For a pairing between X and Y (where Y need not be different from X) to be a bijection, four properties must hold:
each element of X must be paired with at least one element of Y,
no element of X may be paired with more than one element of Y,
each element of Y must be paired with at least one element of X, and
no element of Y may be paired with more than one element of X.
https://en.wikipedia.org/wiki/Bijection -/

class bijection (X : Type u₁) (Y : Type u₂) (f: X → Y ) :=
(into: ∀ x : X, ∃ y : Y, f(x) = y)
(unique_into: ∀ y₁ y₂ : Y, ∀ x : X, f(x)=y₁ ∧ f(x)=y₂ → y₁ = y₂)
(onto: ∀ y : Y, ∃ x : X, f(x) = y)
(unique_onto: ∀ x₁ x₂ : X, ∀ y : Y, f(x₁)=y ∧ f(x₂)=y → x₁ = x₂)

#check borel_space -- borel_space : Π (α : Type u_1) [_inst_1 : topological_space α] [_inst_2 : measurable_space α], Prop

/- A Borel isomorphism is a measurable bijective function between two measurable standard Borel spaces
https://en.wikipedia.org/wiki/Borel_isomorphism -/

def borel_isomorphism  (X : Type u₁) (Y : Type u₂)
              [TSX: topological_space X] [MSX: measurable_space]
              [TSY: topological_space Y] [MSY: measurable_space]
              (f: X → Y )
              [BSX: borel_space X] [BSY: borel_space Y]
              [measurable f] [bijection f] := true

def R01 := set.Icc (0:ℝ) 1

theorem R01_is_topological_space : topological_space R01 := sorry

theorem R01_is_measurable_space: measurable_space R01 := sorry

theorem R01_is_borel_space : borel_space R01 := sorry

-- If (X,𝑑) is s Borel space then it is measurable isomorphic to (0,1)

theorem borel_space_iso_Icc_01 (X: Type u₁) [borel_space X] :
  ∃ (f : X → (set.Icc (0:ℝ) 1)), borel_isomorphism X set_Icc_01_is_borel_space f := sorry

[Mario Carneiro]

mathlib already has function.bijective

[Mario Carneiro]

also into is trivially true

[Mario Carneiro]

as is unique_into

[Mario Carneiro]

also as I mentioned in the other thread this theorem is false, just use X = pempty

[Mario Carneiro]

This is basically asserting that every topological space is [0,1] which is crazy

[Damiano Testa]

Did you maybe mean to state the Borel isomorphism theorem?

https://math.stackexchange.com/questions/556875/any-two-uncountable-borel-subsets-of-0-1-borel-isomorphic

[Mario Carneiro]

Oh, that theorem makes a lot more sense. I think we're not really in a position to prove it though as it needs a lot of setup work in descriptive set theory

[Lars Ericson]

@Damiano Testa no, I was trying to explore a specific claim made in Math StackExchange by reasoning about it in Lean. I understand from @Mario Carneiro that it is false. Even so, I want to learn the most mathlib-ish way to express the claim. The wording of the claim is

" If (𝑌,𝑑) is s Borel space (a Polish space for instance) then it is measurable isomorphic to (0,1) and one can define an order in 𝑌. The isomorphism however is not explicit, it is based on constructions that use the axiom of choice."

[Mario Carneiro]

the "for instance" is apparently important

[Mario Carneiro]

but as stated it is not true

[Mario Carneiro]

you shouldn't believe everything you read on the internet :)

[Mario Carneiro]

damiano's link contains a mention of "standard Borel space (i.e. polish)" and I'm not sure what to make of the added adjective

[Mario Carneiro]

probably I should just look up what this borel isomorphism theorem actually says instead of guessing from peoples' oblique references to it

[Mario Carneiro]

I'm pretty sure damiano is right that this is the theorem that Oliver was thinking of

[Lars Ericson]

Here it is: Two standard Borel sets X and Y are isomorphic iff they are of the same cardinality.

[Mario Carneiro]

We don't have polish spaces AFAIK so this will be some work to formalize

[Lars Ericson]

A Polish space is a second countable, completely metrizable topological space.

• docs#topological_space.second_countable_topology
• I don't know about "completely metrizable"

[Mario Carneiro]

that means it can be equipped with a complete metric space structure

[Lars Ericson]

So all the definitions are there:

• docs#topological_space.second_countable_topology
• docs#complete_space
• docs#metric_space

[Mario Carneiro]

I don't know if there is any particular reason to define "metrizable" though

[Lars Ericson]

I was just reading the first sentence of paragraph 2 of Rao and Srivastava. You can go to nlab:

"A Polish space is a topological space that’s homeomorphic to a separable complete metric space. Every second countable locally compact Hausdorff space is a Polish space, among others."

or Wikipedia which matches Rao and Srivastava and nLab:

• a Polish space is a separable completely metrizable topological space
• that is, a space homeomorphic to a complete metric space that has a countable dense subset

The Wiki of completely metrizable is

"a topological space (X, T) for which there exists at least one metric d on X such that (X, d) is a complete metric space and d induces the topology T."

I'm not sure if this covers it:

import topology.basic
import topology.bases
import topology.uniform_space.cauchy
import topology.metric_space.basic

open topological_space

#check topological_space.second_countable_topology
#check complete_space
#check metric_space

[Mario Carneiro]

is that a question?

[Mario Carneiro]

I question the value of defining "metrizable" because usually we just care about straight up metric spaces

[Mario Carneiro]

I don't know many examples of metrizable spaces that are not metric spaces

[Lars Ericson]

If the goal is to bring polish_space into mathlib, taking Rao and Srivastava's definition of Polish space as reliable, it appears that all of the required sub-definitions are available in mathlib, so you can say

import topology.basic
import topology.bases
import topology.uniform_space.cauchy
import topology.metric_space.basic

open topological_space

universe u
variable α: Type u
variable t: topological_space α
variable s: uniform_space α

def polish_space [uniform_space α] :=
  (@topological_space.second_countable_topology α t) ∧
  (@complete_space α s)

[Lars Ericson]

Except I want one space that is all of these and I don't know how to express it in Lean. If I add s=t as follows:

def polish_space [uniform_space α] :=
  (@topological_space.second_countable_topology α t) ∧
  (@complete_space α s) ∧
  (s = t)

I get the error

type mismatch at application
  s = t
term
  t
has type
  topological_space α
but is expected to have type
  uniform_space α

[Mario Carneiro]

you should take a look at how such definitions are written in mathlib

[Lars Ericson]

I just spent an hour looking and I can't find a good model This is as close as I could get and it doesn't work:

import topology.basic
import topology.bases
import topology.uniform_space.cauchy
import topology.metric_space.basic

open topological_space

structure polish_space (α : Type*) :=
(t : topological_space α)
(is_uniform: uniform_space α )
(is_complete: @complete_space α t)
(is_second_countable: @topological_space.second_countable_topology α t)

[Mario Carneiro]

That's looking better. Drop the @

[Mario Carneiro]

One problem with this definition, mathematically speaking, is that it's not a metric space or metrizable space anymore

[Mario Carneiro]

uniform_space is not a predicate, so you shouldn't call it is_*. Use extends so that a polish space inherits from uniform space

[Mario Carneiro]

Drop t too (the field)

[Mario Carneiro]

the uniform structure implies a top space structure

[Lars Ericson]

DONE

import topology.metric_space.basic

open topological_space

structure polish_space (α : Type*) extends uniform_space α :=
(is_complete: complete_space α )
(is_second_countable: second_countable_topology α)

[Damiano Testa]

Mario Carneiro said:

I question the value of defining "metrizable" because usually we just care about straight up metric spaces

Dear Mario,

at least from a mathematical point of view, the concept of metrizable instead of metric shows up in that you do not need to fix a specific metric. This arises when you have several "natural" metrics on a space, all equivalent, and you like the freedom to move from one to the other. a couple of examples where this happens are

1. $p$-adic norms: the metrics are obtained by choosing a real number $b$ and setting nrm x = b ^ (- val x). Common choices of b are p itself or e; if you $p$-adic field is not $\mathbb{Q}_p$, but some finite extension, then is is common to choose as $b$ the cardinality of the residue field;
2. finite dimensional vector spaces, where all norms are equivalent to one another.

In the first case, it is mostly a matter of making a choice of convention to begin with and then stick to it. The second one is a little more subtle, since sometimes you obtain a "random" norm on X and then you prove that X is a finite dimensional vector space. E.g. the $\ell^p$ norms on a finite dimensional vector space are all equivalent to one another.

The bottom line, though, is that I mostly agree with your statement. I feel that this is similar to when you wonder whether a Hausdorff space comes with a function on pairs of points giving disjoint open sets or you simply assert the existence of such open sets and leave the rest to choice.

[Damiano Testa]

Dear Mario,

reading my previous answer, I want to apologize in case you feel that it is patronizing. I was simply trying to spell out a concept to which I am still trying to adjust of how the definitions that appear in formalizing mathematics later on haunt or help us!

I know that I have been struggling with extracting the "obvious" open sets from the definition of Hausdorff, so it felt very close to my heart!