theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeKernel_le_integral_eventually (h : ℝ → ℝ) (hh : ContinuousOn h (Set.Icc (4 / 53) (4 / 33))) (hpos : ∀ x ∈ Set.Icc (4 / 53) (4 / 33), 0 ≤ h x) (ν : ℝ) (hν : 0 < ν) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → goldbachG12PrimeKernel h N ≤ goldbachG12PrimeIntegral h + ν

Continuous nonnegative first-coordinate weights on the original cross. The prime-to-box limit, mesh cover, and exact cross integral are all proved internally.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeKernel_one_le_integral_eventually (ν : ℝ) (hν : 0 < ν) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → goldbachG12PrimeKernel (fun (x : ℝ) => 1) N ≤ (goldbachG12PrimeIntegral fun (x : ℝ) => 1) + ν

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeKernel_author_le_integral_eventually (ν : ℝ) (hν : 0 < ν) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → goldbachG12PrimeKernel goldbachG11AuthorWeight N ≤ goldbachG12PrimeIntegral goldbachG11AuthorWeight + ν