nonlinear PDE?

Stream: maths

[Uwe Brauer]

Hello, I am working in mathematicial analyis, hyperbolic non-linear PDE to be precise and therefore I have little knowledge of formal proof checkers. (More than 10 years ago I looked a bit into Isabelle but forgot almost everything). I learned about lean in an article about the successful confirmation of a proof of Peter Scholze. So I am curious, sometimes proofs for showing global existence for (classical) solutions of non-linear PDE can be quite sophisticated. Is there any project, any material, in lean trying to provide support for these sort of questions? What I have found so far only concerned, logic, set theory, etc but not really analysis. Can anybody enlighten me please. Regards Uwe Brauer

[Heather Macbeth]

Welcome! I work on nonlinear elliptic PDE (also known as differential geometry :) ). So I share many of your long-term hopes for formalization.

Lean (and other formal proof checkers) are a long way away from being able to do this. At the moment we are doing much more foundational work that heads in that direction -- for example, Remy Degenne contributed a theory of Lp spaces a few months ago, then last month I proved that continuous functions are dense in Lp. An expert user could probably write down a definition of Sobolev spaces now, but it would be a fair bit of work.

[Heather Macbeth]

Yury Kudryashov recently defined Holder spaces.

[Heather Macbeth]

He's also working on a version of Stokes' theorem -- unfortunately integration in several variables, though defined (thanks to work last year by Floris van Doorn), is a bit clunky to work with currently.

[Heather Macbeth]

I think the Gagliardo-Nirenberg-Sobolev inequality would be within reach, again for an expert user.

[Uwe Brauer]

Thanks for your reply. So the situation is as I expected (or feared ;) ). Could you provide any pointers to the work you mentioned? BTW, I am also dealing sometimes with differential geometry, however with a Lorentzian metric, so that some of the corresponding PDE are hyperbolic. regards

[Scott Morrison]

The definition of Lp spaces is at src#measure_theory.Lp.

[Scott Morrison]

Hölder continuity is at src#holder_with.

[Scott Morrison]

Heather's proof that continuous functions are dense in Lp is at src#measure_theory.Lp.bounded_continuous_function_dense.

[Uwe Brauer]

thanks

[Heather Macbeth]

We also have the beginnings of a differential geometry library, by the way (the work of Sebastien Gouezel). It too is in early stages, but here is Yury's recent proof of the Whitney embedding theorem:
src#exists_embedding_euclidean_of_compact