Divisor deletion at the actual signed-error entry

The equality m*n=a is separated before summing modulus divisors. It costs the total modulus mass once per beta index, not once per alpha index. All remaining progression terms have a nonzero difference.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError_add_beta (S N Q : Finset ℕ) (α β γ c : ℕ → ℝ) (a : ℤ) : signedError S N Q α (fun (n : ℕ) => β n + γ n) c a = signedError S N Q α β c a + signedError S N Q α γ c a

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError_eq_clean_add_divisorPart (S N Q : Finset ℕ) (α β c : ℕ → ℝ) (a : ℤ) : signedError S N Q α β c a = signedError S N Q α (betaClean β a) c a + signedError S N Q α (betaDivisorPart β a) c a

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError_abs_le_product_majorant (S N Q : Finset ℕ) (α β c : ℕ → ℝ) (a : ℤ) : |signedError S N Q α β c a| ≤ ∑ n ∈ N, |β n| * ∑ m ∈ S, |α m| * ((∑ q ∈ Q, if ↑m * ↑n ≡ a [ZMOD ↑q] then |c q| else 0) + ∑ q ∈ Q, |c q| / ↑q.totient)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_progression_moduli_le_split (S Q : Finset ℕ) (c : ℕ → ℝ) (a : ℤ) {n : ℕ} (hn : 0 < n) {D : ℝ} (hD : 0 ≤ D) (hne : ∀ m ∈ S, ↑m * ↑n ≠ a → (∑ q ∈ Q, if ↑m * ↑n ≡ a [ZMOD ↑q] then |c q| else 0) ≤ D) : (∑ m ∈ S, ∑ q ∈ Q, if ↑m * ↑n ≡ a [ZMOD ↑q] then |c q| else 0) ≤ ↑S.card * D + ∑ q ∈ Q, |c q|

The equality progression contributes at most one alpha index.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError_abs_le_split (S N Q : Finset ℕ) (α β c : ℕ → ℝ) (a : ℤ) {A D : ℝ} (hA : 0 ≤ A) (hD : 0 ≤ D) (hα : ∀ m ∈ S, |α m| ≤ A) (hN : ∀ n ∈ N, 0 < n) (hne : ∀ n ∈ N, ∀ m ∈ S, ↑m * ↑n ≠ a → (∑ q ∈ Q, if ↑m * ↑n ≡ a [ZMOD ↑q] then |c q| else 0) ≤ D) : |signedError S N Q α β c a| ≤ (A * ∑ n ∈ N, |β n|) * (↑S.card * D + ∑ q ∈ Q, |c q| + ↑S.card * ∑ q ∈ Q, |c q| / ↑q.totient)

A finite majorant retaining the separate equality cost.