noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9SievePrimes (N : ℕ) (z : ℝ) : Finset ℕ

Exactly the primes strictly below z that do not divide the actual N.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9SievePrimes N z = {p ∈ Finset.range ⌈z⌉₊ | Nat.Prime p ∧ p.Coprime N}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9SievePrimes_mem (N p : ℕ) (z : ℝ) : p ∈ fouvryG9SievePrimes N z ↔ Nat.Prime p ∧ p.Coprime N ∧ ↑p < z

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9MotherSifted (N : ℕ) (e : ℝ) (P : Finset ℕ) : ℝ

Actual labelled mother count with a common sieve carrier; no label is merged.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9MotherSifted N e P = ∑ a ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LowPositivePrefixAtoms N e, if (↑N - ↑(a.fst.2 * a.snd) * ↑a.fst.1).natAbs.Coprime (P.prod id) then 1 else 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9MotherSifted_le_rectangles {N : ℕ} {e ρ : ℝ} (hN : 1 ≤ N) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (P : Finset ℕ) (hbig : ∀ k ∈ fouvryG9GridUsed N e ρ, 3 ≤ ρ ^ k.1) : fouvryG9MotherSifted N e P ≤ ∑ k ∈ fouvryG9GridUsed N e ρ, fouvryG9RectangleSifted N ρ k P

Positive coverage transfers literal mother sieving into the actual rectangles.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9MotherSifted_total (A : ℕ) {e ε δ η ρ : ℝ} (he : 0 < e) (he1 : e ≤ 1) (hε : 0 < ε) (hεa : ε < 4 / 53) (hεδ : ε < δ) (hδ : δ < 1 / 2) (hη : 0 < η) (hηu : η < 1 / 8) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) : ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → ∀ (z : ℝ), fouvryG9MotherSifted N e (fouvryG9SievePrimes N z) ≤ ∑ k ∈ fouvryG9GridUsed N e ρ, fouvryG9RectangleMain N ρ δ η k (fouvryG9SievePrimes N z) z + ↑N / Real.log ↑N ^ A

A genuine mother-set upper sieve with the literal prime carrier. The only remaining main-term task is the analytic estimate of the displayed densities.