theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11EulerCorrection_eventually (ζ : ℝ) (hζ : 0 < ζ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → goldbachG11EulerCorrection N ≤ 1 + ζ

The finite 21-factor rough correction tends to one. The threshold is independent of every changing rectangle and prime.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11FamilyError_uniform (C K θ η : ℝ) (hη : 0 < η) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (Q : ℝ), 1 / 4 * Real.log ↑N ≤ Real.log Q → 4 * Real.exp (-Real.eulerMascheroniConstant) * goldbachG11FamilyErrorFactor Q C K θ ≤ 4 * Real.exp (-Real.eulerMascheroniConstant) * C * θ + η

Pay the genuine decaying external-family defect uniformly from the quarter-log lower envelope, before any changing level is supplied.