Trivial bound for the prime exponential sum

Proved

Vino.norm_primeSum_le

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

analytic-number-theorycircle-methodnumber-theoryprime-numbers

For every real $\alpha$ ,

\left|\sum_{\substack{p<N\\ p\ \mathrm{prime}}}e(\alpha p)\right|\;\le\;\pi(N),

the number of primes below $N$ . This is the unweighted counterpart of the trivial bound $|S(\alpha,N)|\le\psi(N)$ for the von Mangoldt weighting.

Preamble

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

Formal statement

namespace Vino

theorem norm_primeSum_le (α : ℝ) (N : ℕ) :
    ‖primeSum α N‖ ≤ (((Finset.range N).filter Nat.Prime).card : ℝ) := 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