regularity structures placement in Mathlib?

Stream: mathlib4

[Thomas Kojar]

I like to start the formalizing for the topic of regularity structures (https://arxiv.org/abs/1303.5113). In particular, I will start with formalizing the reconstruction theorem "Hairer's Reconstruction Theorem without Regularity Structures" from https://arxiv.org/abs/2005.09287.

I followed the instructions of forking the Mathlib in my own github account. I was just wondering about the placement of this topic. It is about stochastic pdes and so it is a mixture of probability and analysis. Should I make a new folder called "Stochastic PDEs"? Should I work on it somewhere separately and then make a request here to upload?

I am not sure if this is the right channel to post this question, if not please let me know which one.

Thank you

[Kevin Buzzard]

Maybe it's best if you post some code here on zulip first and then ask for advice about where that specific code should go

[Thomas Kojar]

For example, the article https://arxiv.org/abs/2005.09287 uses convergence of nonsmoth mollifiers (Lemma 7.4 (Mollifiers).). That is a general classical result that falls slightly outside the bump functions results on Mathlib. So I am guessing, I would have to create a separate file for it that maybe goes under bump functions folder. Correct?

[David Ledvinka]

I will respond to both your questions here and in #mathlib4 > Regularity structures since they are related.

Firstly see the relevant thread #maths > Hairer challenge (of course Mathlib has progressed since then).

For a project of this scale I don't think it makes sense to try to develop it in mathlib directly. A good model to follow would be something like the brownian motion project found here. Note everything in that project is intended to end up in Mathlib but its easier to develop it separately and then port it to Mathlib (which can be a long drawn-out process).

I think the best first step for this project would be to develop a blueprint that splits the paper into digestable lemmas, definitions and theorems that reduce to mathlib definitions and theorems (and ideally also their proofs written out in detail that mathematicians with minimal expertise could follow). See for example the brownian motion blueprint with dependency graph. Also see PFR or Carleson Project for more examples.

I would definitely be interested in helping out with this project but unfortunately I am a bit busy at the moment to read/understand the paper in depth and help write the blueprint (perhaps in the near future if you don't complete it by then).

[Thomas Kojar]

I see thank you for the advice.

[Thomas Kojar]

I created the github project here: https://github.com/TKojar/Regularity_Structures_Lean

I also created the blueprint as described here https://github.com/PatrickMassot/leanblueprint

If anybody is interested to help, please direct message me here at Zulip or at kojartom@msu.edu.