noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9BaseEuler (N : ℕ) (z : ℝ) : ℝ

The base Euler product uses the exact strict prime cutoff and actual N.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9BaseEuler N z = ∏ p ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9SievePrimes N z, (1 - 1 / (↑p - 1))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9BaseEuler_eq_B10 (N : ℕ) (z : ℝ) : fouvryG9BaseEuler N z = goldbachB10PrimeProduct N z

Exact reuse of the already accepted B10/Mertens product normalization.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9BaseEuler_log_upper (ζ : ℝ) (hζ : 0 < ζ) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (N : ℕ), 4 ≤ N → Even N → ∀ (z : ℝ), z₀ ≤ z → fouvryG9BaseEuler N z * Real.log z ≤ 2 * Real.exp (-Real.eulerMascheroniConstant) * (1 + ζ) * SingularSeries.liuSingularSeries N

Uniform Liu singular-series normalization, with the full prime-divisor correction for N supplied by the existing Mertens theorem.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9BaseEuler_sqrt_upper (ζ : ℝ) (hζ : 0 < ζ) : ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → Even N → fouvryG9BaseEuler N √↑N * Real.log ↑N ≤ 4 * Real.exp (-Real.eulerMascheroniConstant) * (1 + ζ) * SingularSeries.liuSingularSeries N

The sqrt(N) specialization, with threshold still before the changing N.