First contribution: Primitives of holomorphic functions

Stream: mathlib4

[Stefan Kebekus]

Dear all,

I am looking for help contributing a piece of code to Mathlib: A formalization of the classic statement that holomorphic functions have primitives:

• https://git.cplx.vm.uni-freiburg.de/kebekus/nevanlinna/src/branch/main/Nevanlinna/holomorphic.primitive.lean

The relevant statement is 'theorem primitive_fderiv' at the bottom of the file. The statement, which is currently formulated for entire functions should clearly be generalized to functions that are holomorphic on metric balls.

As anyone can see, I am a beginner. I have never contributed anything to Mathlib, and I have no idea about mathematical standards, coding standards, or submission procedures. I also have a few questions about the API design. I would appreciate it if someone more experienced could have a look and push me in the right direction.

First questions:

• Code quality: The code compiles and proves the result, but surely needs improvement. With some effort, I can compactify the code from ~600 to ~500 lines (but I still need to add documentation). I wonder about the trade-off between readability and brevity.

• API design: I wonder how many of the intermediate statements should be private, and how many should be public.

• I use partial derivatives throughout the proof. Is it a good idea to isolate partial derivatives for future use? More generally, one could think about Lie derivatives and general differential operators -- but this is a substantial project by itself.

Best wishes,

Stefan.

[Ruben Van de Velde]

One suggestion I'd give already is that we require structuring proofs in a way that there is only one goal active at any point, by using cdots

[Damiano Testa]

Hi Stefan, it is very nice to see you here!

[Sébastien Gouëzel]

I'd like to mention that we already have a PR giving existence of primitives, in #9598. How does it relate to your approach?

[Stefan Kebekus]

Ruben Van de Velde schrieb:

One suggestion I'd give already is that we require structuring proofs in a way that there is only one goal active at any point, by using cdots

Understood, thanks.

[Stefan Kebekus]

Damiano Testa schrieb:

Hi Stefan, it is very nice to see you here!

Thanks! Hoping to meet you here more often...

[Stefan Kebekus]

Sébastien Gouëzel schrieb:

I'd like to mention that we already have a PR giving existence of primitives, in #9598. How does it relate to your approach?

It seems that AlexKontorovich does exactly what I am doing, so my contribution-to-be is obsolete. Thanks for pointing that out!

I wonder how I can proceed now.

• It seems that Alex's PR has been lying untouched since March. Is this normal or is it a sign that something has gone wrong?
• I am trying to write down the basic inequalities of Nevanlinna theory, and my next goal is to discuss elementary properties of harmonic functions [mean value property, relation to holomorphic functions, etc]. How should I continue to avoid writing more code that might then turn out to be obsolete?

Best,

Stefan.

[Johan Commelin]

@Yury G. Kudryashov Do you have time to look at the PR by Alex?

[Stefan Kebekus]

Sébastien Gouëzel schrieb:

I'd like to mention that we already have a PR giving existence of primitives, in #9598. How does it relate to your approach?

As a follow-up question, I wonder about mathlib standards when introducing new notions. For my project, I need to introduce the Laplace operator. On the complex plane, where Nevanlinna theory takes place, this is easy to write down. For general finite-dimensional vector spaces with scalar product, I fear this is not easy at all to write down … and I would like to avoid that for now...

Any help or advice is greatly appreciated.

Best, Stefan.

[Stefan Kebekus]

Johan Commelin schrieb:

Yury G. Kudryashov Do you have time to look at the PR by Alex?

I skimmed over the proof briefly. Do you have a minute for a video-chat?

[Vincent Beffara]

To prove the existence of primitives on a star-like domain it is easier to integrate along a ray than to use two sides of a rectangle, since you can avoid separating real and imaginary parts. I have a proof using this here: https://github.com/vbeffara/Curvint/blob/main/Curvint/Primitive.lean

[Vincent Beffara]

To do it on a ball, another approach would be to write the function as the sum of its Taylor series and define a primitive term by term (although, managing domains of convergence and such could be a bit cumbersome).

[Stefan Kebekus]

@Vincent Beffara Thank you for your helpful comment. I was already wondering if someone was doing curve integrals. Is any of this already available in mathlib?

Also, I understand that you are proving the Riemann mapping theorem? I am, of course, very interested. Is this already done and available?

[Vincent Beffara]

None of this is in mathlib yet ... I have a proof of the Riemann mapping theorem for connected domains in which any non-vanishing holomorphic function has a holomorphic square root, or equivalently on any domain where holomorphic functions have primitives, here https://github.com/vbeffara/RMT4

Of course the condition is the same as simply connected but that fact is missing. I didn't want to develop C1 contours too much because I believe C0 contour will work better eventually - but then to work with C0 contours you need something like path and homotopy lifting, which is something a few people (myself included) started but AFAIK is nowhere done in a satisfactory way.

[Kalle Kytölä]

