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

Proved

CMSharp.S_pdvd_part_base

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 split the complete exponential sum

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

according to whether $p\mid m$ . In the range $1\le h\le k$ the part over $m$ divisible by $p$ degenerates completely:

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

Indeed, writing $m=pm'$ gives $a(pm')^{k}/p^{h}=a\,p^{\,k-h}m'^{k}$ , which is an integer because $h\le k$ ; every character value is therefore $1$ , and there are exactly $p^{h-1}$ multiples of $p$ below $p^{h}$ .

This is the base case of the prime-power recursion for $S(q,a)$ : it terminates the descent $h\mapsto h-k$ once the exponent drops to at most $k$ . The value $p^{h-1}$ is consistent with the target bound $|S(p^{h},a)|\le p^{h(1-1/k)}$ , since $h-1\le h-h/k$ precisely when $h\le k$ .

Formalization note. As with the recursion step, no coprimality between $a$ and $p$ is needed — the identity is an exact evaluation, not an estimate.

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_pdvd_part_base {k p h : ℕ} (hp : 0 < p) (hh : 1 ≤ h) (hhk : h ≤ k) (a : ℤ) :
    ∑ m ∈ (Finset.range (p ^ h)).filter (fun m => p ∣ m),
      CircleMethod.e ((a : ℝ) * (m : ℝ) ^ k / ((p ^ h : ℕ) : ℝ)) = ((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, 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) equals ph−1p^{h-1}ph−1 for h≤kh\le kh≤k

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