The Cohn–Elkies exponent and sign uncertainty

3. Fourier-analytic preliminaries🔗

We reduce the packing and sign-uncertainty problems to radial functions and establish the Mellin–Fourier identities used in both bounds. Throughout, Fourier transforms use the convention of the introduction, \lambda = d/2, and a radial function and its one-variable profile are denoted by the same symbol: g(x) = g(|x|). In the formalization the profile of a test function f is CohnElkies.radialProfile, r \mapsto f(re_1), and the modules of this chapter are CohnElkies/Radial.lean, CohnElkies/MellinFourier.lean, CohnElkies/Radialization.lean and CohnElkies/Admissible/Radialization.lean.

  1. 3.1. Gamma-function identities
  2. 3.2. Radial reduction
  3. 3.3. The radial Mellin transform
  4. 3.4. Subharmonic functions and the Poisson inequality for the half-plane