@Vincent Beffara, we really want Riemann Mapping Theorem in Mathlib! Can I somehow provoke you into PRing small parts at a time? (At least I'll buy you a beer when you get RMT into Mathlib.) I don't see anything wrong with replacing the simply connectedness assumption in RMT by the assumption of existence of primitives while Mathlib does not have the existence of primitives in the desired form. It should be trivial to reconcile once the existence of primitives is resolved.

[Kalle Kytölä]

The primitives question is annoying, of course. I really hope it gets sorted out soon! (I was secretly hoping that the #PrimeNumberTheorem+ project would be a sufficient impetus...)

[Kalle Kytölä]

Also, I'm excited to hear that @Stefan Kebekus is interested in contributing to complex analysis!

[Stefan Kebekus]

@Vincent Beffara Thanks for your quick and helpful answer!

[Stefan Kebekus]

Kalle Kytölä schrieb:

Also, I'm excited to hear that Stefan Kebekus is interested in contributing to complex analysis!

Thank you for the welcome! Let's see if I can be of any use…

[Stefan Kebekus]

@Vincent Beffara @Kalle Kytölä @Sébastien Gouëzel Thanks for all your help. As a next step, I would like to formalize harmonic functions:

• Defining them on finite-dimensional inner-product spaces via the Laplacian
• Showing that (real parts of) (anti)holomorphic functions are harmonic
• Showing that harmonic functions on metric balls are real parts of holomorphic ones
• Characterize harmonic functions on $\mathbb C$ or $\mathbb R^2$ by their mean value properties
• Establish Jensen's inequality (<- which is what I am really heading for)

Are you aware of anyone doing this (…or having done that already)? Is there a group that I should join? Or someone I should be talking to?

As always: Thanks & Best wishes,

Stefan.

[Kalle Kytölä]

Regarding harmonicity theory in Mathlib, I wonder about two things:

Should one immediately aim to characterize weakly harmonic functions by a mean value property and to show that any weakly harmonic function is actually harmonic? Maybe the proof that mean value property implies harmonicity is necessarily quite close to working with distributions / distributional derivatives? I don't know what is the status of distributions and distributional derivatives in Mathlib, but I believe @Anatole Dedecker would know.

Does it make sense to develop a theory of subharmonic functions? One would then obtain harmonicity as: both $\pm u$ are subharmonic (i.e. $u$ is both sub- and superharmonic). This seems quite standard and unless I am mistaken, it might be essentially the same amount of work as harmonicity, but more general.

To be clear, the above are not meant as suggestions to divert from your project, which is extremely welcome! I am just wondering out loud in the hopes that thinking about these issues helps choose the best way to get analysis in Mathlib efficiently and in good generality.

[Stefan Kebekus]

Kalle Kytölä schrieb:

Regarding harmonicity theory in Mathlib, I wonder about two things:

Should one immediately aim to characterize weakly harmonic functions by a mean value property and to show that any weakly harmonic function is actually harmonic? Maybe the proof that mean value property implies harmonicity is necessarily quite close to working with distributions / distributional derivatives? I don't know what is the status of distributions and distributional derivatives in Mathlib, but I believe Anatole Dedecker would know.

Does it make sense to develop a theory of subharmonic functions? One would then obtain harmonicity as: both $\pm u$ are subharmonic (i.e. $u$ is both sub- and superharmonic). This seems quite standard and unless I am mistaken, it might be essentially the same amount of work as harmonicity, but more general.

To be clear, the above are not meant as suggestions to divert from your project, which is extremely welcome! I am just wondering out loud in the hopes that thinking about these issues helps choose the best way to get analysis in Mathlib efficiently and in good generality.

@Kalle Kytölä Message received. I understand what you are suggesting, and I can see why attraction to have this material in mathlib4. At the same time, I fear that these topica are out of scope for me -- I do not use these notions in my daily work or teaching, so I would probably not be a good person to implement that.

If someone else (e.g. you) is interested in implementing (weakly) (pluri)(sub)harmonic functions, I am of course quite open to joining forces!

Best,

Stefan.

[Kalle Kytölä]

I have a feeling that my message failed to convey what I genuinely meant, although I really tried to be explicit that I only wanted to share considerations and point out that for example Anatole's work on distributions may be relevant/helpful. (And the reason I wanted to share such thoughts is because I like the idea of having harmonicity in Mathlib.)

I think harmonicity theory would be very welcome! I don't know of anyone else who would be doing it at the moment, which makes any contribution there even more valuable.

I merely wanted to point out that planning about the right generality is worth some moments before the project. Generality is first of all valuable in the library (Sébastien's change of variables in integration is what in my dream world Mathlib's analysis would look like, but most realistic contributions cannot and will not look anything like that). Additionally, generality can even make things easier or at the very least least not harder. (For example my thought with vague recollections was that the only thing that differs in subharmonicity theory is that it is convenient to allow $+\infty$ as a value, but otherwise many arguments are merely modified by changing some equalities to inequalities. And my naive recollection is that for mean value property implies harmonicity one needs to mollify and I don't know how far that is from distributional arguments then. And in both cases something could be gained from connecting to the right parts of the existing library. Anyway, if I'm for example not right that subharmonicity is a small tweak, then it could be a relatively quick refactor afterwards. I may also just be wrong! I really only wanted to encourage considering these.)

Once more, I think harmonicity results would be extremely welcome. I hope you go on with the project! There are way too few analysis contributors in my opinion.

[Stefan Kebekus]

@Kalle Kytölä I have read and (hopefully!) understood your message. Thanks for taking the time to clarify your point. As a newcomer to the mathlib4 community, I value your explanation (and the highly welcoming spirit in this group). I intend to proceed with this project […and have submitted a few (trivial) PRs already].

Getting all this material into Mathlib4 seems a formidable task. I should begin defining the Laplacian coordinate-freely on finite-dimensional inner product spaces. Doing this cleanly requires some fundamental work, which will take me some time…