Complex analysis

Stream: Sphere packing in 8 dimensions

[Patrick Massot]

Is there a precise description of what is needed in general complex analysis for this project?

[Kevin Buzzard]

Is it still the case that we need to be able to integrate a holomorphic function around this contour which is "two sides of a square and then a quarter of a circle" (the shape that you get four of if you remove a unit diameter disc from a unit square)? Or is there now some hack to avoid this like the other hacks we have for Cauchy integral formula?

[Chris Birkbeck]

So yes we still need to be able to integrate that picture, but as you say, Heather explained a way to do this that should solve this. With that I think we'd have enough contour integration tricks for what we need, but @Sidharth Hariharan can maybe check me on this.

But I guess integrating more general contours is something that would help greatly here and much more widely.

[Patrick Massot]

Could we have an actual statement of a theorem that would help, with all the assumptions and conclusions?

[Sidharth Hariharan]

Screenshot 2025-06-15 at 9.40.29 am.png
Screenshot 2025-06-15 at 9.41.03 am.png

[Sidharth Hariharan]

As Chris said, with this theorem and the existing tricks and hacks, we should be sorted. Heather is actively working on this and has shared some interesting ideas with me.

Essentially this result is needed to prove this result and its analogue for the $-1$-eigenfunction $b$, which show that $a$ and $b$ are indeed Fourier eigenfunctions. I have not yet reduced the proofs of these to the version of Cauchy-Goursat I've shared above, but the idea is that when we compute the Fourier integrals of $I_1 + I_2$ and $J_1 + J_2$, we need to perform the change of variables $z \mapsto \frac{-1}{z}$ in order to show that we obtain $I_3 + I_4$ and $-(J_3 + J_4)$. This Möbius transformation turns the rectangular contours into quarter-circular contours, and we need to apply the above result to turn them back into rectangular contours, as shown below.
Screenshot 2025-06-15 at 9.55.21 am.png

[Sidharth Hariharan]

(Rectangular Cauchy-Goursat is already in mathlib)

[Patrick Massot]

@Heather Macbeth could you clarify whether you are indeed claiming this task and whether you need help?

[Heather Macbeth]

I have indeed been discussing the "trick" with Bhavik, Sid, and Alex Kontorovich. I think I can commit to writing down the details of the trick in tex/blueprint form. That will allow for a more informed discussion of whether to do this, a full contour integration theory, or something of intermediate generality.

[Alex Kontorovich]

If I understand correctly, the contour pull needed for Fig 4.4(b) is something we've already done in the PNT+ project; I think I know how to do (a) also -- will discuss with Heather tomorrow at the Simons meeting...

[Bhavik Mehta]

For (b) indeed we have this in mathlib already, that one's fine, it's 4.4a or more specifically the equality in 5.3 that's most useful.

[Patrick Massot]

Which book is this taken from?

[Pietro Monticone]

It looks like “A First Course in Complex Analysis” by Willms

[Bhavik Mehta]

No, those pictures are from Sid's thesis.

[Pietro Monticone]

Ops, sorry. Almost identical font!

[Antoine Chambert-Loir]

Regarding the Cauchy theorem, what should prevent us to try following the elementary proof by Dixon in American Math. Monthly ?
image.png
image.png

[Kevin Buzzard]

Is this theorem good enough for the application to sphere packing? Doesn't the contour there touch the boundary of where the function is defined?

[Sidharth Hariharan]

Yes, that is indeed the case for the contour we need for this project

[Kevin Buzzard]

I thought that the contour you were interested in touched the real line and you were integrating a modular form which doesn't have analytic continuation to any point in the lower half plane. Did I misremember?

[Sidharth Hariharan]

Yes, the contour does touch the real line. The integrand isn’t exactly a modular form, but some of the functions that make it up are. However, the function looks like $\phi_0\left( \frac{-1}{1+z} \right) \cdot (z+1)^2 \cdot e^{i \pi r z}$. I suppose this is not technically defined at $z = -1$ but $\phi_0$ vanishes as $\Im(z) \to \infty$.

[Kevin Buzzard]

All I'm asking is whether there's an open subset of $\mathbb{C}$ containing the contour and on which the integrand is holomorphic.

[Sidharth Hariharan]

No, there isn’t

[Sidharth Hariharan]

Which is why as you noted earlier the theorem shared by Antoine is unfortunately not quite good enough

[Antoine Chambert-Loir]

There's something I don't understand with the given statement above:
you require holomorphy at all but a countable number of points in the open domain $S$, and continuity on the closure. But then the function is locally bounded at each point where it could not be holomorphic which implies that the singularity is removable.

[Antoine Chambert-Loir]

