5.1. Outline of the construction
The functions f_-, f_+, f_0 are constructed through their Mellin transforms on the critical
line, which are then inverted (Lemma 3.3.8); by (10) the Fourier symmetries
become reflections of the frequency. The ansatz perturbs the Mellin transform of a Gaussian.
-
CohnElkies.mellinMultiplier_mul_E_neg[complete] -
CohnElkies.saddleEnvelope_conj[complete] -
CohnElkies.mellinMultiplier_mul_spectrum_neg[complete]
The Gaussian g_G(r) = 2\pi^{\lambda/2}e^{-\pi r^2} has critical-line Mellin transform
(Definition 3.3.4)
E^G_\lambda(t) = X_{g_G}(t) = \pi^{it/2}\Gamma\bigl(\tfrac{\lambda - it}{2}\bigr)
(in the formalization this formula is the definition of the envelope, CohnElkies.E).
For every even entire h real on the imaginary axis, the perturbed envelope
E_\lambda(t) = E^G_\lambda(t)e^{\lambda h(t/\lambda)} obeys, with m_\lambda from
Lemma 3.3.13, m_\lambda(t)E_\lambda(-t) = E_\lambda(t) and
\overline{E_\lambda(t)} = E_\lambda(-t) for real t; consequently, for polynomials with
P(-\zeta) = Q(\zeta), the Mellin data X_P(t) = E_\lambda(t)P(t/\lambda) and
X_Q(t) = E_\lambda(t)Q(t/\lambda) satisfy m_\lambda(t)X_P(-t) = X_Q(t), i.e. multiplication
of E^G_\lambda by an even factor preserves the Fourier symmetry of Lemma 3.3.13.
Lean code for Lemma5.1.1●3 theorems
Associated Lean declarations
-
CohnElkies.mellinMultiplier_mul_E_neg[complete]
-
CohnElkies.saddleEnvelope_conj[complete]
-
CohnElkies.mellinMultiplier_mul_spectrum_neg[complete]
-
CohnElkies.mellinMultiplier_mul_E_neg[complete] -
CohnElkies.saddleEnvelope_conj[complete] -
CohnElkies.mellinMultiplier_mul_spectrum_neg[complete]
-
theoremdefined in CohnElkies/UpperBound/MellinProfile.leancomplete
theorem CohnElkies.mellinMultiplier_mul_E_neg {ε ℓ : ℝ} (hℓ : 0 < ℓ) (t : ℝ) : CohnElkies.m_ℓ ℓ t * CohnElkies.E ε ℓ (-t) = CohnElkies.E ε ℓ t
theorem CohnElkies.mellinMultiplier_mul_E_neg {ε ℓ : ℝ} (hℓ : 0 < ℓ) (t : ℝ) : CohnElkies.m_ℓ ℓ t * CohnElkies.E ε ℓ (-t) = CohnElkies.E ε ℓ t
The multiplier identity `m_λ(t) E_λ(-t) = E_λ(t)` for the envelope.
-
theoremdefined in CohnElkies/UpperBound/MellinProfile.leancomplete
theorem CohnElkies.saddleEnvelope_conj (ε ℓ t : ℝ) : (starRingEnd ℂ) (CohnElkies.E ε ℓ t) = CohnElkies.E ε ℓ (-t)
theorem CohnElkies.saddleEnvelope_conj (ε ℓ t : ℝ) : (starRingEnd ℂ) (CohnElkies.E ε ℓ t) = CohnElkies.E ε ℓ (-t)
-
theoremdefined in CohnElkies/UpperBound/MellinProfile.leancomplete
theorem CohnElkies.mellinMultiplier_mul_spectrum_neg {ε ℓ : ℝ} (hℓ : 0 < ℓ) {P Q : ℂ → ℂ} (hPQ : ∀ (z : ℂ), P (-z) = Q z) (t : ℝ) : CohnElkies.m_ℓ ℓ t * CohnElkies.spectrum ε ℓ P (-t) = CohnElkies.spectrum ε ℓ Q t
theorem CohnElkies.mellinMultiplier_mul_spectrum_neg {ε ℓ : ℝ} (hℓ : 0 < ℓ) {P Q : ℂ → ℂ} (hPQ : ∀ (z : ℂ), P (-z) = Q z) (t : ℝ) : CohnElkies.m_ℓ ℓ t * CohnElkies.spectrum ε ℓ P (-t) = CohnElkies.spectrum ε ℓ Q t
The multiplier identity `m_λ(t) X_P(-t) = X_Q(t)` of report (40) whenever `P(-ζ) = Q(ζ)`; the cases `(P, Q) = (P₋, P₊)` and `(P₀, P₀)` give `f̂₋ = f₊` and `f̂₀ = f₀`.
\int_0^\infty e^{-\pi r^2}r^{z-1}\,dr = \tfrac12\pi^{-z/2}\Gamma(z/2) at z = \lambda - it
gives
the formula, and the identity m_\lambda(t)E^G_\lambda(-t) = E^G_\lambda(t) is immediate from the
definition of m_\lambda.
The polynomials. For j \in \{-, +, 0\} we choose a polynomial P_j and set
X_{f_j}(t) = E_\lambda(t)P_j(t/\lambda), f_j its inverse Mellin transform. Without the
perturbation (h = 0), f_j is a Gaussian times a polynomial in r^2, since multiplying
X_f(t) by t corresponds to the operator -i(r\,d/dr + \lambda). The requirements are:
P_+(-\zeta) = P_-(\zeta) and P_0(-\zeta) = P_0(\zeta), which by
Lemma 5.1.1 give \widehat{f_-} = f_+ and \widehat{f_0} = f_0;
\overline{P_j(\zeta)} = P_j(-\bar\zeta), which makes f_j real; P_+(-i) = P_-(-i) > 0 and
P_0(-i) = 0, since the first gamma pole t = -i\lambda (normalized frequency \zeta = -i)
determines f_j(0) (Lemma 5.2.17); and, since the sign of P_j(iu) will control the
sign of f_j on the saddle contour of height u (Lemma 5.4.1), P_+(iu) > 0 for
u > -1 while P_-(iu) < 0 < P_0(iu) for u slightly above 1. The simplest choice is
Definition 5.2.12, with a parameter \beta = \epsilon/4. Unperturbed,
f_0 already gives the Bourgain–Clozel–Kahane bound \mathsf{A}_+(d) \le \sqrt{(d+2)/(2\pi)},
and f_+ - f_- a sign radius \sim\sqrt{d/(2\pi)}; Gaussian times polynomial cannot beat the
constant 1/\sqrt{2\pi} (Cohn–Dong–Gonçalves), so the perturbation is essential.
The perturbation. Shifting the contour to t = \lambda(T + iu), u > -1, and writing
r = e^{v(u)} gives
f_j(r) = \dfrac{\lambda E_\lambda(i\lambda u)}{2\pi}\,r^{-(1+u)\lambda}\int_{\mathbb{R}}e^{\mathcal{L}_u(T)}P_j(T+iu)\,dT
with the centered phase \mathcal{L}_u of Definition 5.3.8; v(u) is
defined so that \mathcal{L}_u'(0) = 0 (Definition 5.3.2), and then
\mathcal{L}_u(T) = -\tfrac{\lambda V(u)}{2}T^2 + O(T^3) with V = v'. The Laplace method
(Lemma 5.4.1) shows that the integral has the sign of P_j(iu) for large d,
provided the damping D_u(T) = -\operatorname{Re}\mathcal{L}_u(T) is positive for T \ne 0 and
V(u) > 0; this covers u \ge u_* = -1 + \tfrac{\log\lambda}{4\lambda} for f_+ and
u \ge u_0 = 1 + \epsilon/4 for f_-, f_0, and Lemma 5.5.3 handles f_+ on
0 \le r \le e^{v(u_*)}. Taking h(\zeta) = \int_0^\infty w(a)(\cos(a\zeta) - 1)\,da for a
signed density w (Definition 5.2.4; the variable a parametrizes radial
dilations), the damping becomes
D_u(T) = \int_0^\infty\bigl[\mu_{\lambda,1+u}(a) + \lambda w(a)\cosh(au)\bigr](1 - \cos(aT))\,da
with the gamma damping density \mu of Definition 5.2.6, while the
radius R_{\epsilon,d} = e^{v(u_0)} satisfies
R_{\epsilon,d}/\sqrt d \to \sqrt{(1+u_0)/(4\pi)}\,\exp\bigl(\int_0^\infty w(a)a\sinh(u_0a)\,da\bigr).
So a more negative w gives a smaller radius, but D_u \ge 0 needs
w(a) \ge -\mu_{\lambda,1+u}(a)/(\lambda\cosh(au)), whose limit as \lambda \to \infty,
u \to 1 is the ideal density w_* below.
The ideal density w_*(a) = -\dfrac{e^{-2a}}{2a^2\cosh a} saturates the pointwise damping
constraint and gives the greatest inward displacement (equation (32)):
\int_0^\infty w_*(a)\,a\sinh a\,da = \int_0^\infty -\dfrac{e^{-2a}\tanh a}{2a}\,da = -\tfrac12\log\dfrac{\pi}{2}.
Lean code for Lemma5.1.2●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/UpperBound/WallisRadius.leancomplete
theorem CohnElkies.integral_wallisRadiusIntegrand : ∫ (a : ℝ) in Set.Ioi 0, CohnElkies.wallisRadiusIntegrand a = -(1 / 2) * Real.log (Real.pi / 2)
theorem CohnElkies.integral_wallisRadiusIntegrand : ∫ (a : ℝ) in Set.Ioi 0, CohnElkies.wallisRadiusIntegrand a = -(1 / 2) * Real.log (Real.pi / 2)
Report (33): the limiting short-shell contribution is `-(1/2) log (π / 2)`.
Since w_*(a)a\sinh a = -e^{-2a}\tanh(a)/(2a), the substitution x = 2a turns the integral into
-\tfrac12\int_0^\infty K(x)\,dx with the Laplace kernel
K(x) = e^{-x}(1 - e^{-x})/(x(1 + e^{-x})) (Real.Wallis.laplaceKernel). Expand
e^{-2a}\tanh a = \sum_{k\ge0}(-1)^k(e^{-2(k+1)a} - e^{-2(k+2)a}) and apply Frullani's integral
\int_0^\infty(e^{-\alpha a} - e^{-\beta a})\,da/a = \log(\beta/\alpha) termwise (the alternating
partial sums are dominated):
\int_0^\infty e^{-2a}\tanh(a)\,da/a = \sum_{k\ge0}(-1)^k\log\frac{k+2}{k+1},
the logarithm of the Wallis product \frac21\cdot\frac23\cdot\frac43\cdot\frac45\cdots = \pi/2
(Real.Wallis.integral_laplaceKernel, from Mathlib's Real.Wallis.tendsto_W_nhds_pi_div_two),
equivalently a consequence of the gamma duplication formula.
Since the Gaussian stationary radius at u = 1 is (2\pi)^{-1/2}\sqrt d, the displacement of
Lemma 5.1.2 gives the critical radius (equation (33))
\dfrac{1}{\sqrt{2\pi}}\exp\bigl(-\tfrac12\log\tfrac{\pi}{2}\bigr) = \dfrac{1}{\pi}.
Lean code for Lemma5.1.3●1 theorem
Associated Lean declarations
-
CohnElkies.saddleRadius_wallis_constant[complete]
-
CohnElkies.saddleRadius_wallis_constant[complete]
-
theoremdefined in CohnElkies/UpperBound/WallisRadius.leancomplete
theorem CohnElkies.saddleRadius_wallis_constant : √(1 / (2 * Real.pi)) * Real.exp (-(1 / 2) * Real.log (Real.pi / 2)) = CohnElkies.criticalRadius
theorem CohnElkies.saddleRadius_wallis_constant : √(1 / (2 * Real.pi)) * Real.exp (-(1 / 2) * Real.log (Real.pi / 2)) = CohnElkies.criticalRadius
\exp(-\tfrac12\log\tfrac\pi2) = \sqrt{2/\pi} and \sqrt{2/\pi}/\sqrt{2\pi} = 1/\pi.
One cannot take w = w_* itself: it is not integrable at 0 (w_*(a) = -1/(2a^2) + O(1/a)),
and at u = 1 it cancels the gamma damping exactly, so V(1) \sim 1/(8\lambda) and the
Gaussian width 1/\sqrt{\lambda V(1)} does not shrink. We therefore truncate w_* to an
interval [a_0, A] and taper it slightly, w_s = b\,w_*\mathbf 1_{[a_0,A]} with
b(a) = 1 - 2\epsilon(1+a), which changes the radius exponent by O(\epsilon) while keeping a
damping margin of order \epsilon near u = 1 (Lemma 5.2.8, Lemma 5.2.7). But then
V(u) = V_\gamma - \int_{a_0}^A|w_s|a^2\cosh(ua)\,da becomes negative for large u, since
V_\gamma \sim 1/(2(1+u)) while the shell term grows exponentially in u; this is repaired by
a small positive shell w_B = (Q/\cosh a)\mathbf 1_{[B,B+1]} at much larger dilation parameters
B > A, which is negligible at u = u_0 but dominates w_s at every frequency when
u \ge U = 1 + \epsilon/2 (Lemma 5.3.19); its interval support avoids frequencies at
which its damping would vanish. With w = w_s + w_B and the parameters below, letting first
d \to \infty and then \epsilon \downarrow 0 gives
R_{\epsilon,d}/\sqrt d \to \sqrt{2/(4\pi)}\exp(-\tfrac12\log\tfrac\pi2) = 1/\pi, which matches the
lower bound.