Laplacian

Stream: Is there code for X?

[Sanjay Verma]

Hey all, I'm pretty new to lean and I am trying to generate some proofs about PDEs by using the sorry tactic for basic assumptions and then working with those. I was wondering if anyone had created any way to express Laplacian in n-dimensions?

[Yury G. Kudryashov]

What exactly do you want? Laplacian of a function from docs#EuclideanSpace? From a general finite dimensional inner product space? Something else?

[Yury G. Kudryashov]

In first case, you can take the usual sum of second derivatives.

[Sanjay Verma]

Yury G. Kudryashov said:

In first case, you can take the usual sum of second derivatives.

Thank you for the response! I meant from EuclideanSpace; sorry would you mind writing down how you would express the usual sum of second derivatives in two dimensions or is there somewhere I can check mine against

[Yury G. Kudryashov]

Something like this:

import Mathlib.Analysis.Calculus.LineDeriv.Basic
import Mathlib.Analysis.InnerProductSpace.PiL2

open scoped BigOperators

noncomputable def laplacian {n : Type*} [Fintype n] [DecidableEq n]
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (f : EuclideanSpace ℝ n → E) (x : EuclideanSpace ℝ n) : E :=
  ∑ i, lineDeriv ℝ (lineDeriv ℝ f · (EuclideanSpace.single i 1)) x (EuclideanSpace.single i 1)

[Yury G. Kudryashov]

Note that this won't apply to, e.g., WithLp 2 (Real × Real)

[Yury G. Kudryashov]

Or like this:

import Mathlib.Analysis.Calculus.ContDiff.Basic
import Mathlib.Analysis.InnerProductSpace.PiL2

open scoped BigOperators

noncomputable def laplacian {n : Type*} [Fintype n] [DecidableEq n]
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (f : EuclideanSpace ℝ n → E) (x : EuclideanSpace ℝ n) : E :=
  ∑ i, iteratedFDeriv ℝ 2 f x fun _ ↦ EuclideanSpace.single i 1

[Yury G. Kudryashov]

For nice functions these definitions are equal.

[Yury G. Kudryashov]

