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

Then

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

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

Then

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

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

192 is clear. 193 is already shown in Lemma 7.19.

Inequality 187 and 189 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 154,

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

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

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

Now, the first inequality 194 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}
198

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

Corollary 8.7

194 holds.

Proof

This directly follows from Lemma 8.6.

To prove the second inequality 195, 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 199. Similarly, 200 can be proved using Proposition 6.52 and Lemma 6.42.

199 (resp. 200) 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}
219

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

The second inequality 195 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}
219

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

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

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}

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

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

195 holds.

Proof

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

and by Lemma 8.6, 195 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.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}
232

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 232 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}
233

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

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