The part of $S(p^h,a)$ over residues prime to $p$ vanishes

Proved

CMSharp.S_coprime_part_eq_zero

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

analytic-number-theorycircle-methodexponential-sumsnumber-theory

Let $p$ be a prime, $k\ge1$ , and let $a$ be an integer with $p\nmid a$ . Write

S(p^{h},a)=\sum_{m<p^{h}}e\!\left(\frac{a m^{k}}{p^{h}}\right),\qquad e(\theta)=e^{2\pi i\theta}.

Split this complete sum according to whether $p\mid m$ . The assertion is that the part running over $m$ prime to $p$ vanishes identically,

\sum_{\substack{m<p^{h}\\ p\,\nmid\, m}}e\!\left(\frac{a m^{k}}{p^{h}}\right)=0,

provided $h$ is large enough relative to how divisible $k$ is by $p$ : precisely, whenever there is a $j\ge1$ with $p^{j}\nmid k$ and $2j\le h$ .

Why it is true. Substitute $m\mapsto m+p^{h-j}t$ . Since $2j\le h$ we have $2(h-j)\ge h$ , so $(p^{h-j}t)^{2}\equiv0\pmod{p^{h}}$ and the binomial expansion terminates after the linear term:

(m+p^{h-j}t)^{k}\equiv m^{k}+k\,m^{k-1}p^{h-j}t \pmod{p^{h}}.

The substitution permutes the residues prime to $p$ , so averaging over $t$ modulo $p^{h}$ gives

p^{h}\!\!\sum_{p\nmid m}\!e\!\left(\frac{am^{k}}{p^{h}}\right)=\sum_{p\nmid m}e\!\left(\frac{am^{k}}{p^{h}}\right)\sum_{t}e\!\left(\frac{a k m^{k-1}t}{p^{j}}\right).

The inner sum is a complete additive character sum, hence $0$ unless $p^{j}\mid a k m^{k-1}$ . As $p\nmid a$ and $p\nmid m$ , that would force $p^{j}\mid k$ , which is excluded. So every inner sum vanishes and the whole coprime part is $0$ .

This is the engine behind the prime-power estimate for $S(q,a)$ : it reduces $S(p^{h},a)$ to its $p\mid m$ part, which is a scaled copy of $S(p^{h-k},a)$ , and iterating that recursion yields the classical bound $|S(q,a)|\ll q^{1-1/k+\varepsilon}$ of Vaughan, Theorem 4.2.

Remark. When $p\nmid k$ one may take $j=1$ , so the conclusion holds for every $h\ge2$ .

Preamble

import Definitions.Def_CircleMethod_char
import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
open Finset

Formal statement

namespace CMSharp

theorem S_coprime_part_eq_zero {k p h j : ℕ} (hp : p.Prime) (a : ℤ) (ha : ¬ ((p : ℤ) ∣ a))
    (hj : 1 ≤ j) (hjh : 2 * j ≤ h) (hk : ¬ ((p : ℤ) ^ j ∣ (k : ℤ))) :
    ∑ m ∈ (Finset.range (p ^ h)).filter (fun m => ¬ p ∣ m),
      CircleMethod.e ((a : ℝ) * (m : ℝ) ^ k / ((p ^ h : ℕ) : ℝ)) = 0 := 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, Section 4.1, Lemma 4.4 and the proof of Theorem 4.2 (vanishing of the sum over residues coprime to p).

View graph

The part of S(ph,a)S(p^h,a)S(ph,a) over residues prime to ppp vanishes

The part of $S(p^h,a)$ over residues prime to $p$ vanishes