def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Coordinates (x : (_ : ℕ × ℕ) × ℕ) : ℕ × ℕ × ℕ

Keep the second prime as a label after grouping the long product.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Coordinates x = (x.fst.2 * x.snd, x.fst.2, x.fst.1)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Carrier (N : ℕ) (eps : ℝ) : Finset (ℕ × ℕ × ℕ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Carrier N eps = Finset.image MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Coordinates (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LowPositivePrefixAtoms N eps)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Coordinates_injOn (N : ℕ) (eps : ℝ) : Set.InjOn fouvryG9Coordinates ↑(goldbachB9LowPositivePrefixAtoms N eps)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9_sum_reindex (N : ℕ) (eps : ℝ) (F : ℕ → ℕ → ℝ) : ∑ x ∈ goldbachB9LowPositivePrefixAtoms N eps, F x.fst.1 (x.fst.2 * x.snd) = ∑ y ∈ fouvryG9Carrier N eps, F y.2.2 y.1

Arbitrary kernels can be reindexed without merging two possible prime labels.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Carrier_geometry {N : ℕ} {eps : ℝ} {y : ℕ × ℕ × ℕ} (hy : y ∈ fouvryG9Carrier N eps) : Nat.Prime y.2.1 ∧ Nat.Prime y.2.2 ∧ y.2.1 ∣ y.1 ∧ Nat.Prime (y.1 / y.2.1) ∧ (y.2.2 * y.2.1).Coprime N ∧ ↑N ^ (4 / 53) ≤ ↑y.2.2 ∧ ↑y.2.2 < ↑N ^ (1 / 10) ∧ ↑N ^ (1 / 3) ≤ ↑y.2.1 ∧ y.2.2 * y.2.1 ^ 2 ≤ N ∧ eps * ↑N < ↑(y.2.2 * y.1) ∧ y.2.2 * y.1 < N

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Multiplicity (N : ℕ) (eps : ℝ) (n m : ℕ) : ℕ

The actual long-coordinate weight never exceeds the number of divisors.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Multiplicity N eps n m = {y ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Carrier N eps | y.1 = m ∧ y.2.2 = n}.card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Multiplicity_le_divisors (N : ℕ) (eps : ℝ) (n m : ℕ) : fouvryG9Multiplicity N eps n m ≤ m.divisors.card