Bound for the non-coprime part of the exponential sum

Proved

Vino.norm_vmSum_noncoprime_le

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

analytic-number-theorycircle-methodnumber-theoryprime-numbers

For every real $\alpha$ , every $q\ge1$ and every $N\ge1$ ,

\left|\sum_{\substack{n<N\\ (n,q)>1}}\Lambda(n)\,e(\alpha n)\right|\;\le\;\omega(q)\log N.

This is the error term of the major-arc identity for $S(\alpha,N)$ at a reduced fraction $b/q$ , bounded uniformly in $\alpha$ . It shows that replacing $S(b/q,N)$ by its character expansion over the reduced residues costs at most $\omega(q)\log N$ , which is $O(\log q\log N)$ and therefore invisible next to the main term.

Preamble

import Definitions.Def_Vino_primes
import Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
import Mathlib.Data.Nat.Factorization.PrimePow
import Mathlib.Analysis.SpecialFunctions.Log.Basic
open Finset

Formal statement

namespace Vino

theorem norm_vmSum_noncoprime_le {q : ℕ} (hq : 0 < q) {N : ℕ} (hN : N ≠ 0) (α : ℝ) :
    ‖∑ n ∈ (Finset.range N).filter (fun n => ¬ Nat.Coprime n q),
        ((ArithmeticFunction.vonMangoldt n : ℝ) : ℂ) * CircleMethod.e (α * (n : ℝ))‖
      ≤ (q.primeFactors.card : ℝ) * 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, Sections 3.1-3.2 (the three primes theorem).

View graph