Looking to contribute

Stream: new members

[Carlos Silva]

Hello. I have a masters degree in math, and I am learning lean. I would like to practice lean by working on a topic that I could pull request afterward.

It looks like Polish spaces have not been defined yet. It also requires being "metrizable" which I don’t think is defined either. Is this a good topic to attempt? I am open to suggestions. Thanks!

My github name is carlosa95silva.

[Johan Commelin]

@Carlos Silva Which topics in maths do you like best?

[Johan Commelin]

I'm not familiar with Polish spaces... it sounds a bit specialised.

[Johan Commelin]

But maybe that's just me (-;

[Adam Topaz]

Polish spaces show up a lot in probability theory, right?

[Bolton Bailey]

From the Wikipedia introduction to Polish spaces:

In the mathematical discipline of general topology, 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. Polish spaces are so named because they were first extensively studied by Polish topologists and logicians—Sierpiński, Kuratowski, Tarski and others. However, Polish spaces are mostly studied today because they are the primary setting for descriptive set theory, including the study of Borel equivalence relations. Polish spaces are also a convenient setting for more advanced measure theory, in particular in probability theory.

So despite the name, I think they aren't as specialized as they sound. So yes, this would be good if it would help us to improve Lean's probability theory.

[Sebastien Gouezel]

Polish spaces are definitely not too specialized. Way less than condensed sets, for instance :-)

[Carlos Silva]

Hello. I like logic and the whole area in the middle of analysis and algebra (I never really specialized). Specific areas I like include topology, category theory, representation theory, and functional analysis.

I was thinking of doing Polish spaces because they are used a lot in descriptive set theory. Common examples include N^N and R.

[Adam Topaz]

@Sebastien Gouezel Polish spaces are compactly generated so they "are" a special kind of condensed set ;)

[Mario Carneiro]

What is the advantage of completely metrizable spaces over complete metric spaces? I would imagine that in most non-contrived cases the metric is describable and somewhat canonical, and the latter gives you more flexibility

[Jeremy Avigad]

The paradigm examples are 2^omega (Cantor space) and omega^omega (Baire space). You can represent them in various ways and with various metrics, none canonical. To a logician, a Polish space is roughly one that you can code up with a set of natural numbers. Descriptive set theory provides various ways of characterizing complexity -- it's like computational complexity, except for analysts. (Kechris' book, Classical Descriptive Set Theory, is a nice reference.)

[Johan Commelin]

@Carlos Silva Ok, looks like Polish spaces should be a good contribution! But it might take a bit of fiddling to get the definition correct, in the sense that it should integrate well with the rest of mathlib. I imagine that the definition could look something like this:

class polish_space (X : Type*) [t : topological_space X]
  extends separable_space X :=
(completely_metrizable :
  ∃ m : metric_space X, by exactI m.to_uniform_space.to_topological_space = t ∧ complete_space X)

But it's clear that this isn't very smooth, because there are now two potential topologies on X, namely t and m.to_uniform_space.to_topological_space. This is going to cause headaches because Lean will "always" pick the wrong one, unless there is some machinery to handle it well.

[Mario Carneiro]

I think the machinery needed in this context is an induction principle that says that to prove a property of completely metrizable spaces (depending on the topology), it suffices to prove it for all complete metric spaces