Green's Open Problem 42

References:

• [Gr24] Green, Ben. "100 open problems." (2024).
• [CoEl03] Cohn, Henry, and Noam Elkies. "New upper bounds on sphere packings I." Annals of Mathematics (2003): 689-714.
• [Vi17] Viazovska, Maryna S. "The sphere packing problem in dimension 8." Annals of mathematics (2017): 991-1015.
• [CKM17] Cohn, H., Kumar, A., Miller, S., Radchenko, D., & Viazovska, M. (2017). The sphere packing problem in dimension 24. Annals of mathematics, 185(3), 1017-1033.
• [Sa21] Sardari, Naser Talebizadeh. "Higher Fourier interpolation on the plane." arXiv preprint arXiv:2102.08753 (2021).

noncomputable def Green42.fHat {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasureTheory.MeasureSpace V] [BorelSpace V] [FiniteDimensional ℝ V] (f : V → ℝ) (t : V) : ℝ

The real-valued Fourier transform used in the Cohn--Elkies conditions. For real radial admissible functions, the complex Fourier transform is expected to be real-valued; we take .re to expose the real scalar used in the inequality.

Convention: Mathlib's 𝓕 f w expands to $\int e^{-2\pi i \langle v, w \rangle} f(v) dv$, which matches [CoEl03]'s $\hat{f}(t) = \int f(x) e^{-2\pi i \langle x, t \rangle} dx$.

Equations

• Green42.fHat f t = (FourierTransform.fourier (fun (x : V) => ↑(f x)) t).re

def Green42.CohnElkiesAdmissible {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasureTheory.MeasureSpace V] [BorelSpace V] [FiniteDimensional ℝ V] (f : V → ℝ) : Prop

Definition 2.1 from [CoEl03]: A function is admissible if both the function and its Fourier transform decay sufficiently fast.

Equations

• One or more equations did not get rendered due to their size.

def Green42.SatisfiesCohnElkiesScheme {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasureTheory.MeasureSpace V] [BorelSpace V] [FiniteDimensional ℝ V] (f : V → ℝ) : Prop

The structural rules a function must satisfy to successfully pass through the Cohn-Elkies scheme and generate some valid upper bound.

Equations

• One or more equations did not get rendered due to their size.

def Green42.CohnElkiesOptimal (d : ℕ) (bound : ℝ) : Prop

The statement that there exists a function in dimension d satisfying the Cohn-Elkies scheme which achieves the center density bound bound.

Equations

• Green42.CohnElkiesOptimal d bound = ∃ (f : EuclideanSpace ℝ (Fin d) → ℝ), Green42.SatisfiesCohnElkiesScheme f ∧ f 0 / Green42.fHat f 0 = bound

theorem Green42.green_42 : sorry ↔ CohnElkiesOptimal 2 (√3 / 6)

Can the Cohn-Elkies scheme be used to prove the optimal bound for circle-packings in 2 dimensions?

theorem Green42.green_42.variants.dimension_one : CohnElkiesOptimal 1 (1 / 2)

[CoEl03] proved this when $d = 1$.

theorem Green42.green_42.variants.dimension_eight : CohnElkiesOptimal 8 (1 / 16)

[Vi17] established the case $d = 8$.

theorem Green42.green_42.variants.dimension_twenty_four : CohnElkiesOptimal 24 1

In [CKM17], [Vi17] was adapted to $d = 24$.