# Zulip Chat Archive

## Stream: new members

### Topic: Introduction: Felix W

#### Felix Weilacher (Feb 14 2022 at 19:00):

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 (Feb 14 2022 at 19:03):

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 (Feb 14 2022 at 19:04):

Here's Sébastien's work in progress:

https://github.com/leanprover-community/mathlib/blob/753096224cfbbecc3e112cbbfaf8633a6e199ad8/src/measure_theory/constructions/polish.lean

#### Heather Macbeth (Feb 14 2022 at 19:04):

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

#### Heather Macbeth (Feb 14 2022 at 19:06):

Here's a discussion of that particular work.

#### Felix Weilacher (Feb 14 2022 at 19:07):

Ah, this looks very nice. Thanks!

#### Sebastien Gouezel (Feb 14 2022 at 21:22):

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 (Feb 14 2022 at 22:10):

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 (Feb 14 2022 at 23:00):

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 (Feb 14 2022 at 23:41):

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

#### Yaël Dillies (Feb 14 2022 at 23:46):

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 (Feb 15 2022 at 06:45):

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 (Feb 15 2022 at 07:06):

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 (Feb 15 2022 at 08:16):

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 (Feb 15 2022 at 08:24):

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 (Feb 15 2022 at 08:30):

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 (Feb 15 2022 at 08:31):

what we really want is a `coinductive`

command

#### Mario Carneiro (Feb 15 2022 at 08:32):

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 (Feb 15 2022 at 08:34):

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 (Feb 15 2022 at 08:35):

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

#### Mario Carneiro (Feb 15 2022 at 08:35):

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

#### Mario Carneiro (Feb 15 2022 at 08:36):

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

#### Mario Carneiro (Feb 15 2022 at 08:38):

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 (Feb 15 2022 at 08:41):

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 (Jun 12 2022 at 23:54):

Mario Carneiro said:

what we really want is a

`coinductive`

command

We have a`coinductive`

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

#### Pedro Sánchez Terraf (Sep 08 2022 at 12:37):

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 (Sep 08 2022 at 12:48):

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 (Sep 08 2022 at 12:55):

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 (Sep 08 2022 at 13:10):

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 (Sep 08 2022 at 13:15):

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 (Sep 08 2022 at 13:31):

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 (Oct 31 2022 at 20:04):

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 (Oct 31 2022 at 20:09):

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.

Last updated: Dec 20 2023 at 11:08 UTC