Local expansions of holomorphic functions

Stream: Is there code for X?

[Yourong Zang]

Hello, I am an undergraduate student at Imperial who's doing a UROP this summer, supervised by Prof. Kevin Buzzard. I am currently working on some constructions and elementary properties of Riemann surfaces and holomorphic maps on them (my (very rough and might be incorrect) code is available here https://github.com/justadzr/Lean_2021). I made a few assumptions in my project. The most important ones would probably be the smoothness and analyticity of holomorphic functions on the complex plane. Prof. Buzzard suggested that I should post on Zulip and see if anyone has some version of it.

I saw from https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/holomorphic.20functions.20on.20the.20upper.20half.20plane and https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Stokes'.20theorem/near/225379719 that Cauchy's integral formula is technically done. I was wondering if anyone has integrated these two results and produced some form of the local expansion of holomorphic functions?

Thanks in advance.

[Heather Macbeth]

Just one remark, you don't need to define a new groupoid. Instead you can use docs#times_cont_diff_groupoid with the scalar field ℂ and with the model space docs#model_with_corners_self, i.e., 𝓘(ℂ, ℂ).

[Heather Macbeth]

And holomorphic maps likewise exist, as docs#times_cont_diff for this groupoid.

[Heather Macbeth]

The very important result that analytic = complex-differentiable is still missing (the status is basically the same as in the conversations you linked), but you don't need the manifolds formalism for that -- it's a purely local result (i.e., "would live in the analysis folder").

[Heather Macbeth]

One definition I would love to see is the conformal groupoid, which should be defined for arbitrary dimension.

[Heather Macbeth]

You could prove that docs#sphere is not just a smooth manifold but a conformal manifold.

[Heather Macbeth]

And you could prove that holomorphic implies conformal (both the local version and the fancy groupoid version) -- this is basically the Cauchy-Riemann equations, I have a stub for this which you could adopt.

[Heather Macbeth]

branch#complex-diff

[Yourong Zang]

Heather Macbeth said:

Just one remark, you don't need to define a new groupoid. Instead you can use docs#times_cont_diff_groupoid with the scalar field ℂ and with the model space docs#model_with_corners_self, i.e., 𝓘(ℂ, ℂ).

I have made a lemma that makes Riemann surfaces into smooth_manifolds with the trivial model space. But I think most complex analysis results later would be stated for differentiable_on ℂ. Is it still better to do this with times_cont_diff_groupoid?

[Yourong Zang]

Heather Macbeth said:

And you could prove that holomorphic implies conformal (both the local version and the fancy groupoid version) -- this is basically the Cauchy-Riemann equations, I have a stub for this which you could adopt.

The APIs in your branch are wonderful, especially for computing Jacobians. But do we have the definitions of conformal functions in mathlib?

[Heather Macbeth]

Yourong Zang said:

I have made a lemma that makes Riemann surfaces into smooth_manifolds with the trivial model space. But I think most complex analysis results later would be stated for differentiable_on ℂ. Is it still better to do this with times_cont_diff_groupoid?

