Introduction: Felix W

Stream: new members

[Felix Weilacher]

Hi all! My name is Felix Weilacher. I'm a graduate student at CMU.

Does anyone know how much, if any, descriptive set theory has been formalized in Lean? I haven't been able to find any, but I also don't know much about looking.

[Reid Barton]

I think there isn't anything specific to descriptive set theory (e.g., beyond the definition of Borel sets docs#borel). I know @Sebastien Gouezel has been interested in this recently.

[Heather Macbeth]

Here's Sébastien's work in progress:
https://github.com/leanprover-community/mathlib/blob/753096224cfbbecc3e112cbbfaf8633a6e199ad8/src/measure_theory/constructions/polish.lean

[Heather Macbeth]

(Work in progress by Sébastien looks like finished peer-reviewed code from anyone else ....)

[Heather Macbeth]

Here's a discussion of that particular work.

[Felix Weilacher]

Ah, this looks very nice. Thanks!

[Sebastien Gouezel]

The current state of things is that I have formalized the basics of Polish spaces and analytic sets, with a complete proof of the Lusin-Souslin theorem asserting that a continuous injective image of a Borel set in a Polish space is Borel (which is an amazing theorem when you think of it, and highly nontrivial). With this, I have got a satisfactory statement for the change of variables formula in finite-dimensional real vector spaces:

