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.