noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightRemainingFour (A : Finset ℕ) (N : ℕ) (z b c : ℝ) : ℤ

The four literal signed terms; no analytic estimate is part of their definition.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightRemainingFour A N z b c = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG6 A N z b + MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG7 A N z b c - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11 A N z b - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG12 A N z b c

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightRemainingFive_eq_remainingFour_sub_s5 (A : Finset ℕ) (N : ℕ) (z b c : ℝ) : goldbachWeightRemainingFive A N z b c = goldbachWeightRemainingFour A N z b c - goldbachS5Closed A N z (↑N ^ (1 / 3))

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightFourCoarseCoefficient (ε : ℝ) : ℝ

Coarse coefficient using the proved uniform-eight S5 bound; not the optimized G9 coefficient.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightFourCoarseCoefficient ε = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightFiveCoefficient ε - 8 * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9MainIntegral

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

The actual coarse S5 integral bound is consumed, without sign assumptions on the remaining four terms.

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

The small-epsilon quantifiers remain epsilon0 first, then a threshold for each epsilon.