7.4. Inverse-quadratic tail majorant in Lemma 3.5
Rather than integrating the two bounds (24) and (25) separately over |s| \le B\lambda and
|s| > B\lambda, the formalization averages them into a single integrable majorant.
For every 0 < c < 1/\pi there are \sigma \in (0,1) and \gamma, C > 0 such that, for all
sufficiently large d and all S \in \mathbb{R},
\exp\bigl(H_\sigma(\lambda S)\bigr) \le \dfrac{Ce^{-\gamma\lambda}}{(1 + |S|)^2}, with
H_\sigma from Definition 4.1.11 and R = c\sqrt d. Consequently
\int_{\mathbb{R}}|Z(s + i\sigma\lambda)|\,ds \le CJ\lambda e^{-\gamma\lambda} with
J = \int_{\mathbb{R}}(1 + |S|)^{-2}\,dS, which is (26) of Lemma 4.1.33.
Lean code for Lemma7.4.1●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/CenteredMax.leancomplete
theorem CohnElkies.exists_lowerStripPoissonMajorant_integrable_majorant {c : ℝ} (hc : 0 < c) (hsharp : c < Real.pi⁻¹) : ∃ σ γ C, 0 < σ ∧ σ < 1 ∧ 0 < γ ∧ 0 < C ∧ ∀ᶠ (d : ℕ) in Filter.atTop, ∀ (S : ℝ), Real.exp (CohnElkies.H_σ (↑d / 2) (c * √↑d) σ (↑d / 2 * S)) ≤ C * Real.exp (-γ * (↑d / 2)) / (1 + |S|) ^ 2
theorem CohnElkies.exists_lowerStripPoissonMajorant_integrable_majorant {c : ℝ} (hc : 0 < c) (hsharp : c < Real.pi⁻¹) : ∃ σ γ C, 0 < σ ∧ σ < 1 ∧ 0 < γ ∧ 0 < C ∧ ∀ᶠ (d : ℕ) in Filter.atTop, ∀ (S : ℝ), Real.exp (CohnElkies.H_σ (↑d / 2) (c * √↑d) σ (↑d / 2 * S)) ≤ C * Real.exp (-γ * (↑d / 2)) / (1 + |S|) ^ 2
Report Lemma 3.6: a Cauchy-type integrable majorant for `exp H_σ`, uniform in the dimension.
Combine the uniform negativity H_\sigma(s) \le -\gamma\lambda of Lemma 4.1.31, which
follows from the central bound Lemma 4.1.26 and the maximum property
Lemma 4.1.25 together with the negativity of the bracket from
Lemma 4.1.30, with the logarithmic tail
H_\sigma(\lambda S) \le -\kappa\lambda\log(|S|/A) for |S| \ge B of
Lemma 4.1.32, which follows from the gamma identities of
Lemma 3.1.3 applied to the majorant and the exponential decay of the kernel
(Lemma 4.1.9; with \kappa = \int_{-1}^1P_\sigma(T)\,dT/2 > 0):
for large d, \kappa\lambda \ge 4, and averaging the two bounds (halving \gamma) gives the
inverse-square decay; the bounded interval |S| \le B is absorbed into C. Then
|Z(s+i\sigma\lambda)| \le e^{H_\sigma(s)} (Lemma 4.1.22) and the substitution
s = \lambda S give the L^1 bound.