The Cohn–Elkies exponent and sign uncertainty

7. Report versus formalization🔗

The Lean development follows the report's strategy (a Poisson/Mellin lower bound and a perturbed-Gaussian upper construction) but deviates from it in several places, either because a statement was easier to formalize in a different form or because the original file chose different numerical safety margins. This chapter records those deviations so that the nodes of the preceding chapters can be matched with their Lean counterparts; the nodes below are the formal replacements of the report's arguments, with their own Lean declarations. It also lists what the formalization adds to the report (the Cohn–Elkies bound) and what is still missing.

  1. 7.1. The Poisson inequality: an alternative proof by Phragmén–Lindelöf
  2. 7.2. One-sided Riemann bound in Lemma 3.3
  3. 7.3. Lemma 3.4 without the digamma identity (22)
  4. 7.4. Inverse-quadratic tail majorant in Lemma 3.5
  5. 7.5. Parameters of the upper construction
  6. 7.6. Theorem 1.1: the two halves are fused
  7. 7.7. The Cohn–Elkies bound is proved
  8. 7.8. Stirling's formula
  9. 7.9. The digamma function
  10. 7.10. Subharmonic functions and the half-plane Poisson inequality
  11. 7.11. Statements added in the reformalization
  12. 7.12. Existence of extremizers: deviations from Cohn–Gonçalves
  13. 7.13. Schwartz approximation with a bump mollifier