Assuming that my description is OK, you'll get the result you want from the one I quoted plus a minor limiting argument : you can draw a slighlty smaller homothetic version of your loop inside the domain and let it grow to the loop you want; continuity of the function will make the formula extend.

[Kevin Buzzard]

My simplified (possibly oversimplified) mental model of the situation is that the function they want to integrate is related to a modular form, so it will be defined on the upper half plane and completely chaotic on the real line. The contour is: arc of the unit circle from $1$ to $i$ in the upper half plane, straight line from $1$ to $1+i$ and straight line
from $1+i$ to $i$. The only reason that the function is not chaotic on this contour is that as it approaches 1 the contours are going "straight down".

I should say that I've not read any of the details here, but the behaviour near 1 is going to be wild, the function could take all complex values on any subset of the upper half plane of the form "open disc containing 1 intersect upper half plane". I might be wrong about the details here but what's going on near 1 is super-scary if my mental model is correct.

[Junyan Xu]

Looking at the statement of the rectangular version, it looks like they were really able to prove the theorem with an arbitrary countable set, which can be dense in the domain. And it's not proven that the function is holomorphic everywhere in the open rectangle as an intermediate step.

If it were easy to prove the function must be holomorphic in the open domain, then for the desired quarter-circle contour, we may prove the equality for shrinked copies of the contour by finding a primitive of the function on a star-shaped domain containing the shrinked contour, and take the limit to obtain the equality for the actual contour.

[Junyan Xu]

Apparently the off_countable condition is inherited from Complex.integral_boundary_rect_eq_zero_of_differentiable_on_off_countable (*), and the proof is explained in this paper. Does the function we're interested in really has countably singularities in the domain, or any singularity at all?
It's not hard to prove a version of Morera's theorem (for rectangles parallel to axes) to conclude the function is holomorphic everywhere in the domain using the conclusion of (*).

[Alex Kontorovich]

I have a (dead) PR #9598 which does Morera in balls, in case it helps...

[Junyan Xu]

Oh I didn't notice that there's Morera in the PR; it's nice that you've taken this approach, even though for star-shaped domains (including convex domains, in particular discs) we can show the existence of primitives of holomorphic functions more directly using the integral $F(z)=\int_0^1 f(z_0+t(z-z_0))(z-z_0)\,dt$ (hopefully theorems in Mathlib.Analysis.Calculus.ParametricIntegral is easy to apply ...). The approach via Morera allows you to obtain primitives on domains D such that if $z,w\in D$ then the axis-parallel rectangle with zw as a diagonal lies in D. This condition implies convexity and is satisfied by discs. I might extract parts of #9598 and make a new PR.

[Seewoo Lee]

It might be great to have those details in blueprint too (current version of contour integral part is almost identical to the original paper by Viazovska)

[Kevin Buzzard]

So am I right in saying that even if we had some version of Cauchy's theorem there is a problem involving an integral around a closed contour which we are unable to do? In particular, the problem is not just that Cauchy's theorem is missing, it's also something else? Edit: no I'm not right.

Here is my understanding of the question, and please correct me if I've got something wrong here. There is a function called $\phi_0$ and it's defined here in the blueprint. This is a function which is well-defined on the upper half plane. And there's a contour, let's call it $C$, which is the following: start at $1$, go in a straight line up to $1+i$, and then one unit left in a straight line to $i$, and then clockwise around the unit circle a quarter turn back to $1$. And the claim is that the integral of some function involving $\phi_0$ around this contour is zero.

So I am not very good at analysis and I don't know how to prove this claim, but let me flag the following issue. If we replace the contour $C$ with a triangle $D$ where the curved line from $i$ to $1$ is replaced with a straight line of length $\sqrt{2}$, and if we replace the integral with $\phi_0$ it self, then I don't think it's true that the integral of $\phi_0$ around $D$ is zero for the silly reason that I am not sure that the integral of $\phi_0$ around $D$ is even a well-defined thing. Because that straight line from $1$ to $i$ is not at all a geodesic in the upper half place with its usual hyperbolic metric, and the function $\phi_0$ is completely chaotic at $z=x+iy$ as $y$ tends to zero; it has a natural boundary on the real line and it would not surprise me if $\phi_0$ is taking every complex value infinitely often (and in particular, arbitrarily large values) on the intersection of the upper half plane and any small open disc containing 1. I also suspect that $\phi_0$ will be completely wildly behaved along the straight line from $i$ to $1$ and that any attempt to define the integral from $i$ to $1$ along the straight line by defining it as a limit of the integrals from $i$ to $1+\epsilon(i-1)$ and then letting $\epsilon$ tend to zero will fail because this limit will not converge. Edit: due to a typo in the MS I had completely misunderstood the behaviour of $\phi_0$ near $z=1$ and all my worries expressed below are unfounded.