In the long term (when all the results on equivalence between the various notions have been added to the library), I'm not sure whether it's better to use the weakest possible groupoid (which would be the differentiable_on one you define), the strongest possible groupoid (which would be based on docs#analytic functions -- I'm not sure if the corresponding groupoid exists in mathlib yet), or something in between. @Sebastien Gouezel might have an opinion.

[Heather Macbeth]

I would guess that the best choice of base notion would be one that allows you to share the maximum of material from other parts of mathematics, so either docs#times_cont_diff (which lets you share with real differential geometry) or docs#analytic (which is the best notion for hooking into complex algebraic geometry).

[Heather Macbeth]

Yourong Zang said:

But do we have the definitions of conformal functions in mathlib?

No, this would need to be defined (in general dimension, probably in the context of docs#inner_product_space).

[Heather Macbeth]

And a nice result to have (which is fairly elementary -- maybe in reach of current mathlib tools?) would be the classification of conformal functions in dimension $n\geq 3$, this is one of the many Liouville theorems
https://en.wikipedia.org/wiki/Liouville%27s_theorem_(conformal_mappings)

[Yourong Zang]

Heather Macbeth said:

Yourong Zang said:

But do we have the definitions of conformal functions in mathlib?

No, this would need to be defined (in general dimension, probably in the context of docs#inner_product_space).

Thank you for the remarks.

[Sebastien Gouezel]

Heather Macbeth said:

In the long term (when all the results on equivalence between the various notions have been added to the library), I'm not sure whether it's better to use the weakest possible groupoid (which would be the differentiable_on one you define), the strongest possible groupoid (which would be based on docs#analytic functions -- I'm not sure if the corresponding groupoid exists in mathlib yet), or something in between. Sebastien Gouezel might have an opinion.

I would probably use the strongest possible groupoid (so, the analytic groupoid), to make sure that all results for general analytic functions and for general smooth functions are readily available. Of course, this means that showing that a manifold satisfies these assumptions will be slightly more complicated (because you will have to check that the change of coordinates are analytic, and not merely differentiable) -- but once we have the theorem saying that complex-differentiable functions are analytic, it will just be one apply more.

[Kalle Kytölä]

Heather Macbeth said:

The very important result that analytic = complex-differentiable is still missing (the status is basically the same as in the conversations you linked)

I've been somewhat haunted and obsessed by this comment recently... :ghost:

I (kind of) get it that some complex analysis "with pictures of path homotopies" is hard to formalize... But...

Could someone knowledgeable please summarize the current status of this? I can of course see what docs#complex contains (and if I squint hard, what it doesn't). But does someone e.g. have a branch that is not yet PR'd to mathlib?

Who have made attempts in this direction? And who have plans to work on complex analysis (in 2021, say)?

(Thanks in advance and sorry about begin obsessed! :grinning_face_with_smiling_eyes:)

[Kalle Kytölä]

And besides the (very important) question of who, I would love to know about the status of following specific pieces:

• Are both implications of holomorphic $\Leftrightarrow$ analytic missing?
  • The differentiability of a power series would not require a single contour integral; is there any other obstacle to $\Leftarrow$?
• About the (harder) direction holomorphic $\Rightarrow$ analytic, do we have any of
  • Goursat's lemma?
  • Existence of primitives of holomorphic functions in convex (or star-shaped) domains?
  • Cauchy's integral theorem (and not to confuse with Cauchy's integral formula, I mean the one saying $\oint_\gamma f(z) \, \mathrm{d}z = 0$ for $f$ holom. and $\gamma$ null-homotopic) say in a convex domain and $C^1$ path $\gamma$?
  • Cauchy's integral formula, e.g., for circles? (I'm guessing this one is missing, because Kevin recently asked about a very specific case for his talk to olympiad kids recently --- and if we had this, then hardly anything would be missing from Taylor series and the analyticity of holomorphic functions...)

I am sort of scared to even ask, but it would be great also to hear what has been the difficulty / reason this is not in mathlib? There is a lot more advanced stuff already. And this one is kind of important math... (and undergrad curriculum and what other reasons would we need to care about it...)

[Kalle Kytölä]

Or is it that in mathlib we don't want the "cheap" approach via Goursat's lemma, because Stokes will have to be proved anyway, so it is better to obtain Cauchy's integral formula theorem [EDIT: See, I can't get this right, that's why I needed to elaborate above.] as a corollary?

[Heather Macbeth]

Hi @Kalle Kytölä, I think the big current attempt is by @Yury G. Kudryashov, who has an un-PR'd branch doing Stokes' theorem (for box domains), with weak hypotheses which in particular are satisfied by a complex-differentiable function, not necessarily continuously differentiable. See docs#stokes-new.

[Heather Macbeth]

I hope we can get this work of Yury's in to mathlib, and it should imply quite a lot of things:

[Heather Macbeth]

Kalle Kytölä said:

• About the (harder) direction holomorphic $\Rightarrow$ analytic, do we have any of
  • Goursat's lemma?
  • Existence of primitives of holomorphic functions in convex (or star-shaped) domains?
  • Cauchy's integral theorem (and not to confuse with Cauchy's integral formula, I mean the one saying $\oint_\gamma f(z) \, \mathrm{d}z = 0$ for $f$ holom. and $\gamma$ null-homotopic) say in a convex domain and $C^1$ path $\gamma$?
  • Cauchy's integral formula, e.g., for circles? (I'm guessing this one is missing, because Kevin asked about a very specific case for his talk to olympiad kids recently --- and if we had this, then hardly anything would be missing from Taylor series and the analyticity of holomorphic functions...)

