Prove2Me
Navigate
MissionsFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Vaughan Theorem 4.2: ∣S(q,a)∣≪k,εq1−1/k+ε|S(q,a)|\ll_{k,\varepsilon} q^{1-1/k+\varepsilon}∣S(q,a)∣≪k,ε​q1−1/k+ε

Open
CMSharp.S_sharp_bound

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

analytic-number-theorycircle-methodexponential-sumsnumber-theory

Let k≥2k\ge2k≥2 and ε>0\varepsilon>0ε>0. There is a constant C=C(k,ε)>0C=C(k,\varepsilon)>0C=C(k,ε)>0 such that for every modulus q≥1q\ge1q≥1 and every integer aaa with (a,q)=1(a,q)=1(a,q)=1,

∣S(q,a)∣=∣∑m<qe ⁣(amkq)∣  ≤  C q 1−1k+ε.\left|S(q,a)\right|=\left|\sum_{m<q}e\!\left(\frac{am^{k}}{q}\right)\right|\;\le\;C\,q^{\,1-\frac1k+\varepsilon}.∣S(q,a)∣=​m<q∑​e(qamk​)​≤Cq1−k1​+ε.

This is the classical bound for complete exponential sums, Theorem 4.2 of Vaughan's The Hardy-Littlewood Method. It is sharper than the exponent 1−21−k+ε1-2^{1-k}+\varepsilon1−21−k+ε obtainable by applying Weyl's inequality at N=qN=qN=q: the two agree at k=2k=2k=2, and for every k≥3k\ge3k≥3 one has 1−1k<1−21−k1-\tfrac1k<1-2^{1-k}1−k1​<1−21−k, a saving that grows with kkk.

Structure of the proof. By the Chinese remainder theorem q↦S(q,a)q\mapsto S(q,a)q↦S(q,a) is multiplicative in a twisted sense, S(q1q2,a)=S(q1,aq2k−1)S(q2,aq1k−1)S(q_{1}q_{2},a)=S(q_{1},aq_{2}^{k-1})S(q_{2},aq_{1}^{k-1})S(q1​q2​,a)=S(q1​,aq2k−1​)S(q2​,aq1k−1​) for (q1,q2)=1(q_1,q_2)=1(q1​,q2​)=1, so everything reduces to prime powers, where ∣S(ph,a)∣≤k3(ph)1−1/k|S(p^{h},a)|\le k^{3}(p^{h})^{1-1/k}∣S(ph,a)∣≤k3(ph)1−1/k. Multiplying these local estimates over the prime factorization gives

∣S(q,a)∣  ≤  (k3)ω(q)q 1−1k,|S(q,a)|\;\le\;\left(k^{3}\right)^{\omega(q)}q^{\,1-\frac1k},∣S(q,a)∣≤(k3)ω(q)q1−k1​,

and the accumulated constant is absorbed by the divisor bound: choosing JJJ with k3≤2Jk^{3}\le2^{J}k3≤2J one has (k3)ω(q)≤d(q)J≪εqε(k^{3})^{\omega(q)}\le d(q)^{J}\ll_{\varepsilon}q^{\varepsilon}(k3)ω(q)≤d(q)J≪ε​qε. The ε\varepsilonε in the statement is exactly the price of this last step; the exponent 1−1/k1-1/k1−1/k itself is attained without loss.

Why it matters. In Waring's problem the local factors A(q,n)A(q,n)A(q,n) are built from S(q,a)S(q,a)S(q,a), and the absolute convergence of the singular series depends on how fast ∣S(q,a)∣|S(q,a)|∣S(q,a)∣ decays below the trivial qqq. The exponent 1−1/k1-1/k1−1/k is what makes the singular series converge for s>2ks>2ks>2k rather than only for sss exponentially large in kkk.

Preamble
import Definitions.Def_CircleMethod_waring
import Mathlib.Analysis.SpecialFunctions.Pow.Real
Formal statement
namespace CMSharp

theorem S_sharp_bound {k : ℕ} (hk : 2 ≤ k) {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (q : ℕ) (a : ℤ), 0 < q → Nat.Coprime a.natAbs q →
      ‖CircleMethod.S k q a‖ ≤ C * (q : ℝ) ^ (1 - 1 / (k : ℝ) + ε) := by sorry

end CMSharp
Source
R. C. Vaughan, The Hardy-Littlewood Method, 2nd ed., Cambridge Tracts in Mathematics 125, Cambridge University Press, 1997, Chapter 4, Theorem 4.2 and its proof in Section 4.1.

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactJoin Slack© 2026 Prove2Me