theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Linked_sieveProduct_eq (N : ℕ) (hEven : Even N) (ε Z X : ℝ) : AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (goldbachG11LinkedBoundingSieve N hEven ε Z X) = goldbachB10PrimeProduct N Z

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Linked_sieveProduct_log_le (η : ℝ) (hη : 0 < η) : ∃ (Z₀ : ℝ), 2 ≤ Z₀ ∧ ∀ (N : ℕ), 4 ≤ N → ∀ (hEven : Even N) (ε X Z : ℝ), Z₀ ≤ Z → AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (goldbachG11LinkedBoundingSieve N hEven ε Z X) * Real.log Z ≤ 2 * Real.exp (-Real.eulerMascheroniConstant) * (1 + η) * SingularSeries.liuSingularSeries N

The already proved uniform Euler comparison on the actual G11 sieve.