noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongLabels (N : ℕ) (ρ : ℝ) (k : ℕ × ℕ × ℕ) : Finset (ℕ × ℕ)

The rectangular long labels. There is deliberately no short variable, curved cutoff, or coprimality condition on the second prime.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongLabels N ρ k = {z ∈ Finset.range (N + 1) ×ˢ Finset.range (N + 1) | Nat.Prime z.1 ∧ Nat.Prime z.2 ∧ z.1.Coprime N ∧ ↑N ^ (1 / 3) ≤ ↑z.1 ∧ ρ ^ k.2.1 ≤ ↑z.1 ∧ ↑z.1 < ρ ^ (k.2.1 + 1) ∧ ρ ^ k.2.2 ≤ ↑z.2 ∧ ↑z.2 < ρ ^ (k.2.2 + 1)}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongProducts (N : ℕ) (ρ : ℝ) (k : ℕ × ℕ × ℕ) : Finset ℕ

Distinct products; multiplicities remain in fouvryG9LongAlpha.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongProducts N ρ k = Finset.image (fun (z : ℕ × ℕ) => z.1 * z.2) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongLabels N ρ k)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongAlpha (N : ℕ) (ρ : ℝ) (k : ℕ × ℕ × ℕ) (m : ℕ) : ℝ

A rectangular coefficient independent of the short coordinate.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongAlpha N ρ k m = ↑{z ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongLabels N ρ k | z.1 * z.2 = m}.card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongAlpha_nonneg (N : ℕ) (ρ : ℝ) (k : ℕ × ℕ × ℕ) (m : ℕ) : 0 ≤ fouvryG9LongAlpha N ρ k m

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongAlpha_le_divisors (N : ℕ) (ρ : ℝ) (k : ℕ × ℕ × ℕ) (m : ℕ) : fouvryG9LongAlpha N ρ k m ≤ ↑m.divisors.card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongAlpha_firstIndex_eq (N : ℕ) (ρ : ℝ) (i i' j l m : ℕ) : fouvryG9LongAlpha N ρ (i, j, l) m = fouvryG9LongAlpha N ρ (i', j, l) m

Neither the short label nor even its grid index enters the long coefficient.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongAlpha_bounds (N : ℕ) (ρ : ℝ) (k : ℕ × ℕ × ℕ) (m : ℕ) : 0 ≤ fouvryG9LongAlpha N ρ k m ∧ fouvryG9LongAlpha N ρ k m ≤ ↑m.divisors.card ∧ ↑m.divisors.card = ↑((AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau 2) m)

The full divisor-bound contract, including the ordered-divisor normalization.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Long_sum (N : ℕ) (ρ : ℝ) (k : ℕ × ℕ × ℕ) (F : ℕ → ℕ → ℝ) (n : ℕ) : ∑ z ∈ fouvryG9LongLabels N ρ k, F n (z.1 * z.2) = ∑ m ∈ fouvryG9LongProducts N ρ k, fouvryG9LongAlpha N ρ k m * F n m

Regrouping preserves every ordered prime label, for arbitrary signed kernels.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongProducts_bounds {N : ℕ} {ρ : ℝ} (hρ : 1 < ρ) {k : ℕ × ℕ × ℕ} {m : ℕ} (hm : m ∈ fouvryG9LongProducts N ρ k) : ρ ^ (k.2.1 + k.2.2) ≤ ↑m ∧ ↑m < ρ ^ 2 * ρ ^ (k.2.1 + k.2.2)

The support is a genuine rectangular long interval.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongProducts_le_two {N : ℕ} {ρ : ℝ} (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) {k : ℕ × ℕ × ℕ} {m : ℕ} (hm : m ∈ fouvryG9LongProducts N ρ k) : ↑m ≤ 2 * ρ ^ (k.2.1 + k.2.2)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongLabels_of_cell {N : ℕ} {eps ρ : ℝ} (hρ : 1 < ρ) {k y : ℕ × ℕ × ℕ} (hy : y ∈ fouvryG9GridCell N eps ρ k) : (y.2.1, y.1 / y.2.1) ∈ fouvryG9LongLabels N ρ k

Actual cell labels enter the positive rectangular cover. The second prime is not required to be coprime to N.