Large values of Dirichlet polynomials

DefinitionThe Guth–Maynard large values bound#✓fully proved

For a natural number \(N\) and real numbers \(V\) and \(T\), this is the real number \(N^2 V^{-2} + N^{18/5} V^{-4} + T N^{12/5} V^{-4}\), the factor multiplying \(T^{o(T)}\) on the right-hand side of the Guth–Maynard large values estimate for Dirichlet polynomials. Here \(V^{-2}\) and \(V^{-4}\) are read as \(0\) when \(V = 0\).

noncomputable def bound (N : ℕ) (V T : ℝ) : ℝ :=
  N ^ 2 * V ^ (- 2 : ℤ) + N ^ (18 / 5 : ℝ) * V ^ (- 4 : ℤ) + T * N ^ (12 / 5 : ℝ) * V ^ (- 4 : ℤ)

Used by 1

Used byGuth–Maynard large values estimate

TheoremGuth–Maynard large values estimate#●ready to prove

There is a function \(o : \mathbb{R} \to \mathbb{R}\) with \(o(T) \to 0\) as \(T \to \infty\) such that the following holds. Let \((b_n)_{n \ge 0}\) be complex numbers with \(|b_n| \le 1\) for all \(n\), let \(N \ge 1\) and \(R\) be natural numbers, let \(V > 0\) and \(T > 1\) be real numbers, and let \(t_0, \dots, t_{R-1}\) be points of \([0, T]\) with \(|t_r - t_s| \ge 1\) whenever \(r \ne s\). Suppose that, with \(i\) the imaginary unit,

\[\left|\sum_{n=N}^{2N} b_n n^{i t_r}\right| \ge V\]

for every \(r < R\). Then

\[R \le T^{o(T)} \left(N^2 V^{-2} + N^{18/5} V^{-4} + T N^{12/5} V^{-4}\right).\]

The hypotheses \(N \ge 1\), \(V > 0\) and \(T > 1\) are not stated in the paper; the inequality may be false at \(T = 1\).

public theorem_wanted theorem_1_1 : ∃ o : ℝ → ℝ, o =o[Filter.atTop] (1 : ℝ → ℝ) ∧
    ∀ (b : ℕ → ℂ) (_hb : ∀ n, ‖b n‖ ≤ 1) (N : ℕ) (V : ℝ) (T : ℝ) (R : ℕ) (t : Fin R → ℝ),
    N > 0 → V > 0 → T > 1 → -- these assumptions are necessary but not stated in the paper
    (∀ i j, i ≠ j → |t i - t j| ≥ 1) → (∀ i, t i ∈ Set.Icc 0 T) →
    (∀ r, ‖∑ n ∈ Finset.Icc N (2 * N), b n * n ^ (I * t r)‖ ≥ V) →
    R ≤ T ^ (o T) * bound N V T

Sources

• L. Guth and J. Maynard, New large value estimates for Dirichlet polynomials, Annals of Math, 203 (2) 2026. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_large_value_estimates of the lean-eval benchmark.

Uses 1

Statement usesThe Guth–Maynard large values bound

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.