6. Cohn-Elkies Bounds🔗

In 2003 Cohn and Elkies developed linear programming bounds that apply directly to sphere packings; see Cohn and Elkies (2003). The goal of this section is to formalize the Cohn-Elkies linear programming bound.

The following theorem is the key result of Cohn and Elkies (2003). Note that the original theorem is stated for a class of functions more general then Schwartz functions.

Theorem6.1

Statement uses 2

Statement dependency previews

Preview

Definition 2.3

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1markupTeX✓L∃∀N

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. Let f:\R^d\to\R be a Schwartz function that is not identically zero and satisfies f(x)\leq 0 for \|x\|\geq 1 and \widehat{f}(x)\geq0 for all x\in\R^d. Then the density of any \Lambda-periodic sphere packing is bounded above by \frac{f(0)}{\widehat{f}(0)}\cdot \mathrm{vol}(B_d(0,1/2)).

Lean code for Theorem6.1●1 theorem

theoremdefined in SpherePacking/CohnElkies/LPBound.lean

complete

theorem LinearProgrammingBound' {d : ℕ}
  {f : SchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ} (hne_zero : f ≠ 0)
  (hReal : ∀ (x : EuclideanSpace ℝ (Fin d)), ↑(f x).re = f x)
  (hRealFourier :
    ∀ (x : EuclideanSpace ℝ (Fin d)),
      ↑((FourierTransform.fourier f) x).re =
        (FourierTransform.fourier f) x)
  (hCohnElkies₁ :
    ∀ (x : EuclideanSpace ℝ (Fin d)), ‖x‖ ≥ 1 → (f x).re ≤ 0)
  (hCohnElkies₂ :
    ∀ (x : EuclideanSpace ℝ (Fin d)),
      ((FourierTransform.fourier f) x).re ≥ 0)
  {P : PeriodicSpherePacking d} (hP : P.separation = 1)
  [Nonempty ↑P.centers] {D : Set (EuclideanSpace ℝ (Fin d))}
  (hD_isBounded : Bornology.IsBounded D)
  (hD_unique_covers :
    ∀ (x : EuclideanSpace ℝ (Fin d)), ∃! g, g +ᵥ x ∈ D)
  (hd : 0 < d) (hf : Summable ⇑f) :
  P.density ≤
    ↑(f 0).re.toNNReal / ↑((FourierTransform.fourier f) 0).re.toNNReal *
      MeasureTheory.volume (Metric.ball 0 (1 / 2))

theorem LinearProgrammingBound' {d : ℕ}
  {f :
    SchwartzMap (EuclideanSpace ℝ (Fin d))
      ℂ}
  (hne_zero : f ≠ 0)
  (hReal :
    ∀ (x : EuclideanSpace ℝ (Fin d)),
      ↑(f x).re = f x)
  (hRealFourier :
    ∀ (x : EuclideanSpace ℝ (Fin d)),
      ↑((FourierTransform.fourier f)
              x).re =
        (FourierTransform.fourier f) x)
  (hCohnElkies₁ :
    ∀ (x : EuclideanSpace ℝ (Fin d)),
      ‖x‖ ≥ 1 → (f x).re ≤ 0)
  (hCohnElkies₂ :
    ∀ (x : EuclideanSpace ℝ (Fin d)),
      ((FourierTransform.fourier f)
            x).re ≥
        0)
  {P : PeriodicSpherePacking d}
  (hP : P.separation = 1)
  [Nonempty ↑P.centers]
  {D : Set (EuclideanSpace ℝ (Fin d))}
  (hD_isBounded : Bornology.IsBounded D)
  (hD_unique_covers :
    ∀ (x : EuclideanSpace ℝ (Fin d)),
      ∃! g, g +ᵥ x ∈ D)
  (hd : 0 < d) (hf : Summable ⇑f) :
  P.density ≤
    ↑(f 0).re.toNNReal /
        ↑((FourierTransform.fourier f)
                0).re.toNNReal *
      MeasureTheory.volume
        (Metric.ball 0 (1 / 2))

