theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaClean_highOmega_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) (ξ : ℝ) : |signedError S N Q α (betaHighOmega (betaClean β a) ξ) c a| ≤ 6 * Cscale * (1 + Real.log Cscale) ^ highOmegaLogExponent i k j * 2 ^ (-ξ) * x * (1 + Real.log (2 * x)) ^ highOmegaLogExponent i k j

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaClean_highOmega_signedError_log_payment_kscale (i k j A : ℕ) {Cscale : ℝ} (hCscale : 1 ≤ Cscale) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (U V : ℝ), 1 ≤ U → 1 ≤ V → U * V ≤ x → U ≤ x → V ≤ x → ∀ (S N Q : Finset ℕ), S ⊆ Finset.Ioc 0 ⌊U⌋₊ → N ⊆ Finset.Ioc 0 ⌊V⌋₊ → Q ⊆ Finset.Ioc 0 ⌊x⌋₊ → ∀ (α β c : ℕ → ℝ), (∀ m ∈ S, |α m| ≤ ↑((fouvryTau i) m)) → (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ), |↑a| ≤ Cscale * x → |signedError S N Q α (betaHighOmega (betaClean β a) (highOmegaCutoff x)) c a| ≤ x / Real.log x ^ A ∧ |signedError S N Q α (betaClean β a) c a - signedError S N Q α (betaLowOmega (betaClean β a) (highOmegaCutoff x)) c a| ≤ x / Real.log x ^ A ∧ |signedError S N Q α (betaClean β a) c a| ≤ |signedError S N Q α (betaLowOmega (betaClean β a) (highOmegaCutoff x)) c a| + x / Real.log x ^ A