The finite U and V main-term expansions

Fouvry (1984), (7.11), and the first equality immediately following it: expand both modulus sums, then remove the coprimality restriction by Mobius inversion. The mixed term is rearranged as in (7.13). This stops before Poisson summation and its error estimates.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_moebius_divisors (n : ℕ) : ∑ d ∈ n.divisors, ↑(ArithmeticFunction.moebius d) = if n = 1 then 1 else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprime_indicator_eq_moebius {q : ℕ} (hq : q ≠ 0) (m : ℕ) : (if m.Coprime q then 1 else 0) = ∑ d ∈ q.divisors, if d ∣ m then ↑(ArithmeticFunction.moebius d) else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprime_weight_eq_moebius (S : Finset ℕ) (w : ℕ → ℝ) {q : ℕ} (hq : q ≠ 0) : (∑ m ∈ S, if m.Coprime q then w m else 0) = ∑ d ∈ q.divisors, ↑(ArithmeticFunction.moebius d) * ∑ m ∈ S, if d ∣ m then w m else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dispersionU_eq_double_sum (S N Q : Finset ℕ) (w β c : ℕ → ℝ) (a : ℤ) : dispersionU S N Q w β c a = ∑ q ∈ reducedModuli Q a, ∑ r ∈ reducedModuli Q a, c q * c r / (↑q.totient * ↑r.totient) * coprimeMass N β q * coprimeMass N β r * ∑ m ∈ S, if m.Coprime (q * r) then w m else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dispersionU_eq_moebius (S N Q : Finset ℕ) (w β c : ℕ → ℝ) (a : ℤ) (hQ : ∀ q ∈ Q, q ≠ 0) : dispersionU S N Q w β c a = ∑ q ∈ reducedModuli Q a, ∑ r ∈ reducedModuli Q a, c q * c r / (↑q.totient * ↑r.totient) * coprimeMass N β q * coprimeMass N β r * ∑ d ∈ (q * r).divisors, ↑(ArithmeticFunction.moebius d) * ∑ m ∈ S, if d ∣ m then w m else 0

The exact divisor expansion to which the Poisson estimate for U must be applied.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dispersionV_eq_progression_sum (S N Q : Finset ℕ) (w β c : ℕ → ℝ) (a : ℤ) : dispersionV S N Q w β c a = ∑ q ∈ reducedModuli Q a, ∑ r ∈ reducedModuli Q a, c q * c r / ↑r.totient * coprimeMass N β r * ∑ n ∈ N, β n * ∑ m ∈ S, if n.Coprime q ∧ m.Coprime r ∧ ↑m * ↑n ≡ a [ZMOD ↑q] then w m else 0

The mixed term with the m-sum exposed, as in F84 (7.13), without inverse notation.