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

Then

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

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

Then

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

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.

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

209 is clear. 210 is already shown in Lemma 7.19.

Inequality 204 and 206 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}
213

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

for \(t {\gt} 0\), which is equivalent to 211 by Corollary 6.26. Equivalences of 206 and 212 follows similarly; just change the sign.

Now, the first inequality 211 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 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}
215

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

Corollary 8.7

211 holds.

Proof

This directly follows from Lemma 8.6.

To prove the second inequality 212, 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.50) and the product rule of Serre derivatives (Theorem 6.53), 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 216. Similarly, 217 can be proved using Proposition 6.52 and Lemma 6.42.

216 (resp. 217) is positive (resp. negative) on the (positive) imaginary axis.

Proof

From 13 and Lemma 6.26,

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

Negativity of 217, i.e. \(-640 \Delta (it) H_2(it) {\lt} 0\) follows from Corollary 6.43 and 6.26.

The second inequality 212 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}
236

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

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

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

Proof

By Lemma 6.45,

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

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.54, and the monotonicity follows.

212 holds.

Proof

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

and by Lemma 8.6, 212 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.27 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}
253

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

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

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.29. 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