Average the localized complete sum over translations by m. Each stationary orbit has a genuine quadratic Gauss norm. This retains the square-root saving at moduli p * m², rather than estimating the orbit term by term.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.oddPrimePower_stationary_orbit_norm (p m : ℕ) [Fact (Nat.Prime p)] [NeZero m] (hp2 : p ≠ 2) (hpm : p ∣ m) (a d : ℤ) (hd : ¬↑p ∣ d) (u : ZMod (p * (m * m))) (hu : IsUnit u) (hs : ↑a * (ZMod.castHom ⋯ (ZMod m)) u ^ 2 = ↑d) : ‖∑ t : ZMod (p * (m * m)), ZMod.stdAddChar (↑a * (u + ↑m * t) + ↑d * (u + ↑m * t)⁻¹)‖ = ↑(m * m) * √↑p

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_odd_square_layer_norm_le_roots (p m : ℕ) [Fact (Nat.Prime p)] [NeZero m] (hp2 : p ≠ 2) (hpm : p ∣ m) (a d : ℤ) (hd : ¬↑p ∣ d) : ‖completeKloosterman (p * (m * m)) (↑a) d‖ ≤ ↑m * √↑p * ↑{v : ZMod m | ↑a * v ^ 2 = ↑d}.card

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_odd_odd_power_norm_le (p r : ℕ) [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (hr : 1 ≤ r) (a d : ℤ) (ha : ¬↑p ∣ a) (hd : ¬↑p ∣ d) : ‖completeKloosterman (p * (p ^ r * p ^ r)) (↑a) d‖ ≤ 2 * ↑p ^ r * √↑p