noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3BoundingSieve (N : ℕ) (hEven : Even N) (ε z : ℝ) (p : ℕ) : BoundingSieve

The genuine difference carrier conditioned by divisibility by p; the sieve still acts on n, not on n / p.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3BoundingSieve N hEven ε z p = { support := {n ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.goldbachDifferenceCarrier N ε | p ∣ n}, prodPrimes := (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1BoundingSieve N hEven ε z).prodPrimes, prodPrimes_squarefree := ⋯, weights := (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1BoundingSieve N hEven ε z).weights, weights_nonneg := ⋯, totalMass := MathlibNt.SieveTheory.BombieriVinogradov.trueLogarithmicIntegral ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1Endpoint N ε) / ↑p.totient, nu := (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1BoundingSieve N hEven ε z).nu, nu_mult := ⋯, nu_pos_of_prime := ⋯, nu_lt_one_of_prime := ⋯ }

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_coprime_of_dvd_prodPrimes {N p d : ℕ} {z y : ℝ} (hp : p ∈ goldbachClosedPrimes N z y) (hd : d ∣ goldbachS1ProdPrimes N z) : p.Coprime d

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3BoundingSieve_siftedSum_eq {N : ℕ} (hEven : Even N) (ε z : ℝ) (p : ℕ) : BoundingSieve.siftedSum = ↑(literalH (goldbachDifferenceCarrier N ε) N p z)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3BoundingSieve_multSum_eq_primesInAP {N : ℕ} (hEven : Even N) {ε z y : ℝ} {p d : ℕ} (hε : 0 ≤ ε) (hm : 2 ≤ goldbachS1Endpoint N ε) (hp : p ∈ goldbachClosedPrimes N z y) (hd : d ∣ goldbachS1ProdPrimes N z) : BoundingSieve.multSum d = ↑(BombieriVinogradov.primesInAP (goldbachS1Endpoint N ε) (p * d) (N % (p * d)))

The product-modulus identity is restricted to the coprime sieve support.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3BoundingSieve_mainSum_eq_totientSum {N : ℕ} (hEven : Even N) (ε z : ℝ) (p : ℕ) (μ : ℕ → ℝ) : BoundingSieve.mainSum μ = ∑ d ∈ (goldbachS1ProdPrimes N z).divisors, μ d / ↑d.totient

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3BoundingSieve_rem_eq_standardPrimeAPError {N : ℕ} (hEven : Even N) {ε z y : ℝ} {p d : ℕ} (hε : 0 ≤ ε) (hm : 2 ≤ goldbachS1Endpoint N ε) (hp : p ∈ goldbachClosedPrimes N z y) (hd : d ∣ goldbachS1ProdPrimes N z) : BoundingSieve.rem d = BombieriVinogradov.standardPrimeAPError (goldbachS1Endpoint N ε) (p * d) (N % (p * d))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_mod_mem_unitResidues {N p d : ℕ} {z y : ℝ} (hp : p ∈ goldbachClosedPrimes N z y) (hd : d ∣ goldbachS1ProdPrimes N z) : N % (p * d) ∈ AnalyticNumberTheory.Sieve.unitResidues (p * d)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3BoundingSieve_abs_rem_le_prefix {N : ℕ} (hEven : Even N) {ε z y : ℝ} {p d : ℕ} (hε : 0 ≤ ε) (hm : 2 ≤ goldbachS1Endpoint N ε) (hp : p ∈ goldbachClosedPrimes N z y) (hd : d ∣ goldbachS1ProdPrimes N z) : |BoundingSieve.rem d| ≤ BombieriVinogradov.standardPrimeAPPrefixMaxError N (p * d)