Uniform payment for high-omega signed modulus weights

At the growing cutoff (log x)^(1/5), the clean error is O(x/log^A x) uniformly in all changing dyadic scales, coefficients, and residues. For original beta a separate divisor-deletion cost includes the equality progression. Its eventual payment uses a positive lower exponent for the beta scale and the C.2 level bound; it is not exponentially small in omega.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaClean_modulusHighOmega_signedError_dyadic_bound (i k j : ℕ) {M T L x : ℝ} (hM : 1 ≤ M) (hT : 1 ≤ T) (hx : 1 ≤ x) (hscale : x = 4 * M * T) (hLx : L ≤ x) (S N Q : Finset ℕ) (hS : ∀ m ∈ S, M ≤ ↑m ∧ ↑m ≤ 2 * M) (hN : ∀ n ∈ N, T ≤ ↑n ∧ ↑n ≤ 2 * T) (hQ : Q ⊆ Finset.Ioc 0 ⌊L⌋₊) (α β 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

The exact dyadic specialization uses the upper endpoints 2*M, 2*T. It does not need a positive beta-scale exponent or a nonzero residue.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaClean_modulusHighOmega_signedError_dyadic_log_payment (i k j A : ℕ) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M T L : ℝ), 1 ≤ M → 1 ≤ T → x = 4 * M * T → L ≤ x → ∀ (S N Q : Finset ℕ), (∀ m ∈ S, M ≤ ↑m ∧ ↑m ≤ 2 * M) → (∀ n ∈ N, T ≤ ↑n ∧ ↑n ≤ 2 * T) → Q ⊆ Finset.Ioc 0 ⌊L⌋₊ → ∀ (α β c : ℕ → ℝ), (∀ m ∈ S, |α m| ≤ ↑((fouvryTau i) m)) → (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → (∀ q ∈ Q, c q ≠ 0 → highOmegaCutoff x < ↑q.primeFactors.card) → ∀ (a : ℤ), |↑a| ≤ x → |signedError S N Q α (betaClean β a) c a| ≤ x / Real.log x ^ A

The threshold depends only on the fixed three orders and logarithmic saving. Modulus signs and the residue remain arbitrary after that threshold.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.modulusHighOmega_eventually_signedError_bound (i k j : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M T L : ℝ), 1 ≤ M → 1 ≤ T → 1 ≤ L → x = 4 * M * T → L ≤ x → ∀ (S N Q : Finset ℕ), (∀ m ∈ S, M ≤ ↑m ∧ ↑m ≤ 2 * M) → (∀ n ∈ N, T ≤ ↑n ∧ ↑n ≤ 2 * T) → Q ⊆ Finset.Ioc 0 ⌊L⌋₊ → ∀ (α β c : ℕ → ℝ), (∀ m ∈ S, |α m| ≤ ↑((fouvryTau i) m)) → (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ), a ≠ 0 → |↑a| ≤ x → ∀ (ξ : ℝ), (∀ 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 + 4 * (M + L) * x ^ (3 * δ)

Original beta, with an explicit additional term covering divisor indices and m*n=a. No exponential cutoff gain is asserted for that additional term.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.modulusHighOmega_signedError_dyadic_log_payment (i k j A : ℕ) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M T L : ℝ), 1 ≤ M → 1 ≤ T → 1 ≤ L → x = 4 * M * T → x ^ ε ≤ T → L ≤ x ^ (5 / 9) → ∀ (S N Q : Finset ℕ), (∀ m ∈ S, M ≤ ↑m ∧ ↑m ≤ 2 * M) → (∀ n ∈ N, T ≤ ↑n ∧ ↑n ≤ 2 * T) → Q ⊆ Finset.Ioc 0 ⌊L⌋₊ → ∀ (α β c : ℕ → ℝ), (∀ m ∈ S, |α m| ≤ ↑((fouvryTau i) m)) → (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → (∀ q ∈ Q, c q ≠ 0 → highOmegaCutoff x < ↑q.primeFactors.card) → ∀ (a : ℤ), a ≠ 0 → |↑a| ≤ x → |signedError S N Q α β c a| ≤ x / Real.log x ^ A

Genuine original-beta payment under the C.2 scale restrictions. All orders may be zero, and one threshold works for every changing residue in 0 < |a| ≤ x, including those with equality progressions.