Harmonic functions and the Laplacian

Stream: mathlib4

[Stefan Kebekus]

Dear all,

I am interested in implementing harmonic functions and the Laplacian, with the goal to eventually prove the most elementary statements of Nevanlinna theory. I am writing to ask if anyone is working on this, or interested in joining forces.

If no-one yells at me, my plan is to proceed as follows.

• Define the Laplacian for maps from finite-dimensional real inner product spaces to real vector spaces. [Mostly done]
• Prove that the Laplacian can be computed by differentiation wrt to arbitrary orthonormal bases. [Mostly done]
• Provide the usual API (Laplacian depends on germs, is linear on smooth functions, respects isometries, ...)
• Define Harmonic. For functions on the complex plane, establish the relation between harmonic and (anti-)holomrohpic functions. [Partially done, depends on existence of primitives for holomorphic functios that are in PR review]
• Move on to mean value properties.
• ...

Ideally, I would like to submit partial results/theorems/proofs to mathlib as soon as I have them, Does that make sense?

Best,

Stefan.

[Junyan Xu]

@Geoffrey Irving did (sub)harmonic functions (see here), but maybe for special models rather than an arbitrary inner product space. There is docs#gradient defined for inner product spaces, but I'm not sure how we should spell divergence.

[Geoffrey Irving]

Yes, I have harmonic and subharmonic functions, but only in one complex dimension. I don’t expect it’s upstreamable to mathlib without generalization.

https://github.com/girving/ray/blob/main/Ray/Hartogs/Subharmonic.lean

[Stefan Kebekus]

@Geoffrey Irving Thank you for the info. I am a beginner in this community, but what you have done seems like a very valuable contribution to me, that many [including myself] would like to have…

[Stefan Kebekus]

@Junyan Xu Maybe divergence is not even necessary. If $E$ is a finite-dimensional inner product space, and $v_i$ is a basis, then $\Delta f = \sum_i \frac{\partial^2}{\partial v_i^2} f$ is independent of the choice of basis. The reason is that $\sum_i v_i \otimes v_i$ is canonical, namely the image of the scalar product under the identification $E \otimes E$ with $(E \otimes E)^*$.

[Junyan Xu]

Yeah, I believe that. But since we already have gradient well-defined for an inner-product space, the task left is just to show divergence is well-defined for an inner-product space as well, and then we can compose them. Not to say that a direct approach is worse in any way.

[Johan Commelin]

@Stefan Kebekus For some reason Zulip wants you to write $$v \otimes w$$ in order to get $v \otimes w$...

[Stefan Kebekus]

Johan Commelin schrieb:

Stefan Kebekus For some reason Zulip wants you to write $$v \otimes w$$ in order to get $v \otimes w$...

Roger. Thanks.

[Stefan Kebekus]

Junyan Xu schrieb:

Yeah, I believe that. But since we already have gradient well-defined for an inner-product space, the task left is just to show divergence is well-defined for an inner-product space as well, and then we can compose them. Not to say that a direct approach is worse in any way.

Roger. I plan to come back to this as I get there.