theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeKernel_buchstabGeometry {N : ℕ} (hN : 4 ≤ N) {v : GoldbachG11Label} (hv : v ∈ goldbachG12Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11))) : Real.log (↑N / ↑(goldbachG11LabelProd v)) / Real.log ↑v.snd.snd.snd ∈ Set.Icc 3 (1141 / 132)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12BuchstabUpperMass_le_primeKernel {N : ℕ} (hN : 4 ≤ N) (η W : ℝ) (_hη : 0 ≤ η) (hW : ∀ u ∈ Set.Icc 3 (1141 / 132), LiLiuPrereqBuchstab.buchstab u ≤ W) : Real.log ↑N / ↑N * goldbachG12BuchstabUpperMass N η ≤ (W + η) * goldbachG12PrimeKernel (fun (x : ℝ) => 1) N

Only the raw pointwise Buchstab bound is supplied by the caller.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12BuchstabUpperMass_eventually_nonneg (η : ℝ) (hη : 0 < η) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, 0 ≤ goldbachG12BuchstabUpperMass N η