noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryAPWindow (N m : ℕ) (L U : ℝ) (d : ℕ) : Finset ℕ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryAPWindow N m L U d = {p ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWInterval L U | Nat.Prime p ∧ m * p ≡ N [MOD d]}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryAPWindow_eq_sdiff (N m d : ℕ) {L U : ℝ} (hm : 0 < m) (hL : 0 ≤ L) (hLU : L ≤ U) : goldbachG11OrdinaryAPWindow N m L U d = Wu2004MeanValue.scaledPrimeSet (↑m * U) d N m \ Wu2004MeanValue.scaledPrimeSet (↑m * L) d N m

Half-open prime interval with the original product congruence.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryAPWindow_card_inverse (N m d : ℕ) {L U : ℝ} (hm : 0 < m) (hL : 0 ≤ L) (hLU : L ≤ U) (hmd : m.Coprime d) : ↑(goldbachG11OrdinaryAPWindow N m L U d).card = ↑(AnalyticNumberTheory.Sieve.primesInAP ⌊U⌋₊ d (AnalyticNumberTheory.Sieve.natInvMod d m * N % d)) - ↑(AnalyticNumberTheory.Sieve.primesInAP ⌊L⌋₊ d (AnalyticNumberTheory.Sieve.natInvMod d m * N % d))

Exact inverse residue and closed high endpoint, with no product≤N restriction.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryAPWindow_row (N m d : ℕ) (L U : ℝ) : (∑ p ∈ AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWInterval L U, AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta p * if d ∣ (↑N - ↑m * ↑p).natAbs then 1 else 0) = ↑(goldbachG11OrdinaryAPWindow N m L U d).card

The literal absolute-difference divisibility row, including the zero and negative-side possibilities, is the same finite prime AP window.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryAPWindow_empty_of_not_coprime (N m d : ℕ) (L U : ℝ) (hNd : N.Coprime d) (hmd : ¬m.Coprime d) : goldbachG11OrdinaryAPWindow N m L U d = ∅