Zulip Chat Archive

Stream: new members

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


view this post on Zulip Lars Ericson (Dec 20 2020 at 18:01):

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

view this post on Zulip Mario Carneiro (Dec 20 2020 at 19:52):

mathlib already has function.bijective

view this post on Zulip Mario Carneiro (Dec 20 2020 at 19:53):

also into is trivially true

view this post on Zulip Mario Carneiro (Dec 20 2020 at 19:53):

as is unique_into

view this post on Zulip Mario Carneiro (Dec 20 2020 at 19:55):

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

view this post on Zulip Mario Carneiro (Dec 20 2020 at 19:55):

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

view this post on Zulip Damiano Testa (Dec 20 2020 at 21:13):

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

view this post on Zulip Mario Carneiro (Dec 20 2020 at 21:15):

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

view this post on Zulip Lars Ericson (Dec 20 2020 at 21:39):

@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."

view this post on Zulip Mario Carneiro (Dec 20 2020 at 21:40):

the "for instance" is apparently important

view this post on Zulip Mario Carneiro (Dec 20 2020 at 21:40):

but as stated it is not true

view this post on Zulip Mario Carneiro (Dec 20 2020 at 21:40):

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

view this post on Zulip Mario Carneiro (Dec 20 2020 at 21:41):

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

view this post on Zulip Mario Carneiro (Dec 20 2020 at 21:41):

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

view this post on Zulip Mario Carneiro (Dec 20 2020 at 21:44):

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

view this post on Zulip Lars Ericson (Dec 20 2020 at 22:04):

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

view this post on Zulip Mario Carneiro (Dec 20 2020 at 22:21):

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

view this post on Zulip Lars Ericson (Dec 20 2020 at 23:17):

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

view this post on Zulip Mario Carneiro (Dec 20 2020 at 23:18):

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

view this post on Zulip Lars Ericson (Dec 20 2020 at 23:28):

So all the definitions are there:

view this post on Zulip Mario Carneiro (Dec 20 2020 at 23:32):

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

view this post on Zulip Lars Ericson (Dec 20 2020 at 23:37):

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

view this post on Zulip Mario Carneiro (Dec 20 2020 at 23:42):

is that a question?

view this post on Zulip Mario Carneiro (Dec 20 2020 at 23:43):

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

view this post on Zulip Mario Carneiro (Dec 20 2020 at 23:43):

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

view this post on Zulip Lars Ericson (Dec 21 2020 at 00:12):

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)

view this post on Zulip Lars Ericson (Dec 21 2020 at 00:28):

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 α

view this post on Zulip Mario Carneiro (Dec 21 2020 at 00:31):

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

view this post on Zulip Lars Ericson (Dec 21 2020 at 01:08):

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)

view this post on Zulip Mario Carneiro (Dec 21 2020 at 01:10):

That's looking better. Drop the @

view this post on Zulip Mario Carneiro (Dec 21 2020 at 01:12):

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

view this post on Zulip Mario Carneiro (Dec 21 2020 at 01:14):

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

view this post on Zulip Mario Carneiro (Dec 21 2020 at 01:15):

Drop t too (the field)

view this post on Zulip Mario Carneiro (Dec 21 2020 at 01:15):

the uniform structure implies a top space structure

view this post on Zulip Lars Ericson (Dec 21 2020 at 02:14):

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

view this post on Zulip Damiano Testa (Dec 21 2020 at 07:18):

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. pp-adic norms: the metrics are obtained by choosing a real number bb and setting nrm x = b ^ (- val x). Common choices of b are p itself or e; if you pp-adic field is not Qp\mathbb{Q}_p, but some finite extension, then is is common to choose as bb 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 p\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.

view this post on Zulip Damiano Testa (Dec 21 2020 at 09:02):

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!


Last updated: May 11 2021 at 23:11 UTC