Projects

Stream: Lean for PDEs 2025

[Kevin Buzzard]

I think the projects suggested so far were

1) State the heat equation. Prove that that the standard convolution solution is a solution. Prove that this is the only solution.
2) Implerment the method of characteristics
3) State Navier-Stokes
4) Doob Lp inequality
5) Local martingales

I personally think that any project of the form "state something" is very hard for beginners. It's far easier for an expert to state the questions and then the beginners to try and prove it.

[Michael Rothgang]

(6) State the wave equation (using the abstract formalism from the talk, or by hand)

[Michael Rothgang]

(7) finite speed of propagation for the wave equation

[Kevin Buzzard]

Can you state (7)? I am concerned that many of these projects involve (and in some cases are nothing but) "state something"

[Michael Rothgang]

Once a PDE expert tells me what the statement is, I'm very happy to help with that part.

[Kevin Buzzard]

SLMath have shut off the Zoom feed BTW (so I'm going to sleep now and will stop bothering you!)

[Kevin Buzzard]

The system is a massive learning curve and it's very easy for us as experts to forget this. I'm wondering whether e.g. stating the canonical solution to the wave equation (given initial conditions) is something which should be done by Remy and then proving that it is a solution is perhaps more viable for the participants

[Kevin Buzzard]

This will no doubt involve things like differentiating under the integral etc, but without an expert stating the problem there's a risk that the problem gets stated incorrectly, making it much harder to solve

[Vasily Ilin]

Hi. I am trying to verify the solution to the heat equation -- project 1.

import Mathlib.Probability.Distributions.Gaussian.Real
open ProbabilityTheory

noncomputable
def f (t:ℝ) x := if ht : 0 < t then gaussianPDFReal 0 ⟨t, le_of_lt ht⟩ x else 0

lemma deriv_t {x : ℝ} (ht : t > 0) : deriv (fun t => f t x) t = (f t x) * (-1/t + x^2/t^2) := by
  unfold f
  simp [ht] -- does not simp under binder `deriv`

I have two questions:

1. Is this the right way to circumvent the fact that deriv expects a normed field but gaussianPDFReal takes a NNReal?
2. How to simp f under the binder deriv?

[David K. Zhang]

@Michael Rothgang Suppose u = u(x, t): ℝⁿ × ℝ → ℝ is C² and satisfies the wave equation ∂²u/∂t² = ∇²u.

Finite speed of propagation: If u(x, 0) = 0 and ∂u/∂t(x, 0) = 0 for all x ∈ ℝⁿ lying in the closed ball of radius r centered at x₀ ∈ ℝⁿ, then u(x, t) = 0 for all (x, t) ∈ ℝⁿ × ℝ satisfying 0 ≤ t ≤ r and ||x − x₀|| ≤ r − t.

The physical interpretation of this statement is that a disturbance in u at the point (x₁, t₁) can only affect u at (x₂, t₂) if t₂ − t₁ ≥ ||x₂ − x₁||, i.e., enough time has passed for the disturbance to travel from x₁ to x₂.

[David K. Zhang]

The usual proof of this statement, from Evans' textbook, is as follows:

Screenshot 2025-10-07 at 23.05.20.png

You can see it requires a notion of multidimensional integration (Riemann is fine since we are only integrating continuous functions here) that supports multiple domains (ball and sphere), differentiation under the integral sign, and a multidimensional fundamental theorem of calculus (divergence theorem, i.e., Stokes' theorem for (n-1)-forms).

[David K. Zhang]

Is machinery of this type available in mathlib? I can see that there is a form of divergence theorem present (https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/BoxIntegral/DivergenceTheorem.html) but it appears to only apply to box domains, with a nonstandard notion of integral?

To make the proof work, we had to ban tagged partitions with “long and thin” boxes. More precisely, we use the following generalization of one-dimensional Henstock-Kurzweil integral to functions defined on a box in ℝⁿ...

[David K. Zhang]

In particular, it is not clear to me whether this notion of integral is compatible with the notion defined in https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Calculus/ParametricIntegral.html for differentiation under an integral sign. Can any Mathlib experts weigh in here?

[Yongxi Lin (Aaron)]

Sadly we are missing a lot of things. We don't have the most general version of Stoke's theorem, but I know that some people is working on differential forms so hopefully we can have Stoke's theorem soon.

[Yongxi Lin (Aaron)]

The HK integral and the Bochner integral are also defined differently in mathlib and I don't think we have a theorem saying that these two are equivalent when we are working in ℝⁿ.

[Heather Macbeth]

There's no reason to use the HK integral though?

[Yongxi Lin (Aaron)]

Vasily Ilin said:

Hi. I am trying to verify the solution to the heat equation -- project 1.

import Mathlib.Probability.Distributions.Gaussian.Real
open ProbabilityTheory

noncomputable
def f (t:ℝ) x := if ht : 0 < t then gaussianPDFReal 0 ⟨t, le_of_lt ht⟩ x else 0

lemma deriv_t {x : ℝ} (ht : t > 0) : deriv (fun t => f t x) t = (f t x) * (-1/t + x^2/t^2) := by
  unfold f
  simp [ht] -- does not simp under binder `deriv`

I have two questions:

1. Is this the right way to circumvent the fact that deriv expects a normed field but gaussianPDFReal takes a NNReal?
2. How to simp f under the binder deriv?

I think an easier way to define f is to use toNNReal, although I am not sure whether this can make it easier to prove your lemma.

import Mathlib.Probability.Distributions.Gaussian.Real
open ProbabilityTheory NNReal Real

noncomputable
def f (t:ℝ) x := gaussianPDFReal 0 t.toNNReal x

[David K. Zhang]

@Yongxi Lin oof, that is really unfortunate. Without a developed theory of multivariate calculus in ℝⁿ we really cannot formalize much of PDE theory... We cannot even make it past the very first proof in Evans' PDE book (pg. 23) which uses all of these techniques (on a function with a singularity, no less).

[Yongxi Lin (Aaron)]

One reason we don't have it now is that we want the most general result in mathlib and certainly we want Stoke's theorem for a general class of functions and a general class of domains (e.g. manifolds with boundary, potentially with some corners?). But the general version is hard to formalize.

[David K. Zhang]

That makes sense, but in that case, it seems premature to hold a "Lean for PDEs" workshop when "Lean for Calculus III" is not yet a finished project. I suppose this is why, as @Kevin Buzzard observes, most of the projects are merely of the form "state something" rather than "prove something"?

[David K. Zhang]

To be fair, I am not a PDE expert -- I am primarily a numerical analyst with only a few PDE courses under my belt. But it is my impression that energy arguments of this type (involving integration) are essential to get PDE theory off the ground.

[David K. Zhang]

For example, in proposed project #1:

1) State the heat equation. Prove that that the standard convolution solution is a solution. Prove that this is the only solution.

Both techniques I know to prove uniqueness of solutions for the heat equation, the energy method and the maximum principle, use integration in an essential way.

[Yongxi Lin (Aaron)]

I would argue that some one-dimensional result for periodic heat/schrodinger equations are doable. We have results about Fourier series and integration by part over an interval: intervalIntegral.integral_deriv_mul_eq_sub_of_hasDerivAt.

[David K. Zhang]

Fair, but if (as you say) mathlib only wants theorems in general form, aren't such 1D restrictions throwaway practice projects with no hope of getting upstreamed into mathlib? The exploratory value also seems limited to me, since I doubt we will learn much about the necessary techniques to formalize the ND case from the 1D case.

[David K. Zhang]

Ah, I see the Fourier series results are indeed multivariate, so we might be able to do something for periodic functions over box domains. That seems potentially mathlib-worthy if we can synthetically work around multivariate integration, somehow...

[David K. Zhang]

Actually, I guess we could make progress by defining a purely formal "multivariate integration operator" that sends continuous functions on ℝⁿ to numbers in the right way (linearity, divergence theorem, preserves nonnegativity, etc.) and make all of our results conditional on the existence of such an operator, to leave an intentional gap that can be filled in when calculus on manifolds is sorted out at a later date (at least enough to get the results on ℝⁿ). Would that be an advisable way to proceed?

[Heather Macbeth]

David K. Zhang said:

Actually, I guess we could make progress by defining a purely formal "multivariate integration operator" that sends continuous functions on ℝⁿ to numbers in the right way

@David K. Zhang This doesn't seem necessary to me: there's a full theory of the Bochner integral, already well-used for multivariate integration, e.g https://arxiv.org/abs/2207.12742, https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.37.

The main gap I see for the early chapters of Evans is a version of Stokes' theorem for balls. It should be quite doable to state this using Hausdorff measure, and to prove it by a change of co-ordinates from the box version. I'd love to see someone work on this! As you note, just the statement (black-boxed) would be good enough to go on with.

[Heather Macbeth]

And maybe also a version of spherical co-ordinates: a measure-preserving map between punctured space $V\setminus\{0\}$ and the cylinder $\mathbb{R}^+\times S_0(V)$, where the cylinder is equipped with the measure $r^{\dim V-1}\mu_\mathbb{R}\times \mu_{S_0(V)}$ (where $\mu_{S_0(V)}$ denotes Hausdorff measure).

[Michael Rothgang]

@Vasily Ilin For your "simp under binders" question, the issue is actually slightly different. You have two functions (let's call them f and g), which are equal near t --- and you need to show that deriv f t = deriv g t. This does not only depend on the value at t, but on f and t in a neighbourhood of t. So, you need to apply a suitable lemma.

[Michael Rothgang]

If you hear "binder", really think of a forall or exists quantifier.

[Michael Rothgang]

Here's a start on how to do such a rewriting:

import Mathlib

open ProbabilityTheory

noncomputable
def f (t : ℝ) x := gaussianPDFReal 0 t.toNNReal x

lemma deriv_t {t x : ℝ} (ht : t > 0) : deriv (fun t ↦ f t x) t = (f t x) * (-1 / t + x^2 / t^2) := by
  unfold f gaussianPDFReal
  simp
  -- Idea: because t is positive, near `t` each `max t 0` is actually `t`, and we want to
  -- differentiate a simpler expression.
  -- This is the function we're differentiating now.
  set g1 := fun t ↦ (√(max t 0))⁻¹ * ((√Real.pi)⁻¹ * (√2)⁻¹) * Real.exp (-x ^ 2 / (2 * max t 0))
  -- This is the function we want to differentiate.
  let g := fun t ↦ (√t)⁻¹ * ((√Real.pi)⁻¹ * (√2)⁻¹) * Real.exp (-x ^ 2 / (2 * t))
  have hg (t) (ht : 0 < t) : g1 t = g t := by
    sorry -- exercise: prove this
  have hg' : g1 =ᶠ[nhds t] g := by
    sorry -- this is `hg` stated differently
  rw [Filter.EventuallyEq.deriv_eq hg']
  sorry

[Michael Rothgang]

Let me second what Heather says about Stokes' theorem: if you can state the version you want to use, you're allowed to black-box it and move on!

[Michael Rothgang]

(Differential forms are coming to mathlib, and we want Stokes's theorem for sure, e.g. deduced on manifolds with corners. But this will take in the order of a few months.)

[Luis Gabriel Bariuan]

Hi all, I am playing around with some differential equations from physics. I am currently trying to formalize a lemma where I am effectively taking a limit of a function to show that it tends to a particular function in the certain limit. Say we have k sinh(r/k). How would I go about showing k sinh(r/k) tends to r in the limit of k to infty? I am trying to search for a limit documentation in Mathlib, but I can't really find a reference. Thanks!

[Rémy Degenne]

The keyword for limits is Tendsto, as in Filter.Tendsto
I recommend reading the topology chapter of Mathematics in Lean to learn about that.

[Rémy Degenne]

This is how you write that a function tends to a limit at infinity:

import Mathlib
open Filter
open scoped Topology

example {f : ℝ → ℝ} {l : ℝ} : Tendsto f atTop (𝓝 l) := sorry

[Rémy Degenne]

The "at infinity" part is given by the Filter.atTop filter.

[Yao Liu]

Not knowing what has transpired at the workshop, nor an expert in PDEs (or Lean for that matter), I think the decision for formalizing PDEs would be torn by what generalizations we would want to eventually cover. The linear PDEs has a general theory (cf Hormander's treatise), heavily relying on the theory of distributions, while the nonlinear ones do not usually employ distributions (multiplication being undefined) but emphasize estimates/inequalities of various sorts (Evans' book seems to be of the latter kind). The wave equation is at the crossroad here, more so perhaps than the heat and Laplace's equations: the finite speed of propogation, for example, would be a statement of the support of the fundamental solution, and before that one would need existence and uniqueness. Given the style of abstraction in the rest of mathlib, it seems that distributions would be a natural object to formalize first.

[Michael Rothgang]

Distributions are being actively worked on right now: Moritz Doll is working on tempered distributions (and a number of these changes are open pull requests right now, waiting for review); Anatole Dedecker and Luigi Massacci have formalised distributions (and basic facts, such as a locally integrable function inducing a distribution). That work is also currently under review.

[Michael Rothgang]

Filippo Nuccio and I are formalising Sobolev spaces on top of Anatole and Luigi's work.

[Yao Liu]

That's wonderful. I'll take a look, and if I can find the time I may (finally) contribute something. One thing that I recall that I needed (for my work) was that the distributions supported at a point must be of the form of the delta function and (finitely many of) its derivatives. Do you have that already?

Out of curiosity, is the spectral theory (say the spectrum is discrete for the Laplacian on a compact domain) something that could come out of this push on PDE? One approach seems to involve the Sobolev space.

[Michael Rothgang]

I'm not sure if that's somewhere, waiting for review. @Luigi Massacci Do you have this? If not, is there a good branch of course that includes your work so far, that one could work on top of?

[Michael Rothgang]

I haven't thought about spectral theory so far (nor checked how much of it is in mathlib). If indeed missing, this would certainly be a worthwhile yet.

[Yongxi Lin (Aaron)]

Let me mention this post over here #mathlib4 > Tychonov's Counterexample for the Heat Equation as I think some PDE people may be interested in this.