differential equations

Stream: Is there code for X?

[Jukka Tuomela]

Hi,

I'm totally new to LEAN, just heard about it some months ago. I am curious if there is anything about differential equations? In some sense this could be difficult to formalize because differential equations and their solutions can be understood in many ways. ODE is often thought as a (smooth) vector field. On the other hand a PDE can be thought as a submanifold in jet spaces, or as a map between for example Banach spaces. Also solutions can be interpreted in many ways, for example as integral manifolds or elements in Sobolev spaces.

[Kevin Buzzard]

We have the fundamental theorem of calculus and we're working on a general form of Stokes' theorem but a general theory of differential equations is still missing (and high up on some people's wishlist). Algebra is much more developed, but I am not clear whether this is (a) because it's easier to do in Lean or (b) because there are more mathematicians with algebraic interests than analytic interests in this community (a lot of the media coverage is on the more algebraic parts of the theory, where Lean seems to be far ahead of anything the other provers have done).

[Patrick Massot]

It clearly becomes more and more embarrassing that we don't have Cauchy-Lipschitz in mathlib. But as Kevin wrote, this is not at all due to a technical or mathematical issue. Nobody prioritized it.

[Jukka Tuomela]

Perhaps algebra is more "well-defined"? To me the theory of PDE is mixture of algebraic (for example differential ideals), geometric (for example jet spaces) and analytic (for example Sobolev spaces) ideas.

Laurent Schwartz said that the reason why Bourbaki never considered PDE was that PDE require so many ideas from different parts of math that it didn't suit at all the style of Bourbaki.

[Oliver Nash]

Very interesting! I had no idea Schwartz (or any Bourbakian) had made such a remark. I agree that having so many dependencies makes it harder to formalise but if anything I think this makes a subject more worthy of formalisation.

[Oliver Nash]

I have no doubt we could do PDE theory if we wanted, and I expect we will in time.

[Patrick Massot]

I don't think it's true by modern standards that PDEs have a lot of dependencies.

[Patrick Massot]

The clash with Bourbaki rather comes from a lack of unified theory.

[Oliver Nash]

So it was more that the theory was too nascent?

[Kevin Buzzard]

Furthermore it matters less to our community that PDEs have a lot of dependencies because "just write a few more books" was hard for them, whereas "knock off a few more dependencies, developing just enough of the theory for it to be usable in PDEs" is a much more reasonable ask.

[Jukka Tuomela]

Cauchy-Lipschitz is really Banach fixed point theorem. Does that exist?

[Heather Macbeth]

@Jukka Tuomela Yes -- docs#contracting_with.fixed_point. Mathlib also has some of its other standard consequences, such as the inverse function theorem (docs#has_strict_fderiv_at.local_inverse) and implicit function theorem.

[Heather Macbeth]

By the way, existence and uniqueness for ODEs (Cauchy-Lipschitz as Patrick called it, or Picard-Lindelof as I have also heard it called) does exist in Isabelle, the work of Fabian Immler and Johannes Hölzl:
https://www.isa-afp.org/entries/Ordinary_Differential_Equations.html

[Heather Macbeth]

We would certainly be happy to have it in mathlib if you would like to work on it :). The classical Banach-space version is surely where one would start, but I think it would not be impossible (eventually ...) to get to the flow-of-a-vector-field-on-a-manifold version either -- for example, the tangent bundle has been defined, docs#tangent_bundle

[Heather Macbeth]

Of course, it would be even better to start heading to PDEs. There is a pretty satisfactory theory of Lp spaces in mathlib, thanks to recent work of @Rémy Degenne, so maybe Sobolev spaces would be the next step.

[Jukka Tuomela]

@Heather Macbeth Since Lindelöf was finnish, we of course call it also Picard-Lindelöf!

But what IS a differential equation? Surely one should define a type of differential equation before talking about Banach spaces? Note that in textbooks differential equations are not really seriously defined in general, see for example Evans, PDE, page 2.

I see some problems even on very elementary level. Consider x'=Ax+f; even in elementary applications one wants to allow discontinuous f or even Dirac's deltas. But then we have equality only in the sense of distributions (or otherwise weak inequality). But then what kind of operator is A? If we allow x to be a general (time dependent) distribution, then A is essentially multiplication by a smooth function which is not what we want.

Then if L is the laplacian then the fundamental solution is the solution of -Lu=delta, again with equality in the sense of distributions. But here the fundamental solution can be interpreted to be in many different spaces. So again one would need the concept/term/type of differential equation before introducing Banach (or other) spaces.

So we have the "formal unknown" u, and then "solution" u which is in some specific space.

Now I don't know if these speculations are at all relevant or interesting in the context of LEAN. I guess my point is that it would be interesting to see if it is possible to have a reasonable definition of differential equation. But as I said above I'm new to LEAN so I have no idea how to proceed concretely in this direction.

[Heather Macbeth]

@Jukka Tuomela For sure -- one general principle I have learned about formalizing is that the more abstract the point of view, the more elegantly the formalization works out. And in PDE theory as we know it there is a lack of abstraction -- or maybe there are many competing abstractions, none of which actually cover the full theory.

For now, we just try to develop the theories in some way, and build the usual "bridges" between different points of view explicitly, even if they are a bit clunky. But I hope that as we formalize more mathematics, we will actually find ourselves inventing some new abstractions, just as you say!

Maybe it would help to describe a concrete example of what it's like to do analysis in Lean at the moment, in particular the switching among different degrees of regularity, which as you point out is a constant feature of analysis arguments. In the file
https://github.com/leanprover-community/mathlib/blob/master/src/analysis/fourier.lean
I have done some of the basics of Fourier series. To prove that the span of $t \mapsto e^{int}$ is dense in $L^p$, I wanted to use the "shortcut" argument where you first invoke Stone-Weierstrass to get that it's dense in $C^0$, then apply the density of $C^0$ in $L^p$. So at different points in the argument I work with the bare function $t \mapsto e^{int}$, the same function packaged as an element of $C^0$, and the same function packaged as an element of $L^p$, and I have to explicitly invoke things like docs#continuous_map.to_Lp to go between the different points of view.

[Alistair Tucker]

I was vaguely thinking of doing something with an axiomatic approach (https://encyclopediaofmath.org/wiki/Potential_theory,_abstract). Would that be crazy?

[Jukka Tuomela]

@Heather Macbeth
What you call a bare function is perhaps close to what I meant by formal unknown. In the code you refer to I can in a way understand the statements (more or less) but of course the proofs are obscure to me...

Anyway the "bare function" could be perhaps thought as a section of jet bundle? One needs a kind of formal derivative up to arbitrary order. When one considers PDE systems the formal analysis is quite important (like the principal symbol, involutivity) , and in this analysis one doesn't even need to specify any space where the solutions should live.

[Patrick Massot]

No, what she calls a bare function is what you call a function. The other things are little packages containing a function and a proof of something (a proof of continuity in that case) or a element of $L^p$ (which is a quotient of a space of functions).