Payment at the growing cutoff (log x)^(1/5)

The threshold depends only on fixed orders and the requested logarithmic saving. It precedes all changing scales, supports, coefficients and residues.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.highOmegaCutoff (x : ℝ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.highOmegaCutoff x = Real.log x ^ (1 / 5)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.highOmega_eventually_log_payment (K : ℝ) (hK : 0 ≤ K) (B A : ℕ) : ∀ᶠ (x : ℝ) in Filter.atTop, K * 2 ^ (-highOmegaCutoff x) * (1 + Real.log (2 * x)) ^ B ≤ 1 / Real.log x ^ A

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError_eq_lowOmega_add_highOmega (S N Q : Finset ℕ) (α β c : ℕ → ℝ) (a : ℤ) (ξ : ℝ) : signedError S N Q α β c a = signedError S N Q α (betaLowOmega β ξ) c a + signedError S N Q α (betaHighOmega β ξ) c a

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaClean_highOmega_signedError_log_payment (i k j A : ℕ) : ∀ᶠ (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| ≤ 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

All data, including the changing residue, follow the large-x threshold. The three conclusions give the deleted error, the actual original-to-trimmed difference, and its triangle transfer.