def G12ClippedWindow.Admissible (N : ℕ) (ε : ℝ) (g L U : ℕ → ℝ) : Prop

The coefficient and endpoints are common to every modulus.

Equations

• G12ClippedWindow.Admissible N ε g L U = ∀ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, (0 ≤ g m ∧ g m ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N m) ∧ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiLo N ε m ≤ L m ∧ L m ≤ U m ∧ U m ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiHi N m

noncomputable def G12ClippedWindow.window (N : ℕ) (L U : ℕ → ℝ) (m : ℕ) : Finset ℕ

Literal prime Ioc, with the original finite ambient carrier.

Equations

• G12ClippedWindow.window N L U m = {r ∈ Finset.range (N + 1) | Nat.Prime r ∧ L m < ↑r ∧ ↑r ≤ U m}

theorem G12ClippedWindow.window_subset {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} (h : Admissible N ε g L U) {m : ℕ} (hm : m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N) : window N L U m ⊆ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow N ε m

theorem G12ClippedWindow.endpoint_nonneg {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} (hN : 2 ≤ N) (h : Admissible N ε g L U) {m : ℕ} (hm : m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N) : 0 ≤ L m ∧ 0 ≤ U m

theorem G12ClippedWindow.apWindow_eq_sdiff {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} {m : ℕ} (h : Admissible N ε g L U) (d b : ℕ) (hN : 2 ≤ N) (hm : m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N) : {r ∈ window N L U m | m * r ≡ b [MOD d]} = Wu2004MeanValue.scaledPrimeSet (↑m * U m) d b m \ Wu2004MeanValue.scaledPrimeSet (↑m * L m) d b m

theorem G12ClippedWindow.apWindow_card_eq_inverse {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} {m : ℕ} (h : Admissible N ε g L U) (d b : ℕ) (hN : 2 ≤ N) (hm : m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N) (hmd : m.Coprime d) : ↑{r ∈ window N L U m | m * r ≡ b [MOD d]}.card = ↑(AnalyticNumberTheory.Sieve.primesInAP ⌊U m⌋₊ d (AnalyticNumberTheory.Sieve.natInvMod d m * b % d)) - ↑(AnalyticNumberTheory.Sieve.primesInAP ⌊L m⌋₊ d (AnalyticNumberTheory.Sieve.natInvMod d m * b % d))

Actual AP cardinality: the high window has the unchanged inverse residue.

theorem G12ClippedWindow.window_card {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} (hN : 2 ≤ N) (h : Admissible N ε g L U) {m : ℕ} (hm : m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N) : ↑(window N L U m).card = AnalyticNumberTheory.LargeSieve.PanPrincipal.primeCount ⌊U m⌋₊ - AnalyticNumberTheory.LargeSieve.PanPrincipal.primeCount ⌊L m⌋₊