theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeProduct_nonneg (N : ℕ) (hEven : Even N) (Z : ℝ) : 0 ≤ goldbachB10PrimeProduct N Z

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11BuchstabSieveEnvelope (N : ℕ) (Z A C ρ η : ℝ) : ℝ

Fixed ratio s=2, with the actual-label Buchstab sum in place of prime-window mass.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11BuchstabSieveEnvelope N Z A C ρ η = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11BuchstabUpperMass N η + 8400 * ↑N / ↑N ^ (4 / 53)) * (Real.exp Real.eulerMascheroniConstant + ρ) * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PrimeProduct N Z + 400 * C * ↑N / Real.log ↑N ^ A + 8000 * ↑⌈Z⌉₊

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PaidEnvelope_le_buchstab (η : ℝ) (hη : 0 < η) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (hEven : Even N) (ε Z A C ρ : ℝ), 0 ≤ ρ → goldbachG11PaidRosserEnvelope N hEven ε Z 2 A C ρ ≤ goldbachG11BuchstabSieveEnvelope N Z A C ρ η