theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridIndex_eq_of_bounds {ρ t : ℝ} (hρ : 1 < ρ) {i : ℕ} (hi : ρ ^ i ≤ t) (hiu : t < ρ ^ (i + 1)) : fouvryG9GridIndex ρ t = i

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Grid_rectangle_key {N : ℕ} {ε ρ : ℝ} (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (hbig : 4 ≤ ↑N ^ (4 / 53)) {k : ℕ × ℕ} (hk : k ∈ goldbachG11GridUsed N ε ρ) {v : ℕ × ℕ} (hv : v ∈ goldbachG11GridLong N ε ρ k ×ˢ goldbachG11GridShort N ρ k) : goldbachG11GridKey ρ v = k

The half-open endpoints give a unique key even for added rectangle points.

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ExpandedGridPairs N ε ρ = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridUsed N ε ρ).biUnion fun (k : ℕ × ℕ) => MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridLong N ε ρ k ×ˢ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridShort N ρ k

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11WeightedGridMass_eq_union {N : ℕ} {ε ρ : ℝ} (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (hbig : 4 ≤ ↑N ^ (4 / 53)) (h : ℝ → ℝ) : goldbachG11WeightedGridMass N ε ρ h = ∑ v ∈ goldbachG11ExpandedGridPairs N ε ρ, goldbachG11AllPrimeWeight N v * h (Real.log ↑v.2 / Real.log ↑N)

Forgetting grid keys loses no multiplicity: distinct boxes are disjoint.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ExpandedGridPairs_data {N : ℕ} {ε ρ : ℝ} (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (hbig : 4 ≤ ↑N ^ (4 / 53)) {v : ℕ × ℕ} (hv : v ∈ goldbachG11ExpandedGridPairs N ε ρ) : v.1 ∈ goldbachG11EffectiveProductSupport N ε ∧ ↑N ^ (4 / 53) ≤ ↑v.2 ∧ ↑v.2 < ρ * ↑v.1.minFac ∧ ↑v.1 * ↑v.2 < ρ ^ 2 * ↑N

The only geometric extensions are a multiplicative product endpoint rho^2N and a first/second-prime ordering collar p<rhominFac(m).