theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.g9IntegerFibre_dvd_iff (a : ℤ) (q m n : ℕ) : q ∣ (a - ↑m * ↑n).natAbs ↔ ↑m * ↑n ≡ a [ZMOD ↑q]

Absolute integer differences allow overhanging positive rectangles, including zero values, without truncated natural subtraction.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.g9IntegerFibre_original (N m n : ℕ) (h : m * n ≤ N) : (↑N - ↑m * ↑n).natAbs = N - m * n

On the original product window this is literally the original natural difference.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.g9IntegerFibreDivisibility (U V : Finset ℕ) (α β : ℕ → ℝ) (a : ℤ) (q : ℕ) : ℝ

Weighted divisibility mass on the actual product-indexed sequence.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.g9IntegerFibreDivisibility U V α β a q = ∑ p ∈ U ×ˢ V, if q ∣ (a - ↑p.1 * ↑p.2).natAbs then α p.1 * β p.2 else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.g9IntegerFibreDivisibility_eq (U V : Finset ℕ) (α β : ℕ → ℝ) (a : ℤ) (q : ℕ) : g9IntegerFibreDivisibility U V α β a q = ∑ m ∈ U, ∑ n ∈ V, if ↑m * ↑n ≡ a [ZMOD ↑q] then α m * β n else 0

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.g9IntegerFibreCenter (U V : Finset ℕ) (α β : ℕ → ℝ) (q : ℕ) : ℝ

The center remains the true coprime mass, not a new scalar-density hypothesis.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.g9IntegerFibreCenter U V α β q = (∑ m ∈ U, ∑ n ∈ V, if (m * n).Coprime q then α m * β n else 0) / ↑q.totient

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.g9IntegerFibre_centered_eq (U V : Finset ℕ) (α β : ℕ → ℝ) (a : ℤ) (q : ℕ) : g9IntegerFibreDivisibility U V α β a q - g9IntegerFibreCenter U V α β q = bilinearDiscrepancy U V α β a q

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.g9IntegerFibre_signedError (U V Q : Finset ℕ) (α β c : ℕ → ℝ) (a : ℤ) : ∑ q ∈ reducedModuli Q a, c q * (g9IntegerFibreDivisibility U V α β a q - g9IntegerFibreCenter U V α β q) = signedError U V Q α β c a