theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1PrimeProduct_log_ge_liuSingularSeries (η : ℝ) (hη : 0 < η) (_hη1 : η < 1) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ∀ (z : ℝ), ↑N ^ (1 / 18) ≤ z → 2 * Real.exp (-Real.eulerMascheroniConstant) * (1 - η) * SingularSeries.liuSingularSeries N ≤ MertensTheorem.goldbachSieveProduct N ⌈z⌉₊ * Real.log z