theorem
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_level_eventually
(B : ℝ)
:
∀ᶠ (N : ℕ) in Filter.atTop, 4 ≤ N ∧ ∀ (p : ℕ),
0 < p →
↑p ≤ ↑N ^ (1 / 3) →
1 < LiuWeight.panModulusCutoff N B / p + 1 ∧ ∀ ℓ ∈ (goldbachS1ProdPrimes N (↑N ^ (4 / 53))).primeFactors, ℓ < LiuWeight.panModulusCutoff N B / p + 1
The single cutoff pays the logarithmic loss and both natural rounding
boundaries, uniformly for every outer prime up to N^(1/3).
Inspect dependencies
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_level_eventually · compiled type and proof/definition references.