Multivariate complex analysis

Stream: maths

[Yury G. Kudryashov]

Hi, another project that I want to kickstart is multivariate complex analysis. I've started with #33381 going towards https://en.wikipedia.org/wiki/Hartogs%27s_theorem_on_separate_holomorphicity. Some parts of the proof can be borrowed from @Geoffrey Irving 's https://github.com/girving/ray. If you're going to work on this, then please coordinate here.

What other theorems should we formalize in this domain? Generalizations of some of theorems we have in dimension one, Hartogs's extension theorem, logarithmic convexity of the domain of convergence of a multivariate power series, Cauchy integral theorem in higher dimension, removal of compact singularities, other extension theorems, domain of holomorphy (equivalent conditions), what else?

[Yury G. Kudryashov]

Also, $\partial$ and $\bar\partial$ (required for lots of :up:)

[Patrick Massot]

Is there any specific reason why you want to start on higher dimensions before finishing the basics of dimension one? Or did I miss something and https://leanprover-community.github.io/undergrad_todo.html is outdated on single variable complex analysis?

[Alex Kontorovich]

For my ItaLean talk, I asked Claude where things stood with undergraduate (one-variable) complex analysis. Here are some things it said we didn't have yet:

• Cauchy-Riemann equations (really? That doesn't seem so hard?)
• Residue Theorem (we have a version for rectangles and simple poles in PNT+; would be easy to make a version for higher order poles)
• Weierstrass factorization (we now have a local version - Borel-Caratheodory)
• Riemann Mapping Theorem (@Vincent Beffara was very close to finishing this already two years ago; I'm not sure what happened to it? @Ian Jauslin and I outlined what I thought was the last needed ingredient: holomorphic functions on simply connected domains have primitives)
• Schwartz-Christoffel
• Picard's theorems
• Phragmen-Lindelof
• Rouché

[Patrick Massot]

I think everything is related to difficulties with contours. We have enough to get the main theoretical applications, but nothing that looks like handling “general” contours.

[Alex Kontorovich]

I'm largely convinced now from my PNT experience that we don't need general contours in "practical" applications. That said, is anyone even working on the dreaded Jordan curve theorem? How hard would it be to take the proof, formalized by Hales, and convert it to Lean? I know, I know, that's not the proof that "belongs" to Mathlib... (it's been like this for... 6 years?)

[Yury G. Kudryashov]

We have some versions of Phragmen-Lindelof. For most of the other missing stuff, I was waiting for someone else to formalize the required topological constructions, but possibly, I should just go forward and do it.

[Kevin Buzzard]

Alex Kontorovich said:

I'm largely convinced now from my PNT experience that we don't need general contours in "practical" applications. That said, is anyone even working on the dreaded Jordan curve theorem? How hard would it be to take the proof, formalized by Hales, and convert it to Lean? I know, I know, that's not the proof that "belongs" to Mathlib... (it's been like this for... 6 years?)

Heather told me that she was becoming pretty convinced of this claim, but what about the integral which Sidharth Hariharan wants to do for 8d sphere packing which is the contour in $\mathbb{C}$ which goes from $i$ down to $1$ clockwise along the unit circle, then up from $1$ to $1+i$ and then from $1+i$ to $i$ all in straight lines, and then actually just snip off the sharp end at 1 so you go from $1-\epsilon+\delta i$ to $1+\delta i$ instead. This I think was getting Heather to change her mind. We've found no way to work around this AFAIK (but I didn't talk to Sid about it since he left London for Pittsburgh so might be out of date)

[Yury G. Kudryashov]

I think that https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Integral/CurveIntegral/Poincare.html together with some topology (approximating paths and homotopies by smooth paths and homotopies) should give a version of Convex.exists_forall_hasDerivWithinAt with better assumptions.

[Yury G. Kudryashov]

The only reason I need convexity in that lemma is because I don't have smooth homotopies.

[Michael Rothgang]

The proper proof of the Jordan Curve theorem sounds like a great extended target for "get a group of experts together and bash it through" --- i.e., get the basics for singular homology over the line. This is blocking too many basic topology facts anyway.

[Michael Rothgang]

After that and Mayer-Vietoris (which follows by abstract non-sense also), proving the Jordan Curve theorem is not too difficult IIRC.

[Yury G. Kudryashov]

Do you want to write a blueprint?

[Geoffrey Irving]

This is all very exciting!

[Yury G. Kudryashov]

