noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorIntegralConstant : ℝ

Original cross author weight, with the proved uniform Buchstab majorant.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorIntegralConstant = 564383 / 1000000 * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeIntegral MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorWeight

theorem G12AuthorOutput.original_total_integral (τ : ℝ) (hτ : 0 < τ) (ε : ℝ) : 0 < ε → ε ≤ 2 / 15 → ∃ (K : ℕ), 4 ≤ K ∧ ∀ N ≥ K, Even N → ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductPrimeTotal N ε (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11))) ≤ (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorIntegralConstant + τ) * (MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

The complete original product-prime count, after paying the entire boundary, the whole safe grid, cutoff slice, and genuine low/high weighted main mass.