Current work in (Dispersive) PDE

Stream: mathlib4

[Sahan Wijetunga]

Hi! @BHARGAVA KANAKAPURA and I are doing a reading course with @Terence Tao on dispersive PDE, and we are looking to formalize some related things. Has there been any work done in formalizing dispersive PDE (in mathlib, or elsewhere)? I saw mention of formalizing elliptic PDE here.

Also, there is a TODO to formalize the analytic case for picards theorem. Is anyone currently working on that? I don't see any open pull requests for it but just wanted to check.

[Patrick Massot]

I’m not aware of any such work, but it would be a great topic to work on at #announce > Techniques and Tools for the Formalization of Analysis @ 💬, I think you should apply.