theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm_primeSupported (upper : Bool) (P : Finset ℕ) (D η z : ℝ) (t : List ℕ) : PrimeSupported P (externalTerm upper P D η z t)

The actual full-integer coefficients have only primes from the original carrier.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm_coprime_of_ne_zero (upper : Bool) (P : Finset ℕ) (D η z : ℝ) (t : List ℕ) (N d : ℕ) (hPN : ∀ p ∈ P, p.Coprime N) (hd : (externalTerm upper P D η z t) d ≠ 0) : d.Coprime N

Non-squarefree coefficients are kept; prime support alone eliminates non-reduced moduli when the sieve primes are coprime to the actual N.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm_sum_eq_reduced (upper : Bool) (P : Finset ℕ) (D η z : ℝ) (t : List ℕ) (N : ℕ) (hPN : ∀ p ∈ P, p.Coprime N) (Q : Finset ℕ) (r : ℕ → ℝ) : ∑ d ∈ Q, (externalTerm upper P D η z t) d * r d = ∑ d ∈ AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q ↑N, (externalTerm upper P D η z t) d * r d

Exact reduction of the modulus carrier for the SAME actual external weight.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm_full_eq_signedError (upper : Bool) (P : Finset ℕ) (D η z : ℝ) (t : List ℕ) (N : ℕ) (hPN : ∀ p ∈ P, p.Coprime N) (U V : Finset ℕ) (α β : ℕ → ℝ) (Q : ℝ) : ∑ d ∈ Finset.Icc 1 ⌊Q⌋₊, (externalTerm upper P D η z t) d * AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.bilinearDiscrepancy U V α β (↑N) d = AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError U V (Finset.Ioc 0 ⌊Q⌋₊) α β (fun (d : ℕ) => (externalTerm upper P D η z t) d) ↑N

Full interval and reduced C2 error agree without a weight mask.