elliptic PDEs

Stream: new members

[David Wiygul]

Hello, Leaners. I've been following mathlib developments from afar for years, and now I would like to get more actively involved. My day job is in geometric analysis, and I've recently been in contact with Ben Chow and Pietro Monticone about mathlib projects in this direction, but I am also very interested in the formalization of the theory of elliptic PDEs (independently of applications). Is it fair to say that enough of the prerequisites are in place that it is reasonable to be thinking about adding some of the standard material on elliptic PDE? Is any such work already underway? I would love to talk to anyone else with related interests and to help out if appropriate.

[Kenny Lau]

I don't think we have much PDE

[Yaël Dillies]

Please, Kenny, could you refrain from replying to topics you aren't knowledgeable about?

[Kenny Lau]

ok, sorry

[Kevin Buzzard]

In fact a lot happened behind the scenes recently in a private channel associated to the lean pde workshop a few weeks ago, including formalisation of a general pde, the heat and wave equations and some solutions etc.

[Moritz Doll]

We already have a lot of the functional analysis required for PDEs: docs#IsCoercive.continuousLinearEquivOfBilin is the Lax-Milgram theorem, we have the Gagliardo-Nirenberg-Sobolev inequality docs#MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_le we have Schwartz functions docs#SchwartzMap. Tempered distributions, Sobolev spaces on R^n, test functions, distributions, etc are all in pull requests

[Michael Rothgang]

To add to Moritz' list: Filippo Nuccio and I are working on Sobolev spaces in general (not just of Schwartz functions), i.e. using distributions.

[Michael Rothgang]

Optimistic estimate: in mathlib in March :fingers_crossed:

[Moritz Doll]

It will be fun proving that all of the definitions coincide when restricted appropriately :sweat_smile:

[Moritz Doll]

Can I ask what version you are doing? Localize and weak derivatives?

[Michael Rothgang]

Here's a quick sketch; I can write more in a few hours/this afternoon. (Let me know if you'd like me to!)

