The odd-prime Kloosterman bound

The polynomial character, its quadratic generating series, the finite Euler identity, the actual extension trace identity, and the Stepanov point bound are all proved in the imported modules. Cesaro averaging converts the bound on the total root power sum into individual bounds without losing multiplicity.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosReciprocalRoots_norm_le (p : ℕ) [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (a b : ZMod p) (ha : a ≠ 0) (hb : b ≠ 0) (m : ZMod p) (hm : m ≠ 0) : ‖harcosReciprocalRootPlus (m * a) (m * b)‖ ≤ √↑p ∧ ‖harcosReciprocalRootMinus (m * a) (m * b)‖ ≤ √↑p

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosReciprocalRoots_norm_eq (p : ℕ) [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (a b : ZMod p) (ha : a ≠ 0) (hb : b ≠ 0) : ‖harcosReciprocalRootPlus a b‖ = √↑p ∧ ‖harcosReciprocalRootMinus a b‖ = √↑p

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_odd_prime_weil (p : ℕ) [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (a : ZMod p) (d : ℤ) (ha : a ≠ 0) (hd : ↑d ≠ 0) : ‖completeKloosterman p a d‖ ≤ 2 * √↑p

Harcos's Theorem 1 for the actual complete sum, with an arbitrary integer second frequency and no unproved Weil or root-power premise.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_prime_primitive_weil (p : ℕ) [Fact (Nat.Prime p)] (a d : ℤ) (hprimitive : ¬↑p ∣ a ∨ ¬↑p ∣ d) : ‖completeKloosterman p (↑a) d‖ ≤ 2 * √↑p

The prime-modulus estimate, including p = 2 and one zero frequency. Both frequencies may be arbitrary signed integers; only their simultaneous vanishing modulo the prime is excluded.