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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12UniformClosedConstant = 8 * (564383 / 1000000) * (Real.log (9 / 4) * (43 / 2 * Real.log (53 / 33) - 10))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_closedCrossIntegralLedger (δ : ℝ) (hδ : 0 < δ) : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 2 / 15 ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → (goldbachG67IntegralConstant + 124341093 / 200000000 - goldbachB9PaperSplitIntegral - 10385101 / 100000000 - goldbachG12UniformClosedConstant - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ 4 * ↑(D19 N)

Exact closed cross expression, retaining the strongest already proved C67.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_elementaryIntegralLedger (δ : ℝ) (hδ : 0 < δ) : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 2 / 15 ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → (4 * G67ElementaryIntegral.elementaryIntegral + 124341093 / 200000000 - goldbachB9PaperSplitIntegral - 10385101 / 100000000 - goldbachG12UniformClosedConstant - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ 4 * ↑(D19 N)

An auxiliary elementary lower ledger, not a numerical positivity assertion. The preceding theorem continues to retain the larger actual JR constant.