Explicit trivial bound $|S(\alpha,N)|\le N\log N$

Proved

Vino.norm_vmSum_le_mul_log

by tabbott · Sep 2, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analytic-number-theorycircle-methodnumber-theoryprime-numbers

Combining the triangle inequality with Chebyshev's bound gives, for $N\ge1$ and every real $\alpha$ ,

\left|\sum_{n<N}\Lambda(n)e(\alpha n)\right|\;\le\;N\log N.

This is the benchmark the minor-arc estimate must improve on: Vinogradov's theorem needs a saving of an arbitrary power of $\log N$ over exactly this quantity.

Preamble

import Definitions.Def_Vino_primes
import Mathlib.Analysis.SpecialFunctions.Log.Basic
open Finset

Formal statement

namespace Vino

theorem norm_vmSum_le_mul_log (α : ℝ) (N : ℕ) (hN : 1 ≤ N) : ‖vmSum α N‖ ≤ (N : ℝ) * Real.log N := by sorry

end Vino

Source

R. C. Vaughan, The Hardy-Littlewood Method, 2nd ed., Cambridge Tracts in Mathematics 125, Cambridge University Press, 1997, Chapter 3 (the three primes theorem).

View graph

Explicit trivial bound ∣S(α,N)∣≤Nlog⁡N|S(\alpha,N)|\le N\log N∣S(α,N)∣≤NlogN

Explicit trivial bound $|S(\alpha,N)|\le N\log N$