at prime powers
OpenCMSharp.S_prime_pow_boundLet , let be a prime, let , and let be an integer with . Then
This is the local half of Vaughan's Theorem 4.2: the estimate restricted to prime-power moduli, with an explicit constant depending only on .
The proof is an induction on in which three regimes appear. For one needs genuine cancellation, supplied by the Gauss-sum bound together with . For below the trivial bound already suffices, because forces and to be bounded in terms of alone — this is where the constant comes from. Above that threshold the recursion applies, and it is exponent-neutral: , so the induction closes with the same constant. When the recursion instead terminates at the exact value , which already satisfies the bound.
Combined with multiplicativity of and the divisor bound, this yields the global estimate for arbitrary moduli.
import Definitions.Def_CircleMethod_waring import Mathlib.Analysis.SpecialFunctions.Pow.Real import Mathlib.Data.Nat.Prime.Basic
namespace CMSharp
theorem S_prime_pow_bound {k : ℕ} (hk : 2 ≤ k) {p h : ℕ} (hp : p.Prime) (hh : 1 ≤ h) {a : ℤ}
(ha : ¬ ((p : ℤ) ∣ a)) :
‖CircleMethod.S k (p ^ h) a‖ ≤ (k : ℝ) ^ 3 * ((p ^ h : ℕ) : ℝ) ^ (1 - 1 / (k : ℝ)) := by sorry
end CMSharp