High-omega deletion at the original signed error

No well-factorability claim is made for a masked modulus sequence: the original signed c is retained throughout. Clean beta excludes the equality progression before the modulus divisor bound is used.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.highOmegaLogExponent (i k j : ℕ) : ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.highOmegaLogExponent i k j = (i + 2 * k) ^ 2 + (j + 1) ^ 2 + i + 2 * k + 2 * j

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.highOmega_signedError_bound (i k j : ℕ) {U V x : ℝ} (hU : 1 ≤ U) (hV : 1 ≤ V) (hx : 1 ≤ x) (hUV : U * V ≤ x) (hUx : U ≤ x) (hVx : V ≤ x) (S N Q : Finset ℕ) (hS : S ⊆ Finset.Ioc 0 ⌊U⌋₊) (hN : N ⊆ Finset.Ioc 0 ⌊V⌋₊) (hQ : Q ⊆ Finset.Ioc 0 ⌊x⌋₊) (α β c : ℕ → ℝ) (hα : ∀ m ∈ S, |α m| ≤ ↑((fouvryTau i) m)) (hβ : ∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) (hc : ∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) (a : ℤ) (ha : |↑a| ≤ x) (hclean : ∀ n ∈ N, β n ≠ 0 → ¬↑n ∣ a) (ξ : ℝ) : |signedError S N Q α (betaHighOmega β ξ) c a| ≤ 6 * 2 ^ (-ξ) * x * (1 + Real.log (2 * x)) ^ highOmegaLogExponent i k j

Finite, explicit high-omega deletion. The three orders can be zero. Only elementary global divisor means occur, so the saving is exponential in the actual real cutoff, not weakened by an x^epsilon factor.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaClean_highOmega_signedError_bound (i k j : ℕ) {U V x : ℝ} (hU : 1 ≤ U) (hV : 1 ≤ V) (hx : 1 ≤ x) (hUV : U * V ≤ x) (hUx : U ≤ x) (hVx : V ≤ x) (S N Q : Finset ℕ) (hS : S ⊆ Finset.Ioc 0 ⌊U⌋₊) (hN : N ⊆ Finset.Ioc 0 ⌊V⌋₊) (hQ : Q ⊆ Finset.Ioc 0 ⌊x⌋₊) (α β c : ℕ → ℝ) (hα : ∀ m ∈ S, |α m| ≤ ↑((fouvryTau i) m)) (hβ : ∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) (hc : ∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) (a : ℤ) (ha : |↑a| ≤ x) (ξ : ℝ) : |signedError S N Q α (betaHighOmega (betaClean β a) ξ) c a| ≤ 6 * 2 ^ (-ξ) * x * (1 + Real.log (2 * x)) ^ highOmegaLogExponent i k j