For a general inner product space, you probably want to define the "trace" (or what's the right name?) of a quadratic form (represented as docs#ContinuousMultilinearMap), then apply it to iteratedFDeriv Real 2 f x

[Kevin Buzzard]

I know very little about differential equations but perhaps it's true that on a finite dimensional normed real vector space there's an intrinsic notion of the Laplacian which is independent of choice of orthonormal coordinate system. If I'm not talking nonsense, how would one state this? For the proof, first I guess you define it for R^n like above, and then for a general space you can choose an isomorphism with R^n, pull back the definition, and then prove it's independent of the pullback. Do we have all the tools necessary to do this? Apologies if I'm talking nonsense, I just have this vague idea that the Laplacian is intrinsic in some way.

[Eric Wieser]

Elsewhere we handle this kind of thing by working with Trunc (Basis ..), where the quotient forces us to prove invariance immediately

[Eric Wieser]

Then you use choice to actually pick an arbitrary basis to put in the Trunc

[Kevin Buzzard]

Or Squash...

[Yury G. Kudryashov]

Indeed, Laplacian (with 2nd definition) is invariant under orthogonal coordinate changes, so the Mathlib way to define it is to

• define it for a basis and a bilinear form as the trace of the corresponding matrix;
• show that it's invariant under orthogonal changes of coordinates;
• define laplacian f as the laplacian of iteratedFDeriv Real f x w.r.t. to some orthogonormal basis (using Trunc, Squash, or Classical.choice).

[Sanjay Verma]

So this is what I have for the next step in my proof but I'm getting error with trying to assign n as a Natural number and with the norm. I'm not quite sure what I am doing wrong. Any input is appreciated.

import Mathlib.Analysis.Calculus.LineDeriv.Basic
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Analysis.SpecialFunctions.Pow.Deriv

open scoped BigOperators

noncomputable def laplacian {n : Type*} [Fintype n] [DecidableEq n]
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (f : EuclideanSpace ℝ n → E) (x : EuclideanSpace ℝ n) : E :=
  ∑ i, lineDeriv ℝ (lineDeriv ℝ f · (EuclideanSpace.single i 1)) x (EuclideanSpace.single I 1)

noncomputable def fundamental_solution (n : ℕ) (x : EuclideanSpace ℝ n) : ℝ :=
  if h : n ≥ 3 then
    let ω_n := 2 * real.pi^(n / 2) / real.gamma (n / 2)
    1 / ((n - 2) * ω_n * ∥x∥^(n - 2))
  else 0

[Yury G. Kudryashov]

It's EuclideanSpace Real (Fin n)

[Eric Wieser]

I've created #22861 with @Yury G. Kudryashov's first step above

[Yury G. Kudryashov]

I see that there are (at least) 2 competing approaches. I have no preferences. Please tell me when you decide which one you're going to use.

[A.]

How about this?

We define the Laplace operator on a Riemannian manifold $M$, with metric $g_{jk}$, in a way that naturally generalizes the characterizations of the Laplace operator on Euclidean space, given by (1.49), (1.62), and (1.63). Taking (1.62) as fundamental, we define the Laplace operator $\Delta$ on $M$ to be the second-order differential operator satisfying

$$-(\Delta u,v)=(du,dv)=(\textrm{grad }u, \textrm{grad }v)$$

for $u,v\in C_{0}^{\infty}(M)$.

p. 153 Taylor Partial Differential Equations I

[Eric Wieser]

That doesn't look like a definition to me, but a characterization

[Eric Wieser]

Independently of whether we want to define the laplacian via BilinForm.trace; is BilinForm.trace useful / correct in its own right?

[Kevin Buzzard]

Eric Wieser said:

That doesn't look like a definition to me, but a characterization

yeah that's IsLaplacian : Prop

[A.]

Eric Wieser said:

That doesn't look like a definition to me, but a characterization

Well I'm sorry about that but it is more general.

[Kevin Buzzard]

No, it's just different. For example it doesn't rule out the possibility that no such differential operator exists. You may need both things, the construction and the characterisation, in order to make a robust API (see for example docs#Localization and docs#IsLocalization, or docs#TensorProduct and docs#IsTensorProduct etc etc).

[A.]

Kevin Buzzard said:

No, it's just different. For example it doesn't rule out the possibility that no such differential operator exists...

This is to explain why Taylor's setup with manifolds is not more general? I'm confused.

[Eric Wieser]

Kevin is pointing out that a characterization and a definition are very different things, rather than commenting on any specific characterization or definition

[A.]

I’ll follow those links to see if they enlighten me as to the difference. I do see that where one has a constructive proof of existence it’s nice to use that in the definition, but presumably that’s not always the case?

[Kevin Buzzard]

It depends on whether you want to say "for all differential operators which satisfy the axiom defining the Laplacian, ..." or whether you want to apply the actual Laplacian to something. Here you don't need IsLaplacian because all Laplacians are equal in lean (in contrast to localisations, which are only isomorphic). So your characterisation falls short of what would be needed -- you still need to write down a definition.

[Jz Pan]

But what if there is no constructive proof of existence? This will force us to define IsLaplacian : Prop first, prove that Nonempty ..., and the definition of laplacian have to be Classical.choice ....

[Johan Commelin]

Sure. This discussion is orthogonal to the question of being constructive (which at least Kevin doesn't care about at all).

[Johan Commelin]

If you say: "I define FooBar to be the Wombat y that satisfies x < y + z", then you need to

• realize that the word "the" in "the Wombat" is doing some heavy lifting
• certainly you need to show that such a y exists... because maybe {y : Wombat | x < y + z} is empty!
• preferably show that y is unique, otherwise "the Wombat" is a bit misleading

[A.]

Johan Commelin said:

Sure. This discussion is orthogonal to the question of being constructive (which at least Kevin doesn't care about at all).

I brought up constructiveness so if, as it seems, the purpose of this discussion is to educate @A. then it is relevant.

[A.]

To be clear, I never wished to claim that the snippet I copied contains all the maths required. There are many pages in that book both before and after, and two subsequent volumes.

[Bennett Chow]

Does it make sense to first define the Laplacian acting on $C^2$ functions on a Riemannian manifold $(M^n,g)$? Assuming that we can define tensor fields on manifolds, Levi-Civita connection, covariant differentiation of tensors, and curvatures --- Riemann, Ricci, and scalar --- one of the first things in Ricci flow could be to derive the heat-type equation for the scalar curvature $\partial_t R = \Delta R + 2|\mathrm{Ric}|^2$. Just a thought for a future direction for stuff related to the Laplacian on manifolds from the geometric flows point of view.

[Michael Rothgang]

We have docs#InnerProductSpace.laplacianWithin and docs#InnerProductSpace.laplacian now. We almost surely don't have the Laplacian on a Riemannian manifold yet.

[Antoine Chambert-Loir]

In the context of Taylor's book, the given characterization also gives a definition, once you can take all possible $v$. But it would probably be easier here to split the definition into the definition of the two differential operators div and grad. The first one maps a $\mathcal C^n$-function $u$ to a $\mathcal C^{n-1}$-vector field and is defined by taking the differential of $u$ and using the Riemann tensor to convert it to a vector field. The second one maps a $\mathcal C^m$-vector field to a function, and passes via the Lie derivative of the canonical volume form.

[Antoine Chambert-Loir]

Even if one works on the standard $\mathbf R^n$, maybe with a (nonconstant) Riemannian metric, @Heather Macbeth keeps telling me that for mathlib, it will be valuable to do PDE in a coordinate free way.

[Moritz Doll]

I would think that the Laplacian on forms should be the main definition (for functions one term vanishes and the other one is exactly div grad). Obviously geometric differential operators should be defined invariantly, but I am sceptical that we will avoid coordinates completely (or some way of decomposing parts of manifolds that is basically identical to using local coordinates)

[Moritz Doll]

The more crucial question is what is the correct domain. While C^2 looks reasonable, it is bad from both a functional analysis point of view and also if you care about regularity theory. The most general domain would be distributions, and if you want to solve constant coefficient PDEs and not do partitions of unity, then tempered distributions is the right choice.
I don't know what the state of $C_c^\infty$ distributions is, but tempered distributions is a (wip) PR and I am working on getting all the fancy things to prove regularity for $\Delta u = f$

[Filippo A. E. Nuccio]

@Anatole Dedecker might have something to say about distributions

[Michael Rothgang]

My understanding is that the definition of $C^\infty_c$ distributions is done (by Anatole and @Luigi Massacci, and will be PRed to mathlib very soon).

[Luigi Massacci]

Yes, pinky promise you'll have like 18 PRs to review by Monday. I'm nearly done splitting up the code in manageable bits and adding all the various docstrings, etc

[Antoine Chambert-Loir]

About the domain, I don't exactly agree, or I would say that the question of the naïve laplacian (on $\mathcal C^2$) functions is an existing object that is not exactly defined by its version on $\mathcal C^\infty$-functions, nor by its version on the Sobolev space $W^{1,2}$, nor by its version on distributions. Moreover, the functional analysis point of view has to take into account the subtle question of the closure of those naïve operators (defined on a dense) subspace. So to summary, the definition of the naïve operators will be a prerequisite for all these interesting works.

[Anatole Dedecker]

I agree with Antoine: we will need the $\mathcal{C}^2 \to \mathcal{C}^0$ laplacian in any case, so one might as well start here.

[Anatole Dedecker]

I actually think that we will be able to define the Laplacian on distributions without talking about coordinates. The plan is to define F-valued distributions as the continuous linear maps from scalar-valued test-functions to F (this way, the Schwartz kernel theorem says that you can curryfy distributions). Then, one can define the differential of an F-valued distribution on (an open subset of) E (finite dimensional) as a E →L[𝕜] F-valued distribution. Iterating this process and taking the trace with respect to an inner product on E (this has yet to be defined I think), one gets the Laplacian.

[Moritz Doll]

I would think that you can just define a transpose operator that takes a bounded linear map on test functions and spits out a bounded linear map on distributions, that should be practically the same as what you described, but makes all of the proofs trivial. This is what I did for tempered distributions and it works very well.

[Moritz Doll]

The PR for tempered distributions is mathlib4#29819 (very wip, but the main step in how to define distributions is there)

[Anatole Dedecker]

Of course you can just define the distributional laplacians as the transpose of the one acting on test functions :man_facepalming: For some reason it seemed way more natural to me to define it in terms of the differentiation operator on distributions.
I guess one thing is that my approach would yield the fact that the distributional laplacian coincides with the usual one immediately from the corresponding fact on differentiation, while with your approach it requires proving before that the Laplacian is formally self adjoint, but none of this is very hard.

[Anatole Dedecker]

Moritz Doll said:

I would think that you can just define a transpose operator that takes a bounded linear map on test functions and spits out a bounded linear map on distributions, that should be practically the same as what you described, but makes all of the proofs trivial. This is what I did for tempered distributions and it works very well.

Yes, of course the idea is to use docs#ContinuousLinearMap.precomp as much as possible! Note that for the (coordinate free, but vector-valued) differentiation of distributions, one needs a very slight extra argument because the target space changes, but this is still essentially trivial

[Moritz Doll]

Ah cool, I didn't know that precomp exists without normed spaces. I agree all of these approaches are essentially equivalent and I can't imagine one is significantly better than another.

[A.]

Antoine Chambert-Loir said:

In the context of Taylor's book, the given characterization also gives a definition, once you can take all possible $v$.

Thanks for saying so. I thought I was going mad when everyone piled in to tell me otherwise.