Sphere Packing in Lean

8 Proof of Theorem 5.2

Our proof of the Theorem 5.2 relies on the following two inequalities for modular objects.

Consider the function \(A:(0,\infty )\to \mathbb {C}\) defined as

\begin{equation} \label{eqn:defA} A(t):=-t^2\phi _0(i/t)-\frac{36}{\pi ^2}\, \psi _I(it). \end{equation}
183

Then

\begin{equation} \label{eqn:ineqA} A(t) {\lt} 0 \end{equation}
184

for all \(t {\gt} 0\).

Proposition 8.2

Consider the function \(B:(0,\infty )\to \mathbb {C}\) defined as

\begin{equation} \label{eqn:defB} B(t) := -t^2\phi _0(i/t)+\frac{36}{\pi ^2}\, \psi _I(it) \end{equation}
185

Then

\begin{equation} \label{eqn:ineqB} B(t) {\gt} 0 \end{equation}
186

for all \(t {\gt} 0\).

Here we formalize the proof of the inequalities by Lee [ 7 ] . First, we can rewrite the inequality in 8.1 as follows.

Define two (quasi) modular forms as

\begin{align} F(z) & = (E_2(z) E_4(z) - E_6(z))^2 \label{eqn:defF} \\ G(z) & = H_2(z)^{3} (2 H_{2}(z)^{2} + 5 H_{2}(z) H_{4}(z) + 5 H_{4}(z)^{2}). \label{eqn:defG} \end{align}
Lemma 8.4

We have

\begin{align} \phi _0 & = \frac{F}{\Delta } \label{eqn:phi0-F} \\ \psi _S & = -\frac{1}{2} \frac{G}{\Delta }\label{eqn:psiS-G} \end{align}
Proof

189 is clear. 190 is already shown in Lemma 7.19.

Inequality 184 and 186 are equivalent to

\begin{align} F(it) + \frac{18}{\pi ^2} G(it) {\gt} 0 \label{eqn:ineqAnew} \\ F(it) - \frac{18}{\pi ^2} G(it) {\gt} 0 \label{eqn:ineqBnew} \end{align}

respectively.

Proof

By 151,

\begin{equation} \psi _I(it) = (\psi _S|_{-2}S)(it) = (it)^{2}\psi _S\left(-\frac{1}{it}\right) = -t^2 \psi _S\left(\frac{i}{t}\right). \end{equation}
193

Combined with Lemma 8.4 we can rewrite 184 as

\begin{equation} A(t) = -t^2 \phi _0\left(\frac{i}{t}\right) + \frac{36}{\pi ^2} \psi _S\left(\frac{i}{t}\right) {\lt} 0 \Leftrightarrow \frac{F(it)}{\Delta (it)} + \frac{18}{\pi ^2} \frac{G(it)}{\Delta (it)} {\gt} 0 \end{equation}
194

for \(t {\gt} 0\), which is equivalent to 191 by Corollary 6.25. Equivalences of 186 and 192 follows similarly; just change the sign.

Now, the first inequality 191 follows from the positivity of each \(F(it)\) and \(G(it)\).

For all \(t {\gt} 0\), we have \(F(it) {\gt} 0\) and \(G(it) {\gt} 0\).

Proof

