The Cohn–Elkies Linear Programming Bound

This file proves the Cohn–Elkies linear programming bound on sphere packing densities.

theorem fourier_ne_zero {d : ℕ} {f : SchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ} (hne_zero : f ≠ 0) : FourierTransform.fourier f ≠ 0

theorem f_nonneg_at_zero {d : ℕ} {f : SchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ} (hCohnElkies₂ : ∀ (x : EuclideanSpace ℝ (Fin d)), ((FourierTransform.fourier f) x).re ≥ 0) : 0 ≤ (f 0).re

theorem f_zero_pos {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)), ((FourierTransform.fourier f) x).re ≥ 0) : 0 < (f 0).re

theorem calc_steps' {d : ℕ} {f : SchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ} {P : PeriodicSpherePacking d} {D : Set (EuclideanSpace ℝ (Fin d))} (hD_isBounded : Bornology.IsBounded D) (hd : 0 < d) (hf : Summable ⇑f) : ∑' (x : ↑(P.centers ∩ D)) (y : ↑(P.centers ∩ D)) (ℓ : ↥P.lattice), (f (↑x - ↑y + ↑ℓ)).re = (∑' (x : ↑(P.centers ∩ D)) (y : ↑(P.centers ∩ D)) (ℓ : ↥P.lattice), f (↑x - ↑y + ↑ℓ)).re

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 : ↥P.lattice, 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) (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))