I'm well aware that "the integral of $\phi_0$ along $D$" (which scares the heck out of me) is not the same question as "the integral of some function involving $\phi_0$ and $(z-1)^2$ along $C$", but I am mildly concerned that $(z-1)^2$ might not be enough to dampen the wild oscillations of the modular function.

So what exactly is a detailed maths proof that the integral around this contour is zero?

[Kevin Buzzard]

I think my question is "after definition 7.3 it claims that $a(x)$ is well-defined. What is a maths proof of this claim?"

[Mario Carneiro]

If the function has singular behavior at $1$, wouldn't the usual fix be to cut off the contour near that point, e.g. using a straight line from $x+\epsilon i$ to $1+\epsilon i$ where $x$ intersects the circle segment of $C$, to create a modified contour $C_\epsilon$, and take the limit as $\epsilon\to 0$?

[Mario Carneiro]

you might want to modify that line to be a geodesic; perhaps using a circle of radius $\epsilon$ around $1$ instead

[Kevin Buzzard]

Certainly that limit will exist because the usual Cauchy integral formula will work for the modified contours but that unfortunately won't guarantee that you're not doing infinity - infinity later on. I think that someone who understands the nuts and bolts of the proof needs to clarify exactly what is meant by this statement "a is well-defined" in the blueprint

Note that in the definition of a we're not going around the contour, we're only going from 1 to i via an unspecified path, and I don't want that integral to be infinity or the limit of a sequence with no limit

[Bhavik Mehta]

My understanding of that comment was that the only part which is in question is the fourth integral, since it's an unbounded contour, and the comment is explaining why that integral converges.

[Bhavik Mehta]

I believe the intention of the second integral is that it's a contour over the quarter circle, and we formalised it instead as two straight lines

[Kevin Buzzard]

Do you agree that the second integrand is poorly-behaved at 1 or did I miscalculate? Edit: I did. The second integrand is fine at 1.

[Kevin Buzzard]

It seemed to me that the integrand was wild near 1

[Bhavik Mehta]

I am mildly concerned that $(z-1)^2$ might not be enough to dampen the wild oscillations of the modular function.

I had convinced myself in that past that this doesn't happen because of the second equation in Lemma 7.2: multiplying that through by z^2 gives something which (up to a shift) looks like the integrand. But that doesn't really fix the rest of your concern, I think

[Bhavik Mehta]

But I agree that we don't have a good (formal) understanding of what this integrand does near 1.

[Kevin Buzzard]

So in particular I am not even sure of the meaning of the second term in the definition of a, but as I say I might have miscalculated. I thought that the (z-1)^2 term didn't dampen the phi term quickly enough but I might have made a mistake. Edit: I did, I was misled by a typo in the paper.

[Kevin Buzzard]

This was just a pencil and paper calculation on a train yesterday

[Bhavik Mehta]

For comparison with the original paper, a(x) is defined on the bottom of page 9 here: https://arxiv.org/pdf/1603.04246 (but again this doesn't answer your question)

[Kevin Buzzard]

It is evidence that I've made a mistake with my analysis of the behaviour near 1 though

[Kevin Buzzard]

So let me go though it here. Say $z=1+i\epsilon$ with for now $\epsilon$ a positive real. Then the integrand near 1 looks like a constant times $\phi_0(i(1/\epsilon))\epsilon^2$ which is $\epsilon^2O(c^{1/\epsilon})$ with $c>1$ a real constant so it doesn't look like the integral is going to converge at all. What am I doing wrong? Analysis was never my strong point :-) is $\epsilon^2 O(c^{-1/\epsilon})$ with $c>1$ a real constant so it's all fine.

[Kevin Buzzard]

Bhavik informs me that I've got the growth of phi_0 wrong after all so it looks like all is well

[Kevin Buzzard]

I am still super scared about the integral if you go in a straight line from i to 1 but I'm no longer scared about the contour and I think mario's trick will work

[Kevin Buzzard]

In the blueprint it says "Indeed $\phi_0(z)=O(e^{-2\pi iz})$ as im(z) tends to infinity" and now I realise that this is what misled me. Although this is formally true, should it say the far more useful statement $\phi_0(z)=O(e^{+2\pi iz})$? i.e. "I am bounded by an exponentially decreasing function" rather than "I am bounded by an exponentially increasing function"? The "bounded by an exponentially increasing function" claim (which is what I used) is far too weak to make any deductions about the behaviour of the second integrand near 1 (again unless I made a mistake, but this is the source of my confusion).

[Kevin Buzzard]

I assumed "I am bounded above by an exponentially increasing function" implied "and actually I am exponentially increasing" but now I've done the calculation I've realised that this is far from the case

[Seewoo Lee]

