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}

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 from the definitions. 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 strictly 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 6–8.

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