6. Cohn-Elkies Bounds🔗

Following Cohn and Elkies (2003), we use the sign constraints f(x) \le 0 outside the forbidden radius and \widehat{f}(x) \ge 0 everywhere.

Theorem6.1

AL∃∀Nused by 1

For a lattice-periodic packing with pairwise center distance at least one, any Schwartz function satisfying the Cohn-Elkies sign conditions bounds density by f(0) / \widehat{f}(0) \cdot \mathrm{Vol}(B_d(0,1/2)).

Code for Theorem6.1●1 definition, incomplete

axiom LinearProgrammingBound' : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
LinearProgrammingBound' : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.

axiom-like (no body)

Proof

Use Theorem 5.7 and positivity of Fourier-side terms.

Theorem6.2

AL∃∀Nused by 0

The same bound holds for arbitrary sphere packings (not necessarily periodic).

Code for Theorem6.2●1 definition, incomplete

axiom LinearProgrammingBound : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
LinearProgrammingBound : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.

axiom-like (no body)

Proof

Combine Theorem 6.1 with Theorem 2.13.

Theorem6.3

XL∃∀Nused by 0

There exists a radial Schwartz function g : \mathbb{R}^8 \to \mathbb{R} with

g(x) \le 0 for \|x\| \ge \sqrt{2},
\widehat{g}(x) \ge 0 for all x,
g(0) = \widehat{g}(0) = 1.

Proof

This follows from the explicit a,b construction and the inequalities in Theorem 9.14.