Fourier interpolation in dimensions 8 and 24

ckmrv_fourier_interpolation — a formalization challenge imported from lean-eval in lean-eval comparator format.

Notes

This is the full bijectivity content of Theorem 1.9, simultaneously in dimensions 8 and 24. RadialSchwartz n is Mathlib's complex Schwartz space restricted to radial functions. RapidSampleData k0 consists of four complex sequences indexed by k >= k0, each rapidly decreasing. Coordinates 0, 1, 2, and 3 respectively sample f, its Fourier transform, the radial derivative of f, and the radial derivative of its Fourier transform at sqrt(2*k). The transform is explicitly Mathlib's Schwartz-space FourierTransform.fourierCLM; Mathlib and the paper both use the kernel exp(-2*pi*i*inner(x,y)). The coordinate-axis restriction computes the radial derivative because every sampled radius is positive. The equivalence is pinned to this sampling map, bundles the underlying bijection rather than its additional linear and topological structure, and introduces no trusted interpolation basis.

Formal statement

/-- **Cohn-Kumar-Miller-Radchenko-Viazovska Fourier interpolation theorem.**
In dimension 8 sampling starts at `sqrt 2`, while in dimension 24 it starts
at radius `2`. In both cases the four sample sequences give a bijection
between radial Schwartz functions and rapidly decreasing data. -/
theorem ckmrv_fourier_interpolation :
    CKMRV 8 1 ∧ CKMRV 24 2 := by
  sorry

Informal solution sketch

The authors construct four families of radial Schwartz interpolation basis functions in each of dimensions 8 and 24 using integral transforms of quasimodular forms. Their values, radial derivatives, Fourier-transform values, and Fourier-transform radial derivatives at the radii sqrt(2*k) form the four Kronecker-delta patterns. Polynomial bounds for all Schwartz seminorms of the basis functions imply that arbitrary rapidly decreasing coefficient sequences yield convergent sums in radial Schwartz space. The interpolation identity proves that sampling followed by this reconstruction is the identity, while the delta identities prove the converse. Thus the sampling map is an isomorphism onto four rapidly decreasing sequences, starting at k = 1 in dimension 8 and k = 2 in dimension 24.

Source

H. Cohn, A. Kumar, S. D. Miller, D. Radchenko, and M. Viazovska, 'Universal optimality of the E8 and Leech lattices and interpolation formulas', Ann. of Math. 196 (2022), 983-1082, Theorem 1.9, https://doi.org/10.4007/annals.2022.196.3.3.

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: ckmrv_fourier_interpolation
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.