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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SieveLevel B N = ↑N ^ (1 / 2) / Real.log ↑N ^ (B + 1)

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SieveCutoff B N = √(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SieveLevel B N)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SieveParameters_eventually (B K τ : ℝ) (hB : 0 ≤ B) (hτ : 0 < τ) (hτ1 : τ ≤ 1) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, have Δ := goldbachG11SieveLevel B N; have Z := goldbachG11SieveCutoff B N; max 2 K ≤ Z ∧ Z ≤ ↑N ^ (1 / 4) ∧ 0 < Δ ∧ 2 = Real.log Δ / Real.log Z ∧ Δ ≤ √↑N / Real.log ↑N ^ B ∧ 0 < Real.log Z ∧ Real.log ↑N / Real.log Z ≤ 4 * (1 + τ)

Reuse the existing public B8 cutoff theorem; only the actual G11 level cap is added.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11_le_concreteBuchstabSieve (A ρ δ η : ℝ) (hA : 0 < A) (hρ : 0 < ρ) (hδ : 0 < δ) (hη : 0 < η) : ∃ (B : ℝ) (C : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → ∀ (ε : ℝ), 0 ≤ ε → ↑(goldbachWeightG11 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ goldbachG11BuchstabSieveEnvelope N (goldbachG11SieveCutoff B N) A C ρ η + δ * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

All sieve parameters are now concrete functions of N. The remaining main term is the actual finite Buchstab sum, not the paper's tighter low-band constant.