Sphere Packing in Lean

5 Cohn-Elkies linear programming bounds

In 2003 Cohn and Elkies [ 3 ] developed linear programming bounds that apply directly to sphere packings. The goal of this section is to formalize the Cohn–Elkies linear programming bound.

The following theorem is the key result of [ 3 ] . (The original theorem is stated for a class of functions more general then Schwartz functions)

(Cohn–Elkies [ 3 ] ) Suppose that \(f:\mathbb {R}^d\to \mathbb {R}\) is a Schwartz function that is not identically zero and satisfies the following conditions:

\begin{equation} \label{eqn:Cohn-Elkies-condition-1}f(x)\leq 0\mbox{ for } \| x\| \geq 1\end{equation}
2

and

\begin{equation} \label{eqn:Cohn-Elkies-condition-2}\widehat{f}(x)\geq 0\mbox{ for all } x\in \mathbb {R}^d.\end{equation}
3

Then the density of \(d\)-dimensional sphere packings is bounded above by

\[ \frac{f(0)}{\widehat{f}(0)}\cdot \mathrm{vol}(B_d(0,1/2)). \]
Proof

Here we reproduce the proof given in [ 3 ] . We will first prove the theorem for periodic packings.

Let \(X\subset \mathbb {R}^d\) be a discrete subset such that \(\| x-y\| \geq 1\) for any distinct \(x,y\in X\). Suppose that \(X\) is \(\Lambda \)-periodic with respect to some lattice \(\Lambda \subset \mathbb {R}^d\).

The inequality

\begin{equation} \label{eqn: sharp X 1} \sharp (X/\Lambda )\cdot f(0)\geq \sum _{x\in X}\sum _{y\in X/\Lambda }f(x-y)=\sum _{x\in X/\Lambda }\sum _{y\in X/\Lambda }\sum _{\ell \in \Lambda }f(x-y+l)\end{equation}
4

follows from the condition 2 of the theorem and the assumption on the distances between points in \(X\). The equality

\[ \sum _{x\in X/\Lambda }\sum _{y\in X/\Lambda }\sum _{\ell \in \Lambda }f(x-y+l)=\sum _{x\in X/\Lambda }\sum _{y\in X/\Lambda }\frac{1}{\mathrm{vol}(\mathbb {R}^d/\Lambda )}\, \sum _{m\in \Lambda ^*} \widehat{f}(m)\, e^{2\pi i m(x-y)}. \]

follows from the Poisson summation formula. The right hand side of the above equation can be written as

\[ \sum _{x\in X/\Lambda }\sum _{y\in X/\Lambda }\frac{1}{\mathrm{vol}(\mathbb {R}^d/\Lambda )}\, \sum _{m\in \Lambda ^*} \widehat{f}(m)\, e^{2\pi i m(x-y)}=\frac{1}{\mathrm{vol}(\mathbb {R}^d/\Lambda )}\, \sum _{m\in \Lambda ^*} \widehat{f}(m)\cdot \big|\sum _{x\in X/\Lambda }e^{2\pi i m x}\big|^2. \]

Note that \(\big|\sum _{x\in X/\Lambda }e^{2\pi i m x}\big|^2\geq 0\) for all \(m\in \Lambda ^*\). Moreover, the term corresponding to \(m=0\) satisfies \(\big|\sum _{x\in X/\Lambda }e^{2\pi i 0 x}\big|^2=\sharp (X/\Lambda )^2\). Now we use the condition 3 and estimate

\begin{equation} \label{eqn: sharp X 2}\frac{1}{\mathrm{vol}(\mathbb {R}^d/\Lambda )}\, \sum _{m\in \Lambda ^*} \widehat{f}(m)\cdot \big|\sum _{x\in X/\Lambda }e^{2\pi i m(x-y)}\big|^2 \geq \frac{\sharp (X/\Lambda )^2}{\mathrm{vol}(\mathbb {R}^d/\Lambda )}\cdot \widehat{f}(0). \end{equation}
5

Comparing inequalities 4 and 5 we arrive at

\[ \frac{\sharp (X/\Lambda )}{\mathrm{vol}(\mathbb {R}^d/\Lambda )}\leq \frac{f(0)}{\widehat{f}(0)}. \]

Now we see that the density of the periodic packing \(\mathcal{P}_X\) with balls of radius \(1/2\) is bounded by

\[ \Delta (\mathcal{P}_X)=\frac{\sharp (X/\Lambda )}{\mathrm{vol}(\mathbb {R}^d/\Lambda )}\cdot {\mathrm{vol}(B_d(0,1/2))}\leq \frac{f(0)}{\widehat{f}(0)}\cdot \mathrm{vol}(B_d(0,1/2)). \]

This finishes the proof of the theorem for periodic packings. Theorem 1.15 implies the desired result for arbitrary packings.

The main step in our proof of theorem 1.16 is the explicit construction of an optimal function. It will be convenient for us to scale this function by \(\sqrt{2}\).

Theorem 5.2

There exists a radial Schwartz function \(g:\mathbb {R}^8\to \mathbb {R}\) which satisfies:

\begin{align} g(x)& \leq 0\mbox{ for } \| x\| \geq \sqrt{2} \label{eqn:g1}\\ \widehat{g}(x)& \geq 0\mbox{ for all } x\in \mathbb {R}^8\label{eqn:g2}\\ g(0)& =\widehat{g}(0)=1.\label{eqn:g3} \end{align}

Theorem 5.1 applied to the optimal function \(f(x)=g(x/\sqrt{2})\) immediately implies theorem 1.16.