Documentation

MathlibNt.SieveTheory.LiLiuGoldbachS3LevelGeometry

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.