By Ramanujan’s identity 77, we have \(F(z) = 9 E_4'(z)^2\) and

\begin{equation} F(it) = 9E_4'(it)^2 = 9 \left(240\sum _{n \geq 1} n \sigma _3(n) e^{-2 \pi n t} \right)^{2} {\gt} 0. \end{equation}
195

\(G(it) {\gt} 0\) follows from positivity of \(H_2(it)\) and \(H_4(it)\) (Lemma 6.42).

Corollary 8.7

191 holds.

Proof

This directly follows from Lemma 8.6.

To prove the second inequality 192, we need some identities satisfied by \(F\) and \(G\).

\(F\) and \(G\) satisfy the following differential equations:

\begin{align} \partial _{12}\partial _{10} F - \frac{5}{6} E_{4} F & = 7200 \Delta (-E_{2}’) \label{eqn:ddf} \\ \partial _{12}\partial _{10} G - \frac{5}{6} E_{4} G & = -640 \Delta H_{2} \label{eqn:ddg} \end{align}
Proof

Both can be shown by direct computations. By Ramanujan’s identities (Theorem 6.48) and the product rule of Serre derivatives (Theorem 6.51), we have

\begin{align} \partial _{5} (E_2 E_4 - E_6) & = (E_2 E_4 - E_6)’ - \frac{5}{12} E_2 (E_2 E_4 - E_6) \\ & = \frac{E_2^2 - E_4}{12} \cdot E_4 + E_2 \cdot \frac{E_2 E_4 - E_6}{3} - \frac{E_2 E_6 - E_4^2}{2} - \frac{5}{12}E_2 (E_2 E_4 - E_6) \\ & = -\frac{5}{12} (E_2 E_6 - E_4^2) \label{eqn:S5} \\ \partial _{7} (E_2 E_6 - E_4^2) & = (E_2 E_6 - E_4^2)’ - \frac{7}{12} E_2 (E_2 E_6 - E_4^2) \\ & = \frac{E_2^2 - E_4}{12} \cdot E_6 + E_2 \cdot \frac{E_2 E_6 - E_4^2}{2} - 2 E_4 \cdot \frac{E_2 E_4 - E_6}{3} - \frac{7}{12} E_2 (E_2 E_6 - E_4^2) \\ & = -\frac{7}{12} E_4 (E_2 E_4 - E_6) \label{eqn:S7} \end{align}

and using these we can compute

\begin{align} \partial _{10} F & = \partial _{10} (E_2 E_4 - E_6)^2 \\ & = 2 (E_2 E_4 - E_6) \partial _{5} (E_2 E_4 - E_6) \\ & = -\frac{6}{5} (E_2 E_4 - E_6) (E_2 E_6 - E_4^2), \\ \partial _{12}\partial _{10} F & = -\frac{5}{6} \partial _{12} ((E_2 E_4 - E_6) (E_2 E_6 - E_4)) \\ & = -\frac{5}{6} (\partial _{5}(E_2 E_4 - E_6)) (E_2 E_6 - E_4^2) - \frac{5}{6} (E_2 E_4 - E_6) (\partial _{7} (E_2 E_6 - E_4)) \\ & = \frac{25}{72} (E_2 E_6 - E_4^2)^2 + \frac{35}{72} E_4 (E_2 E_4 - E_6)^2, \\ \partial _{12}\partial _{10}F - \frac{5}{6} E_4 F & = \frac{25}{72}(E_2 E_6 - E_4^2)^2 + \frac{35}{72} E_4 (E_2 E_4 - E_6)^2 - \frac{5}{6} E_4 (E_2 E_4 - E_6)^2 \\ & = \frac{25}{72} ((E_2 E_6 - E_4^2)^2 - E_4 (E_2 E_4 - E_6)^2) \\ & = \frac{25}{72} (- E_2^2 E_4^3 + E_2^2 E_6^2 + E_4^4 - E_4 E_6^3) \\ & = -\frac{25}{72} (E_4^3 - E_6^2) (E_2^2 - E_4) \\ & = 7200 \cdot \frac{E_4^3 - E_6^2}{1728} \cdot \frac{-E_2^2 + E_4}{12}\\ & = 7200 \Delta (-E_2’) \end{align}

which proves 196. Similarly, 197 can be proved using Proposition 6.50 and Lemma 6.41.

196 (resp. 197) is positive (resp. negative) on the (positive) imaginary axis.

Proof

From 13 and Lemma 6.25,

\begin{equation} 7200 (-E_2'(it)) \Delta (it) = 7200 \cdot 24 \left(\sum _{n \ge 1} n \sigma _1(n) e^{-2 \pi n t}\right) \cdot \Delta (it) {\gt} 0. \notag \end{equation}
216

Negativity of 197, i.e. \(-640 \Delta (it) H_2(it) {\lt} 0\) follows from Corollary 6.42 and 6.25.

The second inequality 192 follows from the following two observations. Since \(G(it) {\gt} 0\) for all \(t {\gt} 0\), we can define the quotient

\begin{equation} \label{eqn:Q} Q(t) := \frac{F(it)}{G(it)} \end{equation}
216

as a function on \((0, \infty )\).

We have

\begin{equation} \label{eqn:Qlim} \lim _{t \to 0^+} Q(t) = \frac{18}{\pi ^2}. \end{equation}
217

Proof

We have

\begin{equation} \lim _{t \to 0^+} Q(t) = \lim _{t \to 0^+} \frac{F(it)}{G(it)} = \lim _{t \to \infty } \frac{F(i/t)}{G(i/t)}. \end{equation}
218

By using the transformation laws of Eisenstein series 14, 10 (for \(k = 4, 6\)) and the thetanull functions, 28, 30, we get

\begin{align} F\left(\frac{i}{t}\right) & = t^{12} F(it) - \frac{12t^{11}}{\pi } (E_2(it)E_4(it) - E_6(it))E_4(it) + \frac{36t^{10}}{\pi ^2}E_4(it)^2, \\ G\left(\frac{i}{t}\right) & = t^{10} H_{4}(it)^{3}(2H_{4}(it)^{2} + 5 H_{4}(it)H_{2}(it) + 5 H_{2}(it)^{2}). \end{align}

Since \(F\), \(E_2 E_4 - E_6\) and \(H_2\) are cusp forms, we have \(\lim _{t \to \infty }t^k A(it) = 0\) when \(A(z)\) is one of these forms and \(k \geq 0\). From \(\lim _{t \to \infty } E_4(it) = 1 = \lim _{t \to \infty }H_{4}(it)\), we get

\begin{align} \lim _{t \to \infty } \frac{F(i/t)}{G(i/t)} & = \lim _{t \to \infty } \frac{t^{12} F(it) - \frac{12t^{11}}{\pi } (E_2(it)E_4(it) - E_6(it))E_4(it) + \frac{36t^{10}}{\pi ^2}E_4(it)^2}{t^{10} H_{4}(it)^{3}(2H_{4}(it)^{2} + 5 H_{4}(it)H_{2}(it) + 5 H_{2}(it)^{2})} \\ & = \lim _{t \to \infty } \frac{t^{2} F(it) - \frac{12t}{\pi } (E_2(it)E_4(it) - E_6(it))E_4(it) + \frac{36}{\pi ^2}E_4(it)^2}{H_{4}(it)^{3}(2H_{4}(it)^{2} + 5 H_{4}(it)H_{2}(it) + 5 H_{2}(it)^{2})} \\ & = \frac{18}{\pi ^2}. \end{align}

The function \(t \mapsto Q(t)\) is monotone decreasing.

Proof

It is enough to show that

\begin{align} \frac{\mathrm{d}}{\mathrm{d}t} \left(\frac{F(it)}{G(it)}\right) {\lt} 0 & \Leftrightarrow (- 2\pi ) \frac{F'(it)G(it) - F(it) G'(it)}{G(it)^{2}} {\lt} 0 \\ & \Leftrightarrow F’(it) G(it) - F(it) G’(it) {\gt} 0 \\ & \Leftrightarrow (\partial _{10}F)(it) G(it) - F(it) (\partial _{10}G)(it) {\gt} 0. \end{align}

Let \(\mathcal{L}_{1, 0} := (\partial _{10}F) G - F (\partial _{10} G)\). Then its Fourier expansion starts with

\begin{equation} \mathcal{L}_{1, 0} = 5308416000 q^{\frac{7}{2}} + O(q^{\frac{9}{2}}) \notag \end{equation}
227

and its Serre derivative \(\partial _{22} \mathcal{L}_{1, 0}\) is positive by Corollary 8.9:

\begin{align} \partial _{22} \mathcal{L}_{1, 0} = (\partial _{12} \partial _{10} F) G - F (\partial _{12}\partial _{10} G) = \Delta (7200 (-E_{2}’) G + 640 H_2 F) {\gt} 0. \end{align}

Hence \(\mathcal{L}_{1, 0}(it) {\gt} 0\) by Theorem 6.52, and the monotonicity follows.

192 holds.

Proof

\begin{equation} \frac{F(it)}{G(it)} = Q(t) {\lt} \lim _{u \to 0^+} Q(u) = \frac{18}{\pi ^2} \end{equation}
228

and by Lemma 8.6, 192 follows.

Finally, we are ready to prove Theorem 5.2.

The function

\[ g(x):=\frac{\pi \, i}{8640}a(x)+\frac{i}{240\pi }\, b(x) \]

satisfies conditions 68.

Proof

First, we prove that 6 holds. By Propositions 7.11 and 7.25 we know that for \(r{\gt}\sqrt{2}\)

\begin{equation} \label{eqn:g A} g(r)=\frac{\pi }{2160}\, \sin (\pi r^2/2)^2\, \int \limits _0^\infty A(t)\, e^{-\pi r^2 t}\, dt\end{equation}
229

where

\[ A(t)=-t^2\phi _0(i/t)-\frac{36}{\pi ^2}\, \psi _I(it). \]

from the Proposition 8.1 we know that \(A(t){\lt}0\quad \mbox{for}\; t\in (0,\infty ).\) Therefore identity 229 implies 6.

Next, we prove 7. By Propositions 7.12 and 7.26 we know that for \(r{\gt}0\)

\begin{equation} \label{eqn:g B} \widehat{g}(r)=\frac{\pi }{2160}\, \sin (\pi r^2/2)^2\, \int \limits _0^\infty B(t)\, e^{-\pi r^2 t}\, dt\end{equation}
230

where

\[ B(t)=-t^2\phi _0(i/t)+\frac{36}{\pi ^2}\, \psi _I(it). \]

Finally, the property 8 readily follows from Proposition 7.13 and Proposition 7.27. This finishes the proof of Theorems 8.13 and 5.2.

1

M. Abramowitz, I. Stegun, Handbook of Mathematical Functions with Formulas, Graphs, and Mathematical Tables, Applied Mathematics Series 55 (10 ed.), New York, USA: United States Department of Commerce, National Bureau of Standards; Dover Publications, 1964.

2

J. Bruinier, Borcherds products on O(2,l) and Chern classes of Heegner divisors, Springer Lecture Notes in Mathematics 1780 (2002)

3

H. Cohn, N. Elkies, New upper bounds on sphere packings I, Annals of Math. 157 (2003) pp. 689–714.

4

F. Diamond, J. Shurman, A First Course in Modular Forms, Springer New York, 2005.

5

D. Hejhal, The Selberg trace formula for \(\mathrm{PSL}(2, \mathbb {R})\), Springer Lecture Notes in Mathematics 1001 (1983)

6

W. Kohnen, A Very Simple Proof of the \(q\)-Product Expansion of the \(\Delta \)-Function, The Ramanujan Journal 10 (2005): 71-73.

7

S. Lee, Algebraic proof of modular form inequalities for optimal sphere packings, arXiv preprint arXiv:2406.14659 (2024).

8

D. Mumford, Tata Lectures on Theta I, Birkhäuser, 1983.

9

H. Petersson, Ueber die Entwicklungskoeffizienten der automorphen Formen, Acta Mathematica, Bd. 58 (1932), pp. 169–215.

10

H. Rademacher and H. S. Zuckerman, On the Fourier coefficients of certain modular forms of positive dimension, Annals of Math. (2) 39 (1938), pp. 433–462.

11

J. Serre, A Course in Arithmetic, Springer New York, 1973.

12

Maryna S. Viazovska, The sphere packing problem in dimension 8 , Pages 991–1015 from Volume 185 (2017), Issue 3.

13

D. Zagier, Elliptic Modular Forms and Their Applications, In: The 1-2-3 of Modular Forms, (K. Ranestad, ed.) Norway, Springer Universitext, 2008.


Ecole Polytechnique Federale de Lausanne
1015 Lausanne
Switzerland
Email address: maryna.viazovska@epfl.ch