Sphere Packing in Lean

8 Proof of Theorem 5.3

Our proof of the Theorem 5.3 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}
205

Then

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

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}
207

Then

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

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

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

Definition 8.3
#

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

211 is clear. 212 is already shown in Lemma 7.19.

Inequality 206 and 208 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 165,

\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}
215

Combined with Lemma 8.4 we can rewrite 206 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}
216

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

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

Lemma 8.6

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

Proof

By Ramanujan’s identity 80, 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}
217

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

Corollary 8.7
#

213 holds.

Proof

This directly follows from Lemma 8.6.

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

Lemma 8.8

\(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.49) and the product rule of Serre derivatives (Theorem 6.52), 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 218. Similarly, 219 can be proved using Proposition 6.51 and Lemma 6.41.

218 (resp. 219) 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. \end{equation*}

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

The second inequality 214 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}
238

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

Lemma 8.10
#

We have

\begin{equation} \lim _{t \to 0^+} Q(t) = \frac{18}{\pi ^2}. \end{equation}
239

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}
240

By using the transformation laws of Eisenstein series 14, 10 (for \(k = 4, 6\)) and the thetanull functions, 27, 29, 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}
Lemma 8.11

Let \(F\) be a quasimodular form where the vanishing order of \(F\) at infinity is \(n_0 {\gt} 0\), i.e. \(F(z) = \sum _{n \geq n_0} a_n q^{n}\) with \(a_{n_0} \ne 0\). Then

\begin{equation} \lim _{t \to \infty } \frac{F'(it)}{F(it)} = n_0. \end{equation}
246

Proof

By Lemma 6.44,

\begin{equation} \lim _{t \to \infty } \frac{F'(it)}{F(it)} = \lim _{t \to \infty } \frac{\sum _{n \ge n_0} n a_n e^{-2 \pi n t}}{\sum _{n \ge n_0} a_n e^{-2 \pi n t}} = \lim _{t \to \infty } \frac{n_0 a_{n_0} e^{-2 \pi n_0 t} + O(e^{-2 \pi (n_0 + 1) t})}{a_{n_0} e^{-2 \pi n_0 t} + O(e^{-2 \pi (n_0 + 1) t})} = n_0. \end{equation}
247

Proposition 8.12

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) = F'G - FG'\). Then

\begin{align} \frac{\mathcal{L}_{1, 0}}{FG} = \frac{F'G - FG'}{FG} = \frac{F'}{F} - \frac{G'}{G} \end{align}

The vanishing order of \(F\) and \(G\) at the infinity are \(2\) and \(\frac{3}{2}\) respectively, so by Lemma 8.11, we have

\begin{align} \lim _{t \to \infty } \frac{\mathcal{L}_{1, 0}(it)}{F(it) G(it)} = \lim _{t \to \infty } \left(\frac{F'(it)}{F(it)} - \frac{G'(it)}{G(it)}\right) = 2 - \frac{3}{2} = \frac{1}{2} {\gt} 0 \end{align}

so \(\mathcal{L}_{1, 0}(it) {\gt} 0\) for sufficiently large \(t\). 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.53, and the monotonicity follows.

Corollary 8.13
#

214 holds.

Proof

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

and by Lemma 8.6, 214 follows.

Finally, we are ready to prove Theorem 5.3.

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.14 and 7.28 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}
255

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 255 implies 6.

Next, we prove 7. By Propositions 7.15 and 7.29 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}
256

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.16 and Proposition 7.30. This finishes the proof of Theorems 8.14 and 5.3.

1

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

2

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

3

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

4

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

5

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

6

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

7

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

8

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

9

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.

10

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

11

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

12

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