noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PrimeProduct (N : ℕ) (Z : ℝ) : ℝ

The actual B10 Euler product, written in the existing Mertens normalization with the strict cutoff transported by Nat.ceil.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PrimeProduct N Z = MathlibNt.SieveTheory.MertensTheorem.goldbachSieveProduct N ⌈Z⌉₊

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PrimeProduct_eq_sieveProductPrimeFactors (N : ℕ) (_hEven : Even N) (ε b c Z X : ℝ) : goldbachB10PrimeProduct N Z = AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (goldbachB10BoundingSieve N _hEven ε b c Z X)

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

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