noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedAPWindow (N : ℕ) (ε : ℝ) (m d b : ℕ) : Finset ℕ

Actual prime-r window with the coupled product congruence, before sieving the output.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedAPWindow N ε m d b = {r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow N ε m | m * r ≡ b [MOD d]}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedAPWindow_eq_sdiff {N m : ℕ} {ε : ℝ} (d b : ℕ) (hN : 2 ≤ N) (hm : m ∈ goldbachG11EffectiveProductSupport N ε) : goldbachG11LinkedAPWindow N ε m d b = Wu2004MeanValue.scaledPrimeSet (↑m * goldbachG11PiLiHi N m) d b m \ Wu2004MeanValue.scaledPrimeSet (↑m * goldbachG11PiLiLo N ε m) d b m

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedAPWindow_card_eq_inverse {N m : ℕ} {ε : ℝ} (d b : ℕ) (hN : 2 ≤ N) (hm : m ∈ goldbachG11EffectiveProductSupport N ε) (hmd : m.Coprime d) : ↑(goldbachG11LinkedAPWindow N ε m d b).card = ↑(AnalyticNumberTheory.Sieve.primesInAP ⌊goldbachG11PiLiHi N m⌋₊ d (AnalyticNumberTheory.Sieve.natInvMod d m * b % d)) - ↑(AnalyticNumberTheory.Sieve.primesInAP ⌊goldbachG11PiLiLo N ε m⌋₊ d (AnalyticNumberTheory.Sieve.natInvMod d m * b % d))

Exact count difference, retaining the closed high endpoint and inverse residue.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow_product_le {N m r : ℕ} {ε : ℝ} (hm : m ∈ goldbachG11EffectiveProductSupport N ε) (hr : r ∈ goldbachG11LinkedPrimeWindow N ε m) : r * m ≤ N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow_output_pos {N m r : ℕ} {ε : ℝ} (hm : m ∈ goldbachG11EffectiveProductSupport N ε) (hr : r ∈ goldbachG11LinkedPrimeWindow N ε m) : 0 < N - r * m

On the geometric mother, the actual output is positive, not truncated to zero.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedAPWindow_eq_output_dvd {N m : ℕ} {ε : ℝ} (d : ℕ) (hm : m ∈ goldbachG11EffectiveProductSupport N ε) : goldbachG11LinkedAPWindow N ε m d N = {r ∈ goldbachG11LinkedPrimeWindow N ε m | d ∣ N - r * m}

The progression counted by the source is literally divisibility of the output.