Primitive Weil bounds for every power of an odd prime

The prime endpoint uses the accepted prime Weil theorem. Higher even exponents use square-zero localization and unit-root rigidity; higher odd exponents use the proved quadratic Gauss cancellation. Unequal prime valuations vanish. All frequencies are arbitrary signed integers.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.oddPrimePower_modulus_congr (q r : ℕ) [NeZero q] [NeZero r] (h : q = r) (a d : ℤ) : completeKloosterman q (↑a) d = completeKloosterman r (↑a) d

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_odd_prime_power_primitive_sqrt (p k : ℕ) [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (hk : 1 ≤ k) (a d : ℤ) (hprimitive : ¬↑p ∣ a ∨ ¬↑p ∣ d) : ‖completeKloosterman (p ^ k) (↑a) d‖ ≤ 2 * √↑(p ^ k)

The sharp primitive local estimate at every positive exponent.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_odd_prime_power_primitive_weil (p k : ℕ) [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (a d : ℤ) (hprimitive : ¬↑p ∣ a ∨ ¬↑p ∣ d) : ‖completeKloosterman (p ^ k) (↑a) d‖ ≤ ↑(k + 1) * √↑(p ^ k)

The divisor-factor envelope, including the modulus-one endpoint k = 0. This is the complete Kloosterman sum, not a conditional local-bound interface.