The $p\mid m$ part of $S(p^h,a)$ is $p^{k-1}S(p^{h-k},a)$ for $h\ge k$

Proved

CMSharp.S_pdvd_part_rec

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

analytic-number-theorycircle-methodexponential-sumsnumber-theory

Fix $k\ge1$ , a modulus $p\ge1$ and an integer $a$ , and consider the complete exponential sum

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

Split $S(p^{h},a)$ according to whether $p\mid m$ . This result evaluates the part over $m$ divisible by $p$ , in the range $h\ge k$ :

\sum_{\substack{m<p^{h}\\ p\,\mid\, m}}e\!\left(\frac{a m^{k}}{p^{h}}\right)\;=\;p^{\,k-1}\,S\!\left(p^{\,h-k},a\right).

Writing $m=pm'$ with $m'<p^{h-1}$ turns the phase into $a(pm')^{k}/p^{h}=am'^{k}/p^{h-k}$ , so the summand depends on $m'$ only modulo $p^{h-k}$ . As $p^{h-1}=p^{k-1}\cdot p^{h-k}$ , the range of $m'$ covers each residue class modulo $p^{h-k}$ exactly $p^{k-1}$ times, which produces the factor $p^{k-1}$ and the complete sum $S(p^{h-k},a)$ .

Together with the vanishing of the coprime part, this is the recursion $S(p^{h},a)=p^{k-1}S(p^{h-k},a)$ that drives the classical estimate $|S(q,a)|\ll q^{1-1/k+\varepsilon}$ . Note the exponents match exactly: $p^{k-1}\cdot p^{(h-k)(1-1/k)}=p^{h(1-1/k)}$ , so the induction loses nothing.

Formalization note. No coprimality between $a$ and $p$ is required here; the identity is purely a reindexing. The hypothesis $p\ge1$ only rules out the empty modulus.

Preamble

import Definitions.Def_CircleMethod_waring
import Mathlib.Data.Nat.Prime.Basic
open Finset

Formal statement

namespace CMSharp

theorem S_pdvd_part_rec {k p h : ℕ} (hp : 0 < p) (hk : 1 ≤ k) (hkh : k ≤ h) (a : ℤ) :
    ∑ m ∈ (Finset.range (p ^ h)).filter (fun m => p ∣ m),
      CircleMethod.e ((a : ℝ) * (m : ℝ) ^ k / ((p ^ h : ℕ) : ℝ))
      = (p : ℂ) ^ (k - 1) * CircleMethod.S k (p ^ (h - k)) a := 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 (the reduction of S(p^h,a) to its p | m part).

View graph

The p∣mp\mid mp∣m part of S(ph,a)S(p^h,a)S(ph,a) is pk−1S(ph−k,a)p^{k-1}S(p^{h-k},a)pk−1S(ph−k,a) for h≥kh\ge kh≥k

The $p\mid m$ part of $S(p^h,a)$ is $p^{k-1}S(p^{h-k},a)$ for $h\ge k$