noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_sieveRatio (N : ℕ) (B : ℝ) (p : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_sieveRatio N B p = Real.log ↑(MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B / p) / Real.log (↑N ^ (4 / 53))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_ratio_geometry (B ξ : ℝ) (hB : 0 ≤ B) (hξ : 0 < ξ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (p : ℕ), 1 ≤ p → ↑N ^ (4 / 53) ≤ ↑p → ↑p ≤ ↑N ^ (1 / 3) → 0 < ↑(LiuWeight.panModulusCutoff N B / p) ∧ 3 / 2 ≤ goldbachS3_sieveRatio N B p ∧ goldbachS3_sieveRatio N B p ≤ 6 ∧ |goldbachS3_sieveRatio N B p - (1 / 2 - Real.log ↑p / Real.log ↑N) / (4 / 53)| ≤ ξ

One threshold controls the genuine rounded ratio and its moving argument error for every integer in the full S3 window, not just for a fixed prime.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_ratio_range (B : ℝ) (hB : 0 ≤ B) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (p : ℕ), 1 ≤ p → ↑N ^ (4 / 53) ≤ ↑p → ↑p ≤ ↑N ^ (1 / 3) → 0 < ↑(LiuWeight.panModulusCutoff N B / p) ∧ 3 / 2 ≤ goldbachS3_sieveRatio N B p ∧ goldbachS3_sieveRatio N B p ≤ 6