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

The four signed terms minus the literal strict-low S5 sum. No low estimate is assumed.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightLowFirstRemainder A N z b c = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightRemainingFour A N z b c - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5ClosedBelow A N z (↑N ^ (1 / 3)) (↑N ^ (1 / 10))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightRemainingFive_eq_lowFirstRemainder_sub_high (A : Finset ℕ) (N : ℕ) (z b c : ℝ) (hz : z ≤ ↑N ^ (1 / 10)) : goldbachWeightRemainingFive A N z b c = goldbachWeightLowFirstRemainder A N z b c - goldbachS5Closed A N (↑N ^ (1 / 10)) (↑N ^ (1 / 3))

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightHighFirstCoefficient ε = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightFiveCoefficient ε - 8 * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighMainIntegral

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighMainIntegral_eq_singleIntegral : goldbachB9HighMainIntegral = ∫ (u : ℝ) in 1 / 10..1 / 3, Real.log (2 - 3 * u) / (u * (1 - u))

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

Only the proved high estimate is consumed; the low count remains visible in the left side.

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

epsilon0 is chosen first; the prime-size threshold may depend on the fixed epsilon.