noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryLevel (N : ℕ) (δ : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryLevel N δ = ↑N ^ (1 / 2 - δ)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryLevel_in_source (B : ℝ) {δ : ℝ} (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → goldbachG11OrdinaryLevel N δ ≤ √(4 * ↑N) / Real.log (4 * ↑N) ^ B

A fixed positive power saving pays the ordinary logarithmic level loss at analysis size 4N, while the level itself is still measured against original N.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryLevel_eq_low_at_boundary {N : ℕ} (hn : 0 < ↑N) (δ : ℝ) : ↑N ^ (5 / 9 - δ) / (↑N ^ (1 / 10)) ^ (5 / 9) = goldbachG11OrdinaryLevel N δ

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryLevel_gates {δ θ : ℝ} (hδ : 0 ≤ δ) (hδu : δ < 1 / 2) (hθ : 0 < θ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → 4 ≤ ↑N ^ (4 / 53) ∧ 1 ≤ goldbachG11OrdinaryLevel N δ ∧ 2 ≤ LiLiuPrereqWF.externalInternalLevel (goldbachG11OrdinaryLevel N δ) θ ∧ goldbachG11OrdinaryLevel N δ ≤ ↑N

No level-size or large-cutoff gates are supplied by the eventual caller.