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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridProfileLo N ρ k = ↑⌈max (ρ ^ k.1) (↑N ^ (4 / 53))⌉ - 1

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridProfileHi (ρ : ℝ) (k : ℕ × ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridProfileHi ρ k = ↑⌈ρ ^ (k.1 + 1)⌉ - 1

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridShort_eq_profiles (N : ℕ) (ρ : ℝ) (k : ℕ × ℕ) : goldbachG11GridShort N ρ k = AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWInterval (goldbachG11GridProfileLo N ρ k) (goldbachG11GridProfileHi ρ k)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridLong_balanced_fourN {N m : ℕ} {ε ρ : ℝ} {k : ℕ × ℕ} (hN : 4 ≤ N) (hm : m ∈ goldbachG11GridLong N ε ρ k) : (4 * ↑N) ^ (2 / 53) ≤ ↑m ∧ ↑m ≤ (4 * ↑N) ^ (1 - 2 / 53)

Move to analysis size 4N without changing the original coefficient or residue N. The already proved eta=2/53 common-profile source fits this support.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Grid_profiles_fourN {N m : ℕ} {ε ρ : ℝ} (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (hbig : 4 ≤ ↑N ^ (4 / 53)) {k : ℕ × ℕ} (hk : k ∈ goldbachG11GridUsed N ε ρ) (hm : m ∈ goldbachG11GridLong N ε ρ k) : (2 ≤ goldbachG11GridProfileHi ρ k ∧ ↑m * goldbachG11GridProfileHi ρ k ≤ 4 * ↑N) ∧ (2 ≤ goldbachG11GridProfileLo N ρ k ∧ ↑m * goldbachG11GridProfileLo N ρ k ≤ 4 * ↑N) ∧ goldbachG11GridProfileLo N ρ k ≤ goldbachG11GridProfileHi ρ k

Both complete prime-count profiles obey the same enlarged-size budget.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductCoefficient_abs_le_400 (N m : ℕ) : |↑(goldbachG11ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m)| ≤ 400