High-omega signed modulus weights at the actual error

An arbitrary signed modulus weight supported on omega(q) > ξ gains 2^(-ξ) at the cost of doubling its fixed divisor order. For clean beta the shift is nonzero, so the shifted divisor moment pays the progression sum without any x^epsilon loss. No factorability of a masked weight is asserted.

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

Equations

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

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.modulusHighOmega_abs_le_rankin (j : ℕ) (Q : Finset ℕ) (c : ℕ → ℝ) (hc : ∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) (ξ : ℝ) (hω : ∀ q ∈ Q, c q ≠ 0 → ξ < ↑q.primeFactors.card) {q : ℕ} (hq : q ∈ Q) : |c q| ≤ 2 ^ (-ξ) * ↑((fouvryTau (2 * j)) q)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_modulusHighOmega_modEq_abs_le (j : ℕ) (Q : Finset ℕ) (c : ℕ → ℝ) (hc : ∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) (ξ : ℝ) (hω : ∀ q ∈ Q, c q ≠ 0 → ξ < ↑q.primeFactors.card) (m n : ℕ) (a : ℤ) (hne : ↑m * ↑n - a ≠ 0) : (∑ q ∈ Q, if ↑m * ↑n ≡ a [ZMOD ↑q] then |c q| else 0) ≤ 2 ^ (-ξ) * ↑((fouvryTau (2 * j + 1)) (↑m * ↑n - a).natAbs)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.modulusHighOmega_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) (ξ : ℝ) (hω : ∀ q ∈ Q, c q ≠ 0 → ξ < ↑q.primeFactors.card) : |signedError S N Q α β c a| ≤ 6 * 2 ^ (-ξ) * x * (1 + Real.log (2 * x)) ^ modulusHighOmegaLogExponent i k j

Uniform finite modulus deletion, for all fixed orders including zero and all real cutoffs. Clean beta is used only to exclude m*n=a.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaClean_modulusHighOmega_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) (ξ : ℝ) (hω : ∀ q ∈ Q, c q ≠ 0 → ξ < ↑q.primeFactors.card) : |signedError S N Q α (betaClean β a) c a| ≤ 6 * 2 ^ (-ξ) * x * (1 + Real.log (2 * x)) ^ modulusHighOmegaLogExponent i k j