Prime-power recursion $S(p^h,a)=p^{k-1}S(p^{h-k},a)$

Open

CMSharp.S_prime_pow_rec

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 $a$ an integer with $p\nmid a$ . For the complete exponential sum

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

the value at a prime power reduces to a smaller one:

S(p^{h},a)\;=\;p^{\,k-1}\,S\!\left(p^{\,h-k},a\right)\qquad (k\le h).

The hypothesis controlling the range is the existence of $j\ge1$ with $p^{j}\nmid k$ and $2j\le h$ ; for $p\nmid k$ one may take $j=1$ , so the recursion holds for all $h\ge\max(2,k)$ .

The identity comes from splitting the sum by whether $p\mid m$ . The part over $m$ coprime to $p$ vanishes, and the part over $m=pm'$ reindexes to $p^{k-1}S(p^{h-k},a)$ .

Iterating this descent is what produces the classical bound $|S(q,a)|\ll q^{1-1/k+\varepsilon}$ : the exponents match exactly, since $p^{k-1}\cdot p^{(h-k)(1-1/k)}=p^{h(1-1/k)}$ , so no saving is lost at any step.

Preamble

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

Formal statement

namespace CMSharp

theorem S_prime_pow_rec {k p h j : ℕ} (hp : p.Prime) (a : ℤ) (ha : ¬ ((p : ℤ) ∣ a))
    (hj : 1 ≤ j) (hjh : 2 * j ≤ h) (hk : ¬ ((p : ℤ) ^ j ∣ (k : ℤ)))
    (hk1 : 1 ≤ k) (hkh : k ≤ h) :
    CircleMethod.S k (p ^ h) a = (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, Theorem 4.2 and its proof in Section 4.1.

View graph

Prime-power recursion S(ph,a)=pk−1S(ph−k,a)S(p^h,a)=p^{k-1}S(p^{h-k},a)S(ph,a)=pk−1S(ph−k,a)

Prime-power recursion $S(p^h,a)=p^{k-1}S(p^{h-k},a)$