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

Original cross mother with the actual output sieve providing the second logarithm.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12BuchstabSieveEnvelope N Z A C ρ η = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12BuchstabUpperMass 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.goldbachG12OutputTotal_le_concreteBuchstabSieve (A ρ η : ℝ) (hA : 0 < A) (hρ : 0 < ρ) (hη : 0 < η) : ∃ (B : ℝ) (C : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → ∀ (ε : ℝ), 400 * ∑ m ∈ goldbachG12ActiveProductSupport N, goldbachG12NormalizedCoefficient N m * ↑(goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m).card ≤ goldbachG12BuchstabSieveEnvelope N (goldbachG11SieveCutoff B N) A C ρ η

All cutoff choices are discharged using the square-root-level parameter theorem. No assertion of the author's stronger low-band coefficient is made.