theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeKernel_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 → goldbachG11PrimeKernel h N ≤ goldbachG11PrimeIntegral h + ν

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

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