Lusin Novikov In Mathlib

Stream: mathlib4

[Connor Gordon]

I'm currently working on a formalization of the Lusin Novikov theorem, and you can see my adventures in doing so in this thread and this thread. I would eventually like to push this to Mathlib, and some people encouraged me to start this process early rather than at the end, so here I am.

I've never done this before and have essentially no experience with GitHub, so where would I start with this? Is there a "Mathlib PRs for dummies" that I can read somewhere?

I also have some questions related to organization. This project has three parts that are somewhat independent of each other: definitions and properties relating to sigma ideals (which, so far as I can tell, are not implemented anywhere in Mathlib, so I used the dual filters instead and proved some convenience lemmas); two topology observations that are kind of separate from anything else (not sure if these should be in the main file or somewhere else, but I don't know where else they'd be, as they seem pretty much only useful for this project); and then the core definition of null collections and a bunch of results surrounding it, culminating in the main theorem. Should these all be in separate PRs?

I have everything I've done so far in LusinNovikov.lean, which consists of the definition of the sigma ideal and convenience lemmas, beginning work on the two lemmas in the paper, and proofs of the two topology observations. (Yes I know that this code is very inefficient at many points; I'm currently just trying to get things that work.)

Any suggestions/advice on what I should do?

[Johan Commelin]

Voila: https://leanprover-community.github.io/contribute/index.html

This should get you started. Please let me know if you have further questions about the PR process.

[Yaël Dillies]

@Anatole Dedecker, isn't a sigma ideal exactly a docs#Bornology ?

[Kyle Miller]

There's a difference -- sigma ideals allow countable unions rather than just finite unions.

[Anatole Dedecker]

Looking at the Wikipedia definition I don't think so because of the "countable union" axiom. It seems to be the dual of docs#CountableInterFilter

[Yaël Dillies]

Okay I see

[Connor Gordon]

It seems like this might be a better place to ask then in #maths , so I'll do it here. I've now finished the two topological observations and the two lemmas, and am now trying to complete the proof. For convenient reference, the original paper is Shinko-Lusin-Novikov.pdf. The proof as written in that paper isn't particularly suited for formalization in Lean directly (or at the very least, I'm not sure how to do it, so I've expanded on the splitting and Cantor scheme process a bit more in Outline.pdf.

That leads me to where I'm asking for help now. I'm reasonably convinced that I can implement a proof for the splitting lemma as written in the outline. That being said, I'm not sure how to go from that splitting lemma to the rest of the proof, so I'd rather figure that out first in case I need to modify it. I mainly plan on using the infrastructure in docs#CantorScheme.inducedMap to witness option (2) in light of failure of (1), but I'm not really sure how to construct the Cantor scheme. The main example I know of is docs#Perfect.exists_nat_bool_injection (I'll tag @Felix Weilacher as the author of both of these), but that one involves a splitting lemma only dependent on a single set, where as the Lusin-Novikov argument depends on splitting an entire collection of sets at a time, and I'm not really sure how to actually define the scheme.

Does anyone have any ideas on how I could do this? I'm happy to do most of the work in formalizing the splitting lemma and proving the resulting scheme actually has the properties we want it to, but I'm not really sure what precise statement of the splitting lemma is ideal or how to actually define the scheme.

[Felix Weilacher]

A cantor scheme here is a map from List Bool to Set X. It seems like the splitting lemma as you've set it up will let you construct such a map by induction on the length of the input list. What's the issue?

[Connor Gordon]

I suppose first off that I'm not actually sure how to define a function from List Bool by induction on the length of the list. I see how to define things based on pattern matching nil vs. a :: l, but the latter seems too "local" to the specific list to be able to apply the splitting lemma to all lists of the same length at once. I guess my first question is what the setup for inducting on the length of the list in a definition would look like. (Are there any examples of such definitions in Mathlib?)

But beyond that, the tools I have built up thus far would enable splitting a Finset (Set X), but I'm not sure how to actually index that Finset using the finite strings. I'd imagine I'd want to do that with the splitting lemma, namely having the result of the splitting be indexed by a Bool. I've just not been successful in wrapping my head around that. (Namely, what should the actual types of the inputs and outputs to my splitting lemma be; I currently have unindexed finsets but eventually will need to index them by List Bools.)

[Felix Weilacher]

Maybe you could define a function f : Nat \to P by induction, where f 0 = X, f n has size 2^n, etc. Then afterwards give the appropriate bijection, for each n, between strings of length n and f n.

[Felix Weilacher]

Inducting on list length would be nice, but I also am not sure how to do it.