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.

Lean references used in this proof●2 theorems, 1 incomplete

theoremdefined in SpherePacking/Basic/PeriodicPacking.lean

contains sorry

theorem periodic_constant_eq_constant {d : ℕ} (hd : 0 < d) :
  PeriodicSpherePackingConstant d = SpherePackingConstant d

theorem periodic_constant_eq_constant {d : ℕ}
  (hd : 0 < d) :
  PeriodicSpherePackingConstant d =
    SpherePackingConstant d

theoremdefined in SpherePacking/Basic/PeriodicPacking.lean

complete

theorem periodic_constant_eq_periodic_constant_normalized {d : ℕ} (hd : 0 < d) :
  PeriodicSpherePackingConstant d =
    ⨆ S, ⨆ (_ : S.separation = 1), S.density

theorem periodic_constant_eq_periodic_constant_normalized
  {d : ℕ} (hd : 0 < d) :
  PeriodicSpherePackingConstant d =
    ⨆ S,
      ⨆ (_ : S.separation = 1), S.density

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.