theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPairLiEuler_product_eq (N : ℕ) (hEven : Even N) (ε z : ℝ) (m : ℕ) : AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (goldbachS3BoundingSieve N hEven ε z m) = AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (goldbachS1BoundingSieve N hEven ε z)

Conditioning changes the carrier and its mass, but not the Euler product.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPairLiEuler_coefficient : 2 * Real.exp (-Real.eulerMascheroniConstant) / (4 / 53) = 53 / (2 * Real.exp Real.eulerMascheroniConstant)

Exact conversion of the Mertens normalization; no numerical approximation.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPairLiEuler_fixed_epsilon_lower (ε η : ℝ) (hε : 0 < ε) (hε1 : ε < 1) (hη : 0 < η) (hηu : η < 1 - ε) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (hEven : Even N) (m : ℕ), 53 / (2 * Real.exp Real.eulerMascheroniConstant) * (1 - ε - η) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ BombieriVinogradov.trueLogarithmicIntegral ↑(goldbachS1Endpoint N ε) * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (goldbachS3BoundingSieve N hEven ε (↑N ^ (4 / 53)) m)

A scalar Li-times-Euler estimate, with the genuine strict endpoint and the genuine conditioned sieve. No primality or coprimality of m is needed.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPairLiEuler_common_small_epsilon_lower (ρ : ℝ) (hρ : 0 < ρ) : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 2 / 15 ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (hEven : Even N) (m : ℕ), (53 / (2 * Real.exp Real.eulerMascheroniConstant) - ρ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ BombieriVinogradov.trueLogarithmicIntegral ↑(goldbachS1Endpoint N ε) * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (goldbachS3BoundingSieve N hEven ε (↑N ^ (4 / 53)) m)

Common small-epsilon normalized scalar lower bound. The cutoff for ε depends only on ρ; the eventual cutoff for N is independent of m.