Probably all this for example -- anything for a fixed domain (rectangles, discs, etc).

[Heather Macbeth]

As well as the fact that a uniform limit of holomorphic functions is holomorphic, which I find is one of the commonly-used "hammers" in complex analysis.

[Heather Macbeth]

Kalle Kytölä said:

* The differentiability of a power series would not require a single contour integral; is there any obstacle to $\Leftarrow$?

You're quite right, I think this is missing only for lack of someone getting round to it. We have the continuity of power series for example: docs#analytic_at.continuous_at. I think this is something an enthusiast could PR!

[Heather Macbeth]

For contour integrals, I think the difficulty is really topological, and/or combinatorial: what is the right generality (how should one even set up piecewise-differentiable functions nicely for example?). What does "simply-connected interior" mean -- maybe we should just wait until there's a theory of submanifolds-with-corners :dizzy:

[Heather Macbeth]

But I don't think that matters for applications, where rectangles and circles are probably enough almost all the time!

[Heather Macbeth]

Then, there is another missing piece: to go from the algebraic theory docs#mv_power_series to the docs#analytic_at theory. This would let one one define analytic functions (sine, exp, etc) efficiently from their power series, in very high generality (Banach algebras?). I don't know anything more except that there are subtleties; @Yury G. Kudryashov and @Sebastien Gouezel have thought about it.

[Heather Macbeth]

Oh also -- @Alex Kontorovich and I got started some time ago on a much less general approach, aiming at Goursat: branch#triangles if you're curious. But we stopped when Yury wrote the Stokes branch.

[Sebastien Gouezel]

I think @Yury G. Kudryashov was also working on the "easy" direction (i.e., that analytic functions are differentiable, and even infinitely differentiable). To do it properly (i.e., in any finite or infinite dimension) is not that easy, mainly for bookkeeping reasons: an analytic function around 0, say, can be written as $f (x) = \sum_n p_n(x, \dotsc, x)$ where $p_n$ is an $n$-multilinear function. For the $k$-th derivative of this, you will need in particular to write down the $k$-th derivative of an $n$-multilinear function, which is just painful to write and manipulate.

[Kevin Buzzard]

Is that because we don't have a good API because we didn't think hard enough about the problem, or do you think that there is some actual problem with doing this in DTT? Note that we have got around other hard problems by finding the right abstractions

[Sebastien Gouezel]

I think the math proof is just a notational mess. The $k$-th derivative of $x \mapsto p_n(x, \dotsc, x)$, applied to vectors $v_1,\dotsc, v_k$ is the sum of $p_n(w_1,\dotsc, w_n)$ where among the $w_i$, $n-k$ of them are $x$ and the other ones are the $v_j$ s (but in all possible orders). So, a sum over finsets of $\{1,...,n\}$ of cardinality $k$, and a sum over the permutations of $\{1, ..., k\}$. Nothing is hard, except writing it down precisely (which is never done in the books :-)

[David Wärn]

Isn't it enough to show that the first derivative exists and is also analytic?

[Kevin Buzzard]

So it looks like a sum over injections fin k -> fin n

[Kalle Kytölä]

Thank you Heather for a really helpful status report!

A small correction, in case others want to find out about the current status:
Heather Macbeth said:

... See docs#stokes-new.

...looks like a Freudian slip. I would also like so find this good stuff in the docs, but the correct link seems to still be branch#stokes-new :wink:.

[Kalle Kytölä]

The status report is very uplifting, and efficiently prevents the most severe symptoms of my obsession with the topic. Absolutely great that complex analysis is on its way to mathlib!