Regularity structures

Stream: mathlib4

[Thomas Kojar]

I like to start the formalizing for the topic of regularity structures (https://arxiv.org/abs/1303.5113). I think it might be doable because quite a few of the objects are defined axiomatically. I didn't see anything about this topic here in the chat, but has anybody started or attempted but failed for some reasons?

Anybody interested to help out?

Thank you

[Kexing Ying]

You might find the result from here useful if you are formalizing the reconstruction theorem.

[Thomas Kojar]

thank you @Kexing Ying .

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