noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachFiniteError (A : Finset ℕ) (N : ℕ) (z y : ℝ) : ℤ

The actual finite error: noncoprime differences, square diagonal, repeated triples, and the closed upper endpoint. No size bound is built in.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachFiniteError A N z y = 2 * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachBadCount A N + MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachQ A N z y + MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachR A N z y + MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB6 A N z y

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachFiniteError_nonneg (A : Finset ℕ) (N : ℕ) (z y : ℝ) : 0 ≤ goldbachFiniteError A N z y

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbach_closed_sieve_lower_bound_eventually (ε : ℝ) (hε : 0 < ε) (hεupper : ε < 2 / 15) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∀ (κ σ : ℝ), 1 / 21 < κ → κ < σ → σ ≤ 1 / 3 → 2 * goldbachS1 (goldbachDifferenceCarrier N ε) N (↑N ^ κ) - 2 * goldbachS2 (goldbachDifferenceCarrier N ε) N (↑N ^ (9 / 19 - ε)) - goldbachS3Closed (goldbachDifferenceCarrier N ε) N (↑N ^ κ) (↑N ^ σ) - 2 * goldbachS4 (goldbachDifferenceCarrier N ε) N (↑N ^ σ) - goldbachS5Closed (goldbachDifferenceCarrier N ε) N (↑N ^ κ) (↑N ^ σ) + goldbachS6Closed (goldbachDifferenceCarrier N ε) N (↑N ^ κ) (↑N ^ σ) - goldbachFiniteError (goldbachDifferenceCarrier N ε) N (↑N ^ κ) (↑N ^ σ) ≤ 2 * ↑(D19 N)

The closed-endpoint finite Goldbachbig lower bound for the actual D19 count. The error is explicit and nonnegative, but its power-saving size and the positivity of the resulting lower bound are separate obligations.