theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12WeightedRough_le_kernel (h : ℝ → ℝ) (hh : ∀ (x : ℝ), 0 ≤ h x) (η : ℝ) (hη : 0 < η) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, (Real.log ↑N / ↑N * goldbachG12WeightedRough N fun (r : ℕ) => h (Real.log ↑r / Real.log ↑N)) ≤ (564383 / 1000000 + η) * goldbachG12PrimeKernel h N

Uniform weighted rough-mother bound; no output prime test is imposed.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorRough_integral_budget (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Real.log ↑N / ↑N * goldbachG12WeightedRough N (goldbachG12AuthorPrimeWeight N) ≤ 564383 / 1000000 * goldbachG12PrimeIntegral goldbachG11AuthorWeight + δ

Consumes the proved continuous author-weight quadrature on the ORIGINAL cross.