You've convinced me to fill in some 1-dimensional gaps first. Here is some progress towards Riemann mapping theorem (Complex.exp is a covering map): #33421 #33422 #33423 #33425

[Alex Kontorovich]

Yury, FYI John Morgan and I are (slowly) working through the "Covering Spaces Project" (started at the Simons meeting in June, for John to learn Lean). Of course you're welcome to scoop it; I'm sure John won't mind!...

[Yury G. Kudryashov]

Are you going to upstream anything soon?

[Yury G. Kudryashov]

I want to quickly go towards some big results (incl. Riemann mapping theorem) in a series of Mathlib PRs.

[Yury G. Kudryashov]

Why do you give your own definition for stuff that's already in Mathlib (e.g., Complex.exp)?

[Yury G. Kudryashov]

This makes upstreaming much harder.

[Yury G. Kudryashov]

Next: #33445. Here, I would appreciate a review from someone involved in writing algebraic topology for Mathlib. I've removed 1 layer of bundling and I've rewritten the proof.

[Yury G. Kudryashov]

In particular, I wonder what parts of the old proof can be deprecated immediately (all of it?)

[Alex Kontorovich]

Yury G. Kudryashov said:

Why do you give your own definition for stuff that's already in Mathlib (e.g., Complex.exp)?

This was mostly an exercise for John to learn about Lean/Mathlib. So he made up his own names, and the first bit of the project was to show how to connect his names to existing definitions/theorems in Mathlib. Again, go as quick as you'd like, don't worry about us. I was pointing to it in case the blueprint there may be of use to you...

[Michael Rothgang]

About the Riemann mapping theorem: have you seen https://github.com/vbeffara/RMT4? (There are PRs to bump it to 4.21, and I'm sure Ruben would be happy to bump it further.) If you have, great - I just want to avoid accidental duplicated work.

[Michael Rothgang]

Wait: are you talking about a different Riemann mapping theorem?

[Michael Rothgang]

Yury G. Kudryashov said:

Do you want to write a blueprint?

For Jordan Curve assuming Mayer-Vietoris? Sure, I can do that. (Basically, copy three pages from Bredon's textbook and flesh them out.) Will we have Mayer-Vietoris for topological spaces, though?

[Ruben Van de Velde]

Yeah, if anyone wants to pick up anything from it, I can bump it quickly

[Sébastien Gouëzel]

For Jordan curve, do you know the following version? Take two compact subsets K_1 and K_2 of R^n which are homeomorphic. Then R^n \ K_1 and R^n \ K_2 have the same number of connected components. It's less than one page once you have singular homology (or any homology, for what it's worth), and useful notably for spheres and for balls. Instead of doing something specific to spheres (or circles in dimension 2), I'd say it's worth going directly for this general version because it's not harder. And it's much more surprising: take two far away circles in the plane, or two circles one inside the other: then the complements are really different (two disks and a twice-punctured plane for the first one -- a disk, an annulus and a once-punctured plane for the second one) but they indeed have the same number of connected components.

[Sébastien Gouëzel]

(Sketch of proof: there is a homeomorphism of R^(2n) sending K_1 \times {0} to {0} \times K_2, so R^(2n)\K_1 and R^(2n)\K_2 are homeomorphic. Then relate the homology of R^n\K_1 to that of R^(n+1)\K_1 by Mayer-Vietoris applied to K_1 x [0,+\infty) and K_1x (-\infty, 0]. Inductively, relate the homology of R^n\K_1 to that of R^(n+i)\K_1. For i=n, since R^(2n)\K_1 and R^(2n)\K_2 are homeomorphic, they have the same homologies. Then R^n\K_1 and R^n\K_2 also have the same homologies)

[Snir Broshi]