Proof for Theorem 6.1

uses 1

Here we reproduce the proof given in Cohn and Elkies (2003). The inequality \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) follows from the first Cohn-Elkies condition 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\geq0 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 second Cohn-Elkies condition and estimate \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). Comparing inequalities, 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.

Theorem6.2

uses 0used by 1markupTeX✓L∃∀N

Let f:\R^d\to\R be a Schwartz function that is not identically zero and satisfies Cohn-Elkies condition 1 and Cohn-Elkies condition 2 above. Then the density of any \Lambda-periodic sphere packing is bounded above by \frac{f(0)}{\widehat{f}(0)}\cdot \mathrm{vol}(B_d(0,1/2)).

Lean code for Theorem6.2●1 theorem

theoremdefined in SpherePacking/CohnElkies/LPBound.lean

complete

theorem LinearProgrammingBound {d : ℕ}
  {f : SchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ} (hne_zero : f ≠ 0)
  (hReal : ∀ (x : EuclideanSpace ℝ (Fin d)), ↑(f x).re = f x)
  (hRealFourier :
    ∀ (x : EuclideanSpace ℝ (Fin d)),
      ↑((FourierTransform.fourier f) x).re =
        (FourierTransform.fourier f) x)
  (hCohnElkies₁ :
    ∀ (x : EuclideanSpace ℝ (Fin d)), ‖x‖ ≥ 1 → (f x).re ≤ 0)
  (hCohnElkies₂ :
    ∀ (x : EuclideanSpace ℝ (Fin d)),
      ((FourierTransform.fourier f) x).re ≥ 0)
  (hd : 0 < d) (hf : Summable ⇑f) :
  SpherePackingConstant d ≤
    ↑(f 0).re.toNNReal /
        ↑(FourierTransform.fourier (⇑f) 0).re.toNNReal *
      MeasureTheory.volume (Metric.ball 0 (1 / 2))

theorem LinearProgrammingBound {d : ℕ}
  {f :
    SchwartzMap (EuclideanSpace ℝ (Fin d))
      ℂ}
  (hne_zero : f ≠ 0)
  (hReal :
    ∀ (x : EuclideanSpace ℝ (Fin d)),
      ↑(f x).re = f x)
  (hRealFourier :
    ∀ (x : EuclideanSpace ℝ (Fin d)),
      ↑((FourierTransform.fourier f)
              x).re =
        (FourierTransform.fourier f) x)
  (hCohnElkies₁ :
    ∀ (x : EuclideanSpace ℝ (Fin d)),
      ‖x‖ ≥ 1 → (f x).re ≤ 0)
  (hCohnElkies₂ :
    ∀ (x : EuclideanSpace ℝ (Fin d)),
      ((FourierTransform.fourier f)
            x).re ≥
        0)
  (hd : 0 < d) (hf : Summable ⇑f) :
  SpherePackingConstant d ≤
    ↑(f 0).re.toNNReal /
        ↑(FourierTransform.fourier (⇑f)
                0).re.toNNReal *
      MeasureTheory.volume
        (Metric.ball 0 (1 / 2))

Proof for Theorem 6.2

Proof uses 2

Proof dependency previews

Preview

Theorem 2.13

Loading preview

Proof dependency preview content is loaded from the rendered-fragment cache.

The result follows immediately from Theorem Theorem 2.13 and the Cohn-Elkies periodic theorem Theorem 6.1.

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

Theorem6.3

uses 1used by 1markupTeXXL∃∀N

There exists a radial Schwartz function g:\R^8\to\R which satisfies: g(x)\leq 0\text{ for } \|x\|\geq \sqrt{2} \widehat{g}(x)\geq0\text{ for all } x\in\R^8 g(0)=\widehat{g}(0)=1.