Prime-power base case $S(p^h,a)=p^{h-1}$ for $h\le k$

Open

CMSharp.S_prime_pow_base

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

analytic-number-theorycircle-methodexponential-sumsnumber-theory

Let $p$ be a prime and $a$ an integer with $p\nmid a$ . In the range $h\le k$ the complete exponential sum at the prime power $p^{h}$ takes the exact value

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

under the same range hypothesis as the recursion: there is a $j\ge1$ with $p^{j}\nmid k$ and $2j\le h$ .

The reason is that the part of the sum over $m$ coprime to $p$ vanishes identically, while on the remaining terms $m=pm'$ the phase $a(pm')^{k}/p^{h}=a\,p^{\,k-h}m'^{k}$ is an integer, so each of the $p^{h-1}$ surviving terms contributes $1$ .

This terminates the descent $h\mapsto h-k$ in the prime-power analysis of $S(q,a)$ . The value is consistent with the target estimate $|S(p^{h},a)|\le p^{h(1-1/k)}$ , since $h-1\le h-h/k$ exactly when $h\le k$ .

Preamble

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

Formal statement

namespace CMSharp

theorem S_prime_pow_base {k p h j : ℕ} (hp : p.Prime) (a : ℤ) (ha : ¬ ((p : ℤ) ∣ a))
    (hj : 1 ≤ j) (hjh : 2 * j ≤ h) (hk : ¬ ((p : ℤ) ^ j ∣ (k : ℤ))) (hhk : h ≤ k) :
    CircleMethod.S k (p ^ h) a = ((p ^ (h - 1) : ℕ) : ℂ) := 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 base case S(ph,a)=ph−1S(p^h,a)=p^{h-1}S(ph,a)=ph−1 for h≤kh\le kh≤k

Prime-power base case $S(p^h,a)=p^{h-1}$ for $h\le k$