noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1BetaGeometryD (N : ℕ) (s : ℝ) : ℕ

The natural lower-sieve level attached to the fixed beta = 4 / 33 and arbitrary fixed 4 ≤ s < 33 / 8.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1BetaGeometryD N s = ⌈↑N ^ (4 / 33 * s)⌉₊

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1BetaGeometryZeta (N : ℕ) (s : ℝ) : ℝ

The genuine real Suzuki endpoint attached to S1BetaGeometryD.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1BetaGeometryZeta N s = ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1BetaGeometryD N s) ^ (1 / s)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1BetaGeometryZ (N : ℕ) (s : ℝ) : ℕ

The natural Suzuki endpoint obtained by transporting the genuine real root through Nat.ceil.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1BetaGeometryZ N s = ⌈MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1BetaGeometryZeta N s⌉₊

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1BetaGeometry_two_le_D {N : ℕ} {s : ℝ} (hN : 2 ≤ N) (hs : 0 < s) : 2 ≤ S1BetaGeometryD N s

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1BetaGeometry_one_lt_zeta {N : ℕ} {s : ℝ} (hD : 2 ≤ S1BetaGeometryD N s) (hs : 0 < s) : 1 < S1BetaGeometryZeta N s

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1BetaGeometry_two_le_Z {N : ℕ} {s : ℝ} (hD : 2 ≤ S1BetaGeometryD N s) (hs : 0 < s) : 2 ≤ S1BetaGeometryZ N s

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1BetaGeometry_rpow_le_zeta {N : ℕ} {s : ℝ} (hs : 0 < s) : ↑N ^ (4 / 33) ≤ S1BetaGeometryZeta N s

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1BetaGeometry_zeta_le_rpow_eventually (s η : ℝ) (hs4 : 4 ≤ s) (hη : 0 < η) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → S1BetaGeometryZeta N s ≤ ↑N ^ (4 / 33 + η)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1BetaGeometry_eventually_ge_constant (s R : ℝ) (hs : 0 < s) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → R ≤ ↑(S1BetaGeometryD N s)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1BetaGeometry_panModulusCutoff_eventually (s B : ℝ) (hs4 : 4 ≤ s) (hslt : s < 33 / 8) (_hB : 0 ≤ B) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → 2 ≤ S1BetaGeometryD N s ∧ 1 < S1BetaGeometryZeta N s ∧ 2 ≤ S1BetaGeometryZ N s ∧ S1BetaGeometryD N s ≤ LiuWeight.panModulusCutoff N B + 1

@[simp]

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1BetaGeometry_ceil_zeta_eq_Z (N : ℕ) (s : ℝ) : ⌈S1BetaGeometryZeta N s⌉₊ = S1BetaGeometryZ N s

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1BetaGeometry_logD_div_logZeta_eq_s {N : ℕ} {s : ℝ} (hD : 2 ≤ S1BetaGeometryD N s) (hs : 0 < s) : Real.log ↑(S1BetaGeometryD N s) / Real.log (S1BetaGeometryZeta N s) = s

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1BetaGeometry_Z_le_D {N : ℕ} {s : ℝ} (hD : 2 ≤ S1BetaGeometryD N s) (hs1 : 1 ≤ s) : S1BetaGeometryZ N s ≤ S1BetaGeometryD N s

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1BetaGeometry_lt_D_of_lt_zeta {N p : ℕ} {s : ℝ} (hD : 2 ≤ S1BetaGeometryD N s) (hs1 : 1 ≤ s) (hp : ↑p < S1BetaGeometryZeta N s) : p < S1BetaGeometryD N s

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1BetaGeometry_lt_D_of_lt_Z {N p : ℕ} {s : ℝ} (hD : 2 ≤ S1BetaGeometryD N s) (hs1 : 1 ≤ s) (hp : p < S1BetaGeometryZ N s) : p < S1BetaGeometryD N s

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1BetaGeometry_primeFactor_lt_D {N p : ℕ} {s : ℝ} (hN : 2 ≤ N) (hs4 : 4 ≤ s) (hp : Nat.Prime p) (hpP : p ∣ goldbachS1ProdPrimes N (S1BetaGeometryZeta N s)) : p < S1BetaGeometryD N s

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1BetaGeometry_threshold (s B η : ℝ) (hs4 : 4 ≤ s) (hslt : s < 33 / 8) (hB : 0 ≤ B) (hη : 0 < η) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → 2 ≤ S1BetaGeometryD N s ∧ 1 < S1BetaGeometryZeta N s ∧ 2 ≤ S1BetaGeometryZ N s ∧ ↑N ^ (4 / 33) ≤ S1BetaGeometryZeta N s ∧ S1BetaGeometryZeta N s ≤ ↑N ^ (4 / 33 + η) ∧ S1BetaGeometryD N s ≤ LiuWeight.panModulusCutoff N B + 1 ∧ Real.log ↑(S1BetaGeometryD N s) / Real.log (S1BetaGeometryZeta N s) = s ∧ ∀ p < S1BetaGeometryZ N s, p < S1BetaGeometryD N s