@[instance_reducible]

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachS1LowerRosser (P : Prop) : Decidable P

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachS1LowerRosser P = Classical.propDecidable P

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1BoundingSieve_lowerErrSum_le_prefixSum {N : ℕ} (hEven : Even N) {ε z : ℝ} (hε : 0 ≤ ε) (hm : 2 ≤ goldbachS1Endpoint N ε) {D Q0 : ℕ} (hDQ : D ≤ Q0 + 1) : LinearSieve.lowerErrSum (goldbachS1BoundingSieve N hEven ε z) D (LinearSieve.lowerRosserWeight (goldbachS1ProdPrimes N z) D) ≤ ∑ q ∈ Finset.Icc 1 Q0, BombieriVinogradov.standardPrimeAPPrefixMaxError N q

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1_lowerRosser_mainTerm_sub_prefix_le {N : ℕ} {ε z : ℝ} (hε0 : 0 < ε) (_hε1 : ε < 1) (hEven : Even N) (hm : 2 ≤ goldbachS1Endpoint N ε) (_hz : 2 ≤ z) {D Q0 : ℕ} (hprimeD : ∀ p ∈ (goldbachS1ProdPrimes N z).primeFactors, p < D) (hDQ : D ≤ Q0 + 1) : BombieriVinogradov.trueLogarithmicIntegral ↑(goldbachS1Endpoint N ε) * ∑ d ∈ (goldbachS1ProdPrimes N z).divisors, LinearSieve.lowerRosserWeight (goldbachS1ProdPrimes N z) D d / ↑d.totient - ∑ q ∈ Finset.Icc 1 Q0, BombieriVinogradov.standardPrimeAPPrefixMaxError N q ≤ ↑(goldbachS1 (goldbachDifferenceCarrier N ε) N z)

The genuine finite S1 carrier satisfies the lower Rosser inequality with the exact main sum and the honest standard prime-AP prefix remainder.