theorem integral_image_eq_integral_abs_det_fderiv_smul {f : E → E} {s : set E}
  (hs : measurable_set s) {f' : E → (E →L[ℝ] E)}
  (hf' : ∀ x ∈ s, has_fderiv_within_at f (f' x) s x) (hf : inj_on f s) (g : E → F) :
  ∫ x in f '' s, g x ∂μ = ∫ x in s, |(f' x).det| • g (f x) ∂μ := ...

I am going to PR all of this to mathlib (the first bits are in #11965 and #11971), but it is going to take some time before everything is merged (the branch has 4259 added lines compared to master, so I expect I will need a few dozens PRs...)

[Felix Weilacher]

Thanks Sebastien!

I'm interested generally in formalizing stuff from descriptive set theory. Do you have any plans to continue down this path or were you mostly interested in the change of variables formula?

[David Wärn]

I think an interesting approach to descriptive set theory / infinite games would be to use 'coinductive types'. This should give a formally simple way to reason about games played on trees. I don't know any descriptive set theory but when I looked at the proof of Borel determinacy recently it seemed like all the basic notions (game, strategy in a game, a play in a game, a play consistent with a strategy, covering of a game...) are naturally coinductive. Lean doesn't natively support coinductive types so a first step would be to define the 'indexed M-type given an indexed container' (basically the type of strategies in a certain game), which is a little technical but also just a one-time cost.

[Mario Carneiro]

@David Wärn This already exists as docs#pfunctor.M

[Yaël Dillies]

And I direct you to this very nice paper for the context: http://www.contrib.andrew.cmu.edu/~avigad/Papers/qpf.pdf

[David Wärn]

Oh, that's very nice. Then I think one would only need the generalisation to type families / indexed M-types. For example, we can define a type of (non-wellfounded) trees like this:

import data.pfunctor.univariate.M
def game : Type 1 := pfunctor.M ⟨Type, ulift⟩
def move (g : game) : Type := g.head
def next_game (g : game) (m : move g) : game := g.children (ulift.up m)

Now I would like to define the type of "infinite paths" in a given tree aka the type of plays in the game, coinductively: a path p : path g should consist of a move p.head : move g together with a path p.tail : path (next_game g p.head).

[Sebastien Gouezel]

Felix Weilacher said:

I'm interested generally in formalizing stuff from descriptive set theory. Do you have any plans to continue down this path or were you mostly interested in the change of variables formula?

The Lusin-Souslin was my endgoal here, I am not planning to go further in this direction.

[Yaël Dillies]

Do you know about docs#mvqpf, David? It's not exactly indexed because it only accepts indexing by docs#fin2, but the generalization should be straightforward.

[David Wärn]

What does it do exactly? The generalisation from docs#pfunctor.M to indexed M-types (in the sense of https://hott.github.io/M-types/m-types.pdf ) is also straightforward, but it needs to be done and have a good API.

[Mario Carneiro]

This is easier said than done. I personally consider the QPF work a mostly failed experiment - the API is not easy to use and I don't think that there is an easy fix for that. Certainly adding indices will only make it harder to use

[Mario Carneiro]

what we really want is a coinductive command

[Mario Carneiro]

There are a lot of universe limitations in the functors too, so you can't just apply it mechanically without a lot of lifting

[Yaël Dillies]

Mario Carneiro said:

what we really want is a coinductive command

Would that involve a modification to Lean or rather an addition an additional layer as what the paper seemed to get to?

[Mario Carneiro]

Hard to say. We have a layered implementation of nested inductives in lean 3 and look how that turned out

[Mario Carneiro]

Certainly I see no way to get the desired definitional equalities without a kernel modification

[Mario Carneiro]

You can say "forget about defeq" which is fine I guess, but not so much inside the indices of an indexed coinductive

[Mario Carneiro]

I think a tactic that does an M-type construction on the spot will work better than instantiating pfunctor.M because it can avoid the universe issues, but it doesn't solve the defeq issues, or perhaps more importantly, the interaction with all other tactics

[Mario Carneiro]

By the way @David Wärn , if you are itching to use pfunctor.W anyway, there is a general technique for encoding indices in an untyped (co)inductive. You make a "skeleton" type which just ignores the indices, and then you carve out the subset of values which lie in a given index

[Eric Wieser]

Mario Carneiro said:

what we really want is a coinductive command

We have acoinductive command already, docs#tactic.coinductive_predicate (it's presumably not the right one)

[Pedro Sánchez Terraf]

Felix Weilacher said:

I'm interested generally in formalizing stuff from descriptive set theory. Do you have any plans to continue down this path or were you mostly interested in the change of variables formula?

Same here! Have you made any advances on this?

[Sebastien Gouezel]

I was only interested in the change of variables formula, so the Lusin-Souslin theorem was the endgoal for me here, and I am not planning to do anything further in this direction.

[Pedro Sánchez Terraf]

Sebastien Gouezel said:

I was only interested in the change of variables formula, so the Lusin-Souslin theorem was the endgoal for me here, and I am not planning to do anything further in this direction.

Thanks again! I'm sorry if you received a direct notification of my message (intended for @Felix Weilacher), since you already told me this.

[Felix Weilacher]

Pedro Sánchez Terraf said:

Same here! Have you made any advances on this?

No, I have been (slowly) learning enough lean to where I feel comfortable doing so, though :). I am in a course this semester on lean, and hope to write up some DST for my course projects.

[Pedro Sánchez Terraf]

I'm just starting with Lean, too, also going slow.

I'm familiar with most the basics from Kechris' book, I'd be glad in to join any project on the formalization of DST, and I know at least one person here that would also like to do that.

Are you going for classical DST, or would you like to include effective versions?

[Felix Weilacher]

OK, I'll let you know if I do start writing anything. Working together would be great.

I don't know a lot of effective DST, so I wasn't planning on including it. If you know some, I think it would be good to include for sure.

[Pedro Sánchez Terraf]

Felix Weilacher said:

No, I have been (slowly) learning enough lean to where I feel comfortable doing so, though :smile:. I am in a course this semester on lean, and hope to write up some DST for my course projects.

Hey @Felix Weilacher, just saw that you're advancing to the Borel Isomorphism theorem. Congrats! I'm still in tutorial phase, and started to read Gouëzel's sources. It seems that you accelerated quite a bit after these two months.

[Pedro Sánchez Terraf]

Felix Weilacher said:

OK, I'll let you know if I do start writing anything. Working together would be great.

I'll take a look at your repo; if your still interested in doing some joint thing, just ring the "@". Otherwise, it would be most useful to know what is probably not in your immediate interests in order to avoid overlaps.