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

Certified negative scalar entries; the lower-sieve and S3 integrals are not estimated.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightThreeNegativeScalarCoefficient = Real.exp (-Real.eulerMascheroniConstant) * (159 / 2 * MathlibNt.SieveTheory.SwitchingPrinciple.dimensionOneLowerLinearSieveFactor 6 + 33 / 2 * MathlibNt.SieveTheory.SwitchingPrinciple.dimensionOneLowerLinearSieveFactor (33 / 8)) - 53 / 2 * Real.exp (-Real.eulerMascheroniConstant) * (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_primeKernelIntegral (1 / 3) + MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_primeKernelIntegral (3 / 11)) - 4 * (84289 / 100000) - 540996 / 100000 - 2 * (60962 / 100000)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightThreeNegativeScalarCoefficient_le : goldbachWeightThreeNegativeScalarCoefficient ≤ goldbachWeightSixCoefficient 0 - 2 * (60962 / 100000)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_remainingFive_threeNegativeScalars_small_epsilon (δ : ℝ) (hδ : 0 < δ) : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 2 / 15 ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachWeightRemainingFive (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11))) + (goldbachWeightThreeNegativeScalarCoefficient - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ 4 * ↑(D19 N)

Actual D19 signed bound with the three certified negative constants. No positivity of the remaining count or of the coefficient is assumed or asserted.