Removing common prime factors from signed frequencies

The only analytic input is the primitive prime-power estimate. The descent retains the totient correction at modulus one, so both zero frequencies and arbitrary signed nonprimitive frequencies are included.

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

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.localGlobal_completeKloosterman_one (a d : ℤ) : completeKloosterman 1 (↑a) d = 1

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.localGlobal_prime_power_descent_norm (p k : ℕ) [Fact (Nat.Prime p)] (a d : ℤ) : ‖completeKloosterman (p ^ (k + 1)) (↑(↑p * a)) (↑p * d)‖ ≤ ↑p * ‖completeKloosterman (p ^ k) (↑a) d‖

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.localGlobal_gcd_scale (p n : ℕ) (a d : ℤ) : (p * n).gcd ((↑p * a).natAbs.gcd (↑p * d).natAbs) = p * n.gcd (a.natAbs.gcd d.natAbs)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.localGlobal_sqrt_scale (p n g : ℕ) : √↑(p * g) * √↑(p * n) = ↑p * √↑g * √↑n

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_prime_power_weil_of_primitive (p : ℕ) [Fact (Nat.Prime p)] (hlocal : ∀ (k : ℕ) (a d : ℤ), ¬↑p ∣ a ∨ ¬↑p ∣ d → ‖completeKloosterman (p ^ k) (↑a) d‖ ≤ ↑(k + 1) * √↑(p ^ k)) (k : ℕ) (a d : ℤ) : ‖completeKloosterman (p ^ k) (↑a) d‖ ≤ ↑(k + 1) * √↑((p ^ k).gcd (a.natAbs.gcd d.natAbs)) * √↑(p ^ k)

Exact all-frequency prime-power reduction. The primitive input is explicit, and is not being asserted as an unconditional analytic theorem here.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.localGlobal_card_divisors_prime_power (p k : ℕ) [Fact (Nat.Prime p)] : (p ^ k).divisors.card = k + 1