Can invariance of domain (#33018) also fit here, or is it unrelated to singular homology?

[Sébastien Gouëzel]

Invariance of domain is an "easy" consequence of the fact that the complement of a set homeomorphic to a sphere has two connected components, so that's definitely related.

[Yury G. Kudryashov]

Michael Rothgang said:

Wait: are you talking about a different Riemann mapping theorem?

I'm talking about https://en.wikipedia.org/wiki/Riemann_mapping_theorem, so the repo you've referenced seems relevant. I'll see if it's easier to port their work to Mathlib or write a new version.

[Ruben Van de Velde]

Michael Rothgang said:

About the Riemann mapping theorem: have you seen https://github.com/vbeffara/RMT4? (There are PRs to bump it to 4.21, and I'm sure Ruben would be happy to bump it further.) If you have, great - I just want to avoid accidental duplicated work.

Up to 4.26 now

[Yury G. Kudryashov]

Sébastien Gouëzel said:

(Sketch of proof: there is a homeomorphism of R^(2n) sending K_1 \times {0} to {0} \times K_2, so R^(2n)\K_1 and R^(2n)\K_2 are homeomorphic. Then relate the homology of R^n\K_1 to that of R^(n+1)\K_1 by Mayer-Vietoris applied to K_1 x [0,+\infty) and K_1x (-\infty, 0]. Inductively, relate the homology of R^n\K_1 to that of R^(n+i)\K_1. For i=n, since R^(2n)\K_1 and R^(2n)\K_2 are homeomorphic, they have the same homologies. Then R^n\K_1 and R^n\K_2 also have the same homologies)

How do I build the homeomorphism of R^(2n)?

[Yury G. Kudryashov]

UPD: already found.

[Sébastien Gouëzel]

Let $\phi : K_1 \to K_2$ be a homeomorphism. Extend it to a continuous map $\tilde\phi : K_1 \to \R^n$ by Tietze. Then the map $(x,y)\mapsto (x, y+\phi(x))$ is a homeomorphism of $\R^{2n}$ sending $K_1 \times \{0\}$ to $\{(x, \phi(x))\}$. Using the inverse of $\phi$ and the same process, one gets another homeomorphism of $\R^{2n}$ sending $\{0\}\times K_2$ to $\{(x, \phi(x))\}$. Composing the inverse of the second one with the first one gives a homeo of $\R^{2n}$ sending $K_1\times \{0\}$ to $\{0\} \times K_2$ as desired.

[Yury G. Kudryashov]

I've got this in #33505:

theorem exists_bijOn_unitBall_map_eq_zero {U : Set ℂ} (hUo : IsOpen U) (hUc : IsSimplyConnected U)
    (hU : U ≠ univ) {x₀ : ℂ} (hx₀ : x₀ ∈ U) :
    ∃ f : ℂ → ℂ, DifferentiableOn ℂ f U ∧ BijOn f U (ball 0 1) ∧ f x₀ = 0 := by

@Ruben Van de Velde @Michael Rothgang It was easier for me to do it myself. We can pick up my/your implementation of specific theorems/lemmas/definitions during review.

[Yury G. Kudryashov]

$\approx 20\%$ of the code come from trivial lemmas in #33442

[Yury G. Kudryashov]

About singular homologies: it would be nice if someone extends docstrings in the file about docs#AlgebraicTopology.singularHomologyFunctor so that people who only saw the point topology definition can understand how to work with this definition.

[Yury G. Kudryashov]

Also, if someone volunteers to explain this to me (e.g., in a call), then I can try to formalize the Mayer-Vietoris sequence so that we can have the Jordan curve theorem etc.

[Andrew Yang]

I wonder if there are some abstract nonsense one could do to show that it satisfies the Eilenberg-Steenrod axioms?
@Joël Riou might have some ideas on this?

[Joël Riou]

I can only link to #new members > Subdivison Lemma/ Lemma of Small Simplices/ Excision Theorem

[Albert Smith]

For JCT / Sébastien's generalization, along with Mayer-Vietoris, Mathlib is also currently missing homotopy invariance of $H_*$, which seems like the most plausible route to proving goals like $H_*(\R^{n+1} \setminus (K \times \R)) = H_*(\R^n \setminus K)$ and $\tilde H_*(\R^{n+1} \setminus (K \times [0, \infty))) = 0$. (IIRC this is being worked on)

[Joël Riou]

There is a thread about the homotopy invariance #homology > Homotopy invariance of singular homology

[Vincent Beffara]

(Coming back to Lean after a few months ...) Yes the only piece missing to get the usual form of RMT is indeed the existence of primitives on simply connected domains, which in turn (as well as the usual version of the residue theorem) involves, in the plan that I had, defining contour integrals along continuous curves. I have a messy definition here https://github.com/vbeffara/Curvint/blob/main/Curvint/Covering.lean that builds a covering space of an open domain of the complex plane with a holomorphic function on it by gluing local primitives, and then lifts the contour. I was planning to come back to it this semester and clean it up, now that there is homotopy lifting with a good API ...

[Yury G. Kudryashov]

RMT is in #33505

[Yury G. Kudryashov]

(if RMT = Riemann mapping theorem)

[Vincent Beffara]

Ah nice :-) I was always planning to get $\log f$ as a primitive of $f'/f$ but indeed lifting through $\exp$ makes more sense here.

[Snir Broshi]

Can we compile a checklist of what's missing, and perhaps convert it into issues tagged "t-complex-analysis"?

[Yury G. Kudryashov]

You can try to do it, then post it here for review.

[Snir Broshi]

Unfortunately my knowledge in complex analysis is only a short undergrad course, but I can try

[Snir Broshi]

Here's a preliminary list without checking which already exist

• Borel-Carathéodory theorem
• Casorati-Weierstrass theorem
• Cauchy integral formula
• Cauchy integral theorem
• Cauchy residue theorem
• Cauchy-Riemann equations
• Cauchy's argument principle
• Identity theorem
• Liouville's theorem
• Maximum modulus principle
• Minimum modulus principle
• Morera's theorem
• Open mapping theorem
• Phragmén-Lindelöf principle
• Picard's great theorem
• Picard's little theorem
• Riemann mapping theorem (#33505)
• Rouché's theorem
• Schwarz lemma
• Schwarz reflection principle
• Schwarz-Pick theorem
• Weierstrass factorization theorem

[Yury G. Kudryashov]

We have many of these, see https://leanprover-community.github.io/undergrad.html (section about complex analysis) for a start.

[Snir Broshi]

I only see Cauchy's integral formula and maximum modulus principle in the intersection of this list and the undergrad list

[Yury G. Kudryashov]

We definitely have Liouville's theorem, Schwarz lemma, open mapping theorem, and some kind of Phragmen-Lindelof principle.

[Junyan Xu]

There's already a list above: #maths > Multivariate complex analysis @ 💬

[Yury G. Kudryashov]

We have file#Analysis/Complex/PhragmenLindelof

[Yury G. Kudryashov]

Also, I proved some form of the argument principle while formalizing Riemann mapping theorem.

[Yury G. Kudryashov]

What counts as Cauchy-Riemann equations? One direction is, e.g., https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Complex/Conformal.html#DifferentiableAt.conformalAt We also have theorems like HasStrictDerivAt.complexToReal_fderiv' Should we add fderiv Real f .I = I \bu fderiv Real f 1 and call it Cauchy-Riemann? Or should we add relations on the derivatives of im ∘ f ∘ Prod.mk x etc for f : Complex -> Complex?

[Junyan Xu]

I'm planning to do this formulation of the residue theorem:
image.png
The winding number is immediate from #33108, and I'm planning to define integration of a holomorphic function / closed form along a continuous path similarly using IsCoveringMap.monodromy with the covering map obtained from #31925.

[Snir Broshi]

Junyan Xu said:

There's already a list above: #maths > Multivariate complex analysis @ 💬

Yes I started with it (though I removed Schwarz-Christoffel since I couldn't find such a theorem), then I added more stuff, and the point is to figure out what already exists and then create issues

[Snir Broshi]

Yury G. Kudryashov said:

What counts as Cauchy-Riemann equations?

Might be a basic take, but I view them as the criterion for when a differentiable function ℝ² → ℝ² can be viewed as a differentiable function ℂ → ℂ. A version with im and re is also nice.

[Yury G. Kudryashov]

@Junyan Xu Note that we also have docs#curveIntegral

[Yury G. Kudryashov]

Snir Broshi said:

Yury G. Kudryashov said:

What counts as Cauchy-Riemann equations?

Might be a basic take, but I view them as the criterion for when a differentiable function ℝ² → ℝ² can be viewed as a differentiable function ℂ → ℂ. A version with im and re is also nice.

We have it for ℂ → E. There are several ways to specialize it to ℂ → ℂ.

[Yury G. Kudryashov]

I formalized "number of roots = integral" as a prerequisite for RMT

[Junyan Xu]

IIRC Vincent reduced RMT to existence of square root of nonvanishing function on 1-connected domain as the only input requiring covering space theory.

[Junyan Xu]

Note that we also have docs#curveIntegral

Yeah my focus is to construct something invariant under arbitrary homotopies, but it will definitely be part of the API that it's equal to curveIntegral for C^1 curves.

[Yury G. Kudryashov]

My proof of RMT uses the same fact about covering spaces.

[Yury G. Kudryashov]

BTW, #34090 is the next PR cherry-picked from my RMT proof.