Common-frequency descent

Reduction of units is surjective even when the removed factor is not coprime to the retained modulus. Its uniform fibers give a totient ratio, not in general the removed factor. In particular the modulus-one endpoint is retained.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_eq_sum_units (q : ℕ) [NeZero q] (a : ZMod q) (d : ℤ) : completeKloosterman q a d = ∑ u : (ZMod q)ˣ, ZMod.stdAddChar (a * ↑u + ↑d * ↑u⁻¹)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stdAddChar_mul_modulus_cast (q r : ℕ) [NeZero q] [NeZero r] (z : ZMod (q * r)) : ZMod.stdAddChar (↑r * z) = ZMod.stdAddChar ((ZMod.castHom ⋯ (ZMod q)) z)

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

Exact descent before division; valid also when q=1 or either frequency vanishes.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_common_factor (q r : ℕ) [NeZero q] [NeZero r] (a d : ℤ) : completeKloosterman (q * r) (↑(↑r * a)) (↑r * d) = ↑(q * r).totient / ↑q.totient * completeKloosterman q (↑a) d

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

For a nontrivial retained prime power, every removed prime-power factor contributes exactly its size. This includes p=2 and t=0.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_zero_zero (q : ℕ) [NeZero q] : completeKloosterman q 0 0 = ↑q.totient

The fully degenerate endpoint has size φ(q), not q.