The Fouvry interval estimate from primitive prime powers

This is a conditional assembly theorem. It assumes only the local primitive estimate, not any complete all-modulus or incomplete Kloosterman estimate.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalInterval_fouvry_of_primitive_prime_power (hlocal : ∀ (p k : ℕ) (x : Fact (Nat.Prime p)) (a d : ℤ), ¬↑p ∣ a ∨ ¬↑p ∣ d → ‖completeKloosterman (p ^ k) (↑a) d‖ ≤ ↑(k + 1) * √↑(p ^ k)) {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (q : ℕ) (x : NeZero q) (d : ℤ) (X Y : ℝ), X ≤ Y → Y - X ≤ ↑q → ‖reciprocalInterval q d X Y‖ ≤ C * √↑(q.gcd d.natAbs) * ↑q ^ (1 / 2 + ε)