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

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

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaClean_modulusHighOmega_signedError_dyadic_log_payment_kscale (i k j A : ℕ) {Cscale : ℝ} (hCscale : 1 ≤ Cscale) : ∀ᶠ (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| ≤ Cscale * 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_signedError_dyadic_log_payment_kscale (i k j A : ℕ) {Cscale ε : ℝ} (hCscale : 1 ≤ Cscale) (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| ≤ Cscale * x → |signedError S N Q α β c a| ≤ x / Real.log x ^ A