MathlibNt.SieveTheory.LiLiuGoldbachS1LevelSix

source

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1LevelSixZ (N : ℕ) :

ℕ

The fixed lower-sieve endpoint from the original α = 4 / 53 geometry.

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1LevelSixZ N = ⌈↑N ^ (4 / 53)⌉₊

Instances For

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1LevelSixZ · compiled type and proof/definition references.

source

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1LevelSixD (N : ℕ) :

ℕ

The corresponding s = 6 sieve level D = Z^6.

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1LevelSixD N = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1LevelSixZ N ^ 6

Instances For

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1LevelSixD · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1LevelSix_two_le_Z {N : ℕ} (hN : 2 ≤ N) :

2 ≤ S1LevelSixZ N

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1LevelSix_two_le_Z · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1LevelSix_two_le_D {N : ℕ} (hN : 2 ≤ N) :

2 ≤ S1LevelSixD N

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1LevelSix_two_le_D · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1LevelSix_panModulusCutoff_eventually (B : ℝ) (_hB : 0 ≤ B) :

∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → 2 ≤ S1LevelSixZ N ∧ 2 ≤ S1LevelSixD N ∧ S1LevelSixD N ≤ LiuWeight.panModulusCutoff N B + 1

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1LevelSix_panModulusCutoff_eventually · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1LevelSix_ceil_rootD_eq_Z (N : ℕ) :

⌈↑(S1LevelSixD N) ^ (1 / 6)⌉₊ = S1LevelSixZ N

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1LevelSix_ceil_rootD_eq_Z · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1LevelSix_logD_div_logZ_eq_six {N : ℕ} (hZ : 2 ≤ S1LevelSixZ N) :

Real.log ↑(S1LevelSixD N) / Real.log ↑(S1LevelSixZ N) = 6

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1LevelSix_logD_div_logZ_eq_six · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1LevelSix_lt_Z_of_lt_rpow {N ℓ : ℕ} (hℓ : ↑ℓ < ↑N ^ (4 / 53)) :

ℓ < S1LevelSixZ N

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1LevelSix_lt_Z_of_lt_rpow · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1LevelSix_lt_powSix_of_lt {Z p : ℕ} (hZ : 2 ≤ Z) (hp : p < Z) :

p < Z ^ 6

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1LevelSix_lt_powSix_of_lt · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1LevelSix_lt_D_of_lt_Z {N p : ℕ} (hZ : 2 ≤ S1LevelSixZ N) (hp : p < S1LevelSixZ N) :

p < S1LevelSixD N

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1LevelSix_lt_D_of_lt_Z · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1LevelSix_primeFactor_lt_D {N p : ℕ} (hN : 2 ≤ N) (hp : Nat.Prime p) (hpP : p ∣ goldbachB10ProdPrimes N (↑N ^ (4 / 53))) :

p < S1LevelSixD N

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S1LevelSix_primeFactor_lt_D · compiled type and proof/definition references.