• define the derivative of a distribution (i.e. purely algebraically)
• add a predicate HasWeakDerivative for a function (similar to HasFDerivative etc.; true if the distribution induced by f' is the derivative of the distribution induced by f)
• define weakDeriv (I'd need to check if we had a better name alreabdy) of a function: 0 if not locally integrable; if f is locally integrable and the derivative of the distribution induced by f is regular, choose a locally integrable function inducing it

• define a predicate MemSobolev: one option was to define this on distributions first and then pull it back to functions. For W^{1,p} distributions, this would say MemLp and the weak derivative is in MemLp also.
  I don't remember the current plan for higher order; one option is MemLp f and MemSobolev k-1 p (f')

• We also want to define a Sobolev norm.

With all of this, make the definitions total - but be careful about junk values and your statements meaning what you want them to do.
I need to remember some details of our plan (current focus is reviewing the work on distributions), but that was some outline.

[Michael Rothgang]

So: yes, weak derivatives - but no localisation. (What do you mean with that?)

[Moritz Doll]

Ah ok. There are some versions where you localize first, you do have to do that if you want the Fourier definition on manifolds. I have seen this in books also for the weak derivative one, but I can't remember why you would need it (maybe to avoid using a specific measure?)
Maybe we should move this discussion to the maths stream?

[Moritz Doll]

Just as an fyi: I did prove integration by parts in higher dimensions, which is a rather stale PR that I could dig up for you. It had some issues, but maybe you would be interested in revisiting it instead of proving it again yourself

[David Wiygul]

Thank you all for your replies. It sounds like much of elliptic theory needs to wait until distributions and Sobolev spaces are in place, but not everything. In particular would it be reasonable to try to introduce various versions of the maximum principle and possibly Schauder estimates? On the functional-analytic side, does mathlib know about Fredholm operators between Banach spaces? From a design perspective, how important is it to aim for high generality from the start? For example, if I am interested in a result on scalar equations but it generalizes to systems, am I obligated to work with systems right away?

[Sébastien Gouëzel]

We don't have anything on Fredholm operators. This would be a very good topic for formalization, because I think we have all the necessary prerequisites.

As for generality, yes mathlib would aim for high generality, but trying to keep a reasonable stance because otherwise nothing gets done. For instance we won't develop elliptic regularity on the line separately from the general case. However, it wouldn't have to be the highest generality either -- I think a version for differential operators would be very welcome, we wouldn't need to go directly to pseudodifferential operators for instance.

As for your specific question between scalar and system equations, it depends on what you want to prove and if it makes a real difference or not. Often, you will find out that changing the target space doesn't make any difference. But if you want to rely on a maximum principle, say, which is naturally scalar-valued, then let's go for the scalar case.

[Moritz Doll]

Fredholm operators would be amazing and also a good project for starting to get into formalising. Abstract functional analysis tends to be quite a bit easier than anything that requires calculus or measure theory.

[Yongxi Lin (Aaron)]

I have spent some time thinking about formalizing the weak maximum principle of a general second order elliptic operator and I believe a necessary tool is Taylor's theorem in higher dimension (because you need this to show that the Hessian at an interior maximum is negative semi-definite), which is right now still missing in Mathlib and maybe @Moritz Doll will be interested in this.

[David Wiygul]

@Yan Yablonovskiy 🇺🇦 , I would be interested in helping with Fredholm theory, if there is any need.

It seems like maximum principles would have a very favorable applications-to-prerequisites ratio. @Yongxi Lin (Aaron) , is Taylor's theorem the main missing ingredient as far as you can see?

Thinking about Schauder estimates, does mathlib know about Hölder spaces over domains in Euclidean space?

[Yan Yablonovskiy 🇺🇦]

Yan Yablonovskiy 🇺🇦 , I would be interested in helping with Fredholm theory, if there is any need.

To clarify , it was more of a "would like to work on it" react, since it does seem to be a good beginner formalisation excercise. So I would be very more than happy to work with anyone on it :smiling_face:

[Moritz Doll]

It might be that Taylor with the integral remainder is easier to formalise in higher dimensions. I have never tried it because I was dreading the discussion that want to have it not for C^k, but something where the last derivative is only integrable (I.e., C^k-1 and k-1 derivative is absolutely continuous). I haven't checked whether everything is there, I think it is possible, but a somewhat serious amount of work.

[Moritz Doll]

Fredholm operators are definitely easier and I would be happy to help if anyone wants to do that. (It feels like a "I could do it on a weekend, so it should be good for someone new" project)

[Michael Rothgang]

Fredholm operators would be great to have! They're on my personal "I would like to get to it somebody, but this will not happen soon at all" list, i.e. I thought about it, would be happy to help if you're stuck or could probably review a mathlib PR.

[Michael Rothgang]

There has been some prior attempts, which you may find useful:

• I just found this branch https://github.com/leanprover-community/mathlib4/compare/master...fredholm, one year old (I haven't looked at it at all)
• two students in Bonn worked on it last year: https://github.com/fpvandoorn/LeanCourse24/compare/master...HermaeusMorea:LeanCourse24:master. Their code duplicates some results in mathlib (and is not mathlib-level yet), but could also provide inspiration.
• I also have a branch working on it: https://github.com/leanprover-community/mathlib4/compare/master...grunweg:MR-Fredholm-ops

[Michael Rothgang]

Some quick thoughts about them:

• you probably don't want to assume your domain or co-domain are Banach spaces --- so an assumption of a closed image will be necessary. (My branch omitted that for easy prototyping; for mathlib, you want to add it.)
• That said, for Fredholm operators between Banach spaces the closed-ness of the image already follows from the other two conditions. That's not completely trivial, but would also be a nice general lemma to add.
• There are many kinds of results that would be nice to have. Invariance of the Fredholm index under compact perturbations is one; the relation to semi-Fredholm operators and the formal adjoint another. Any of these would be great to have!

[Sébastien Gouëzel]

Michael Rothgang said:

• That said, for maps between Banach spaces the closed-ness of the image is automatic. That would also be a nice general lemma to add.

I'm not sure what you mean here. There are many continuous linear maps between Banach spaces whose image is not closed. Maybe you mean that if the image has finite codimension then it closed? (Which is true but not completely trivial if I remember correctly).

Note that for the more general class of semi-Fredholm operators you need to impose in any case that the image is closed. (I am not saying that we should go directly for semi-Fredholm instead of Fredholm, although it would be even more great!)

[Yan Yablonovskiy 🇺🇦]

I think it would make sense in terms of mathlib generality to go for semi-Fredholm

[Michael Rothgang]

I think mathlib should have both semi-Fredholm and Fredholm operators, and the relation between them.

[Michael Rothgang]

I'm not sure what you mean here. There are many continuous linear maps between Banach spaces whose image is not closed. Maybe you mean that if the image has finite codimension then it closed? (Which is true but not completely trivial if I remember correctly).

Let me be precise: for bounded linear operators between Banach spaces, having finite-dimensional kernel and finite-dimensional cokernel implies the image is closed, i.e. "Fredholm operators" in this setting could be defined without requiring the image to be closed.
We shouldn't require completeness for defining Fredholm operators, so the general definition needs to include the closed image condition.

[Kevin Buzzard]

Are you going to include the p-adic case? Serre once wrote a paper on it!

[Moritz Doll]

Moritz Doll said:

It might be that Taylor with the integral remainder is easier to formalise in higher dimensions. I have never tried it because I was dreading the discussion that want to have it not for C^k, but something where the last derivative is only integrable (I.e., C^k-1 and k-1 derivative is absolutely continuous). I haven't checked whether everything is there, I think it is possible, but a somewhat serious amount of work.

I actually started to write some code, approximately half of the proof is done (there are a lot of parts where one has to check differentiability or continuity which is highly annoying)

[Michael Rothgang]

That's #31176, right?

[Michael Rothgang]

Re: localisation
My goal is absolutely to also define, for e.g. an open set $U\subset\mathbb{R}^n$, Sobolev spaces of functions $U\to E$ (and even further, we also want domains with nice enough boundary). I will need vector bundle sections of Sobolev class myself, so localisation will absolutely come up eventually.

[Moritz Doll]

Can't even have my secret PRs :smile: it is not up to date, but yes.

[Michael Rothgang]

To keep a PR secret, you need to post about it a week or two after opening your dummy PR :grinning:

[Ruben Van de Velde]

If you want a secret pr, you should label it t-data :see_no_evil:

[Moritz Doll]

Michael Rothgang said:

That's #31176, right?

It is sorry-free and doesn't need Hahn-Banach (Lang uses it, which is completely unnecessary)

[David Wiygul]

@Yongxi Lin (Aaron) and @Moritz Doll , I see that mathlib has the multivariable chain rule and the single-variable Taylor's theorem (with little-o error estimate). Would it be mathlib-appropriate to derive the maximum principle by combining these, without first formalizing a higher-dimensional Taylor's theorem?

[Moritz Doll]

Sorry, I don't understand what you are proposing. Generally, if you find a slick proof that uses less machinery than the usual textbook ones, that is very much in scope.

[David Wiygul]

Sorry: I was too vague to be understandable, but your answer encouraged me to just try, and it seems to be working out. Briefly, what I meant was to prove the below lemma by applying the chain rule to g := fun t => f (a + t \smul v) to reduce to the one-dimensional case and then to use the mean value theorem (well, I had originally said the one-dimensional Taylor's theorem) to finish; maybe there is a more efficient way to exploit what's already in the library, but this seems to do the job. Next I want to work on the maximum principle itself (at least at an interior point to start), and when I get that done, I would like to ask for feedback, in case you or another expert has time to take a look. For now, I'm quite certain that the proof I've written of the below is a stylistic mess (so will not share it at this stage), but can I ask you if the statement looks alright? Is there a more mathlibby way to write it (or factor it); should it be more general?

example (h : IsLocalMin f a)
    (hf1 : ∀ᶠ x in nhds a, DifferentiableAt ℝ f x)
    (hf2 : DifferentiableAt ℝ (fderiv ℝ f) a) :
    ∀ v : E, (iteratedFDeriv ℝ 2 f a) ![v, v] ≥ 0

[Bennett Chow]

It will be great to have the weak maximum principle for both elliptic and parabolic second-order PDEs, say for $C^2$ functions. In practice, in Ricci flow, the parabolic maximum principle will be applied to smooth ($C^\infty$) functions on smooth manifolds, often compact, but sometimes noncompact. To address noncompactness, often cutoff functions are used, although in less common circumstances the Omori--Yau maximum principle is used https://www.sciencedirect.com/science/article/pii/S0022123685711548 . Once an elliptic maximum principle is proved, I assume that it will not be difficult to prove the parabolic analogue given by adding a $\partial/\partial t$ in front. Now, the elliptic maximum principle is simply the multivariable first and second derivative tests, where the second derivative test gives the nonpositivity of the Hessian at a maximum point (and the nonnegativity of the Hessian at a minimum point). For this one can reduce this to considering straight lines in $\mathbb{R}^n$ (and geodesics on Riemannian manifolds). So one does not need Taylor's theorem. After developing the scalar maximum principle for elliptic and parabolic equations, it will be useful for Ricci flow to develop the tensor maximum principle, see Section 9 of Hamilton's 3D 1982 paper: (https://projecteuclid.org/journals/journal-of-differential-geometry/volume-17/issue-2/Three-manifolds-with-positive-Ricci-curvature/10.4310/jdg/1214436922.full) (more generally the maximum principle for systems) of Hamilton (in Sections 3 and 4 of his 4-d 1986 paper https://projecteuclid.org/journals/journal-of-differential-geometry/volume-24/issue-2/Four-manifolds-with-positive-curvature-operator/10.4310/jdg/1214440433.pdf) [there is a precursor to this by Hans Weinberger https://memoriam.cse.umn.edu/hfw/Math/InvariantSets.pdf ]. That maximum principle is in the setting of symmetric covariant 2-tensors and more generally in terms of sections of Riemannian vector bundles, where the framework is in terms of fiber-wise convex sets that are invariant under parallel translation. The convexity is from the idea that the Laplacian operator averages things out, so given two points in the fiber-set, one wants the straight line segment between these two points to still be in the set. Assuming we develop the Riemannian geometry track in Lean, some applications are: (1) Elliptic application: [David Wiygul and I disucssed this] Give a proof of the Li--Yau lower bound for the first eigenvalue of the Laplacian on a closed Riemannian manifold with nonnegative Ricci curvature in terms of the diameter https://www.researchgate.net/publication/239222762_Estimates_of_eigenvalues_of_a_compact_Riemannian_manifold . (2) Parabolic application: Prove the standard lower estimate for the scalar curvature under Ricci flow. (3) A simpler parabolic application is a re-proof of the elementary fact that for a smooth solution to the linear heat equation $u_t = u_{xx}$ on the unit circle, we have the gradient estimate $|u_x| \leq C e^{-t}$. This is a special case of a much more general result that on a closed Riemannian manifold, $|\nabla u| \leq C e^{-\lambda_1 t}$, where $\lambda_1$ is the first eigenvalue of the Laplacian (this can be proved using eigenfunction expansions) (reference? maybe this is in one of Chavel's books). But for the circle, there is a cute proof using the parabolic maximum principle and in particular Aleksandrov reflection, which is a special case of what Bob Gulliver and I developed for extrinsic curvature flows of Euclidean hypersurfaces. Namely, consider the equation $v_t = v_{xx} + v$ and apply Aleksandrov reflection. This proof should be mentioned in my first paper with Bob in PDE Calc. Var. in the 90's https://link.springer.com/article/10.1007/BF01254346 . In general, the parabolic weak maximum principle is hugely important to Ricci flow and it would be great to develop it on manifolds. Expositions of the parabolic maximum principle, in the context of Ricci flow are given in some of my coauthored AMS books https://bookstore.ams.org/bennett-chow . In particular, an introductions is in Chapter 4 of my book with Dan Knopf (Mathematical Surveys and Monographs, Vol. 110) and some more advanced versions in Chapters 10 and 12 of the multi-authored book Mathematical Surveys and Monographs, Vol. 144, with various applications in all the books.