There are three looking similar (meromorphic) modular forms, $\phi_0, \phi_{-2}, \phi_{-4}$, and $\phi_0 = (E_2 E_4 - E_6)^2 / \Delta$ is a cusp form, so indeed $\phi_0(z) = O(e^{2 \pi i z})$.
I'm not sure if this answers any of your question, but I guess disadvantage of using the straight line is that it is not a good contour on upper half plane (not a geodesic, not behaves well under the Mobius transform). I just double checked the paper and we don't have issue with singularity (again because $\phi_0$ is a cusp form, the limit of $\phi_0(-1/(z-1))$ as $z \to 1$ is 0). Quarter circle from 1 to $i$ is informally the best but probably not formally, and the two segments $1 \to 1 + i \to i$ seems to be "both informally and formally good choice" (under the Cauchy theorem we want)

[Kevin Buzzard]

@Seewoo Lee did you just make the same sign error as the sign error I'm complaining about in the post directly above, or it is me who's made the sign error?

[Kevin Buzzard]

Lol you just changed it!

[Kevin Buzzard]

OK so we agree that the blueprint has a sign error and that this is what caused me all the confusion?

[Seewoo Lee]

Oh yes I did! And it is not even blueprint but published version too.
Screenshot 2025-07-07 at 7.34.16 AM.png

[Seewoo Lee]

I also confuses pretty often between $q = e^{2 \pi i z} = e^{-2 \pi t}$ for $z = it$.

[Kevin Buzzard]

OK marvellous!

So in summary:

1) there's a trivial sign error in the paper
2) this sign error caused me to completely misunderstand the behaviour of the integrand near 1 thus making me super-worried about what was going on
3) the usual Cauchy's theorem should be fine

[Kevin Buzzard]

I had seen the $\Delta$ in the denominator of $\phi_0$ and assumed that we'd be picking up a pole at $q=0$ because of the remark about $e^{-2\pi iz}$, I only realised after Bhavik DMed me that the numerator had a double zero :-)

[Seewoo Lee]

Yeah then everything seems fine! Also let's fix typo..

[Mario Carneiro]

maybe link it back here

[Junyan Xu]

crosslinking #PR reviews > #22782 Etale space @ 💬

[taha hoseinpour]

hi, my name is taha hoseinpour, i am an undergrad cs student, i would like to contribute to the project, could someone kindly help me where to start contributing from or which current available task is suitable for start? ( sorry if i am not sending a message in appropriate topic sentence, if i am doing such a thing).

[Chris Birkbeck]

Hello! So you can have a look at the open issues here. As for what is suitable, that depends more on you background and preferences.

[Chris Birkbeck]

So I'd recommend having a look at the blueprint and open tasks, seeing which looks doable to you and then feel free to start a new topic in this stream with any questions you might have.

[taha hoseinpour]

Chris Birkbeck said:

Hello! So you can have a look at the open issues here. As for what is suitable, that depends more on you background and preferences.

hi, thanks for he reply, i will be ok with most of the mathematics given enough time, i can understand them, but it is lean that i am new to, anyway, i will learn lean pretty quickly, and hopefully if i got stuck in mathematics can i ask questions? i guess it should be doable https://github.com/thefundamentaltheor3m/Sphere-Packing-Lean/issues/91

[Chris Birkbeck]

yes definitely, feel free to claim a task and ask questions if you are unsure!

[Sidharth Hariharan]

Hi @taha hoseinpour, thank you for your interest! To reiterate what @Chris Birkbeck said, feel free to ask questions about Lean and maths alike. If you’re new to Lean, there are many excellent resources to get started, for instance the repo for a Lean course @Bhavik Mehta taught at Imperial College London last year, which gives you a basic idea of the way things are defined in various parts of mathlib.
Good to have you on board this project!

[Seewoo Lee]

Thank you for your interest @taha hoseinpour ! For the issue 91 you mentioned, I intend to resolve #87 (restrict quasimodular forms to imaginary axis) first which may provide some API for the lemma. I'm working on it but quite slowly, so I may finish some initial version of it first and you may use it to actually formalize proof of the lemma.

[taha hoseinpour]

Seewoo Lee said:

Thank you for your interest taha hoseinpour ! For the issue 91 you mentioned, I intend to resolve #87 (restrict quasimodular forms to imaginary axis) first which may provide some API for the lemma. I'm working on it but quite slowly, so I may finish some initial version of it first and you may use it to actually formalize proof of the lemma.

hi, thank you, it will take some time for me too, to read the proofs and get familiar with lean, so nothing to worry about.

[Seewoo Lee]

@taha hoseinpour FYI, the PR 87 is now review-ready, and you can find the statement in the PR as antiSerreDerPos in Derivative.lean (with sorry).