MathlibNt.SieveTheory.LiLiuGoldbachG11ExceptionFibers

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelCoordinates (v : GoldbachG11Label) :

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelCoordinates v = (v.snd.snd.fst, v.snd.snd.snd, v.snd.fst, v.fst)

Instances For

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelCoordinates_injective :

Function.Injective goldbachG11LabelCoordinates

Inspect dependencies

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

source

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

Finset GoldbachG11Label

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11DivisorFiber N n = {v ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelProd v ∣ n}

Instances For

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelCoordinates_mem_largePrimeDivisors {N n : ℕ} {v : GoldbachG11Label} (hn : n ≠ 0) (hv : v ∈ goldbachG11DivisorFiber N n) :

goldbachG11LabelCoordinates v ∈ (largePrimeDivisors n (↑N ^ (4 / 53))).product ((largePrimeDivisors n (↑N ^ (4 / 53))).product ((largePrimeDivisors n (↑N ^ (4 / 53))).product (largePrimeDivisors n (↑N ^ (4 / 53)))))

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11DivisorFiber_card_le {N n : ℕ} (hn1 : 1 ≤ n) (hnN : n < N) :

(goldbachG11DivisorFiber N n).card ≤ 160000

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_difference_strict_bounds {N n : ℕ} {eps : ℝ} (heps : 0 ≤ eps) (hn : n ∈ goldbachDifferenceCarrier N eps) :

1 ≤ n ∧ n < N

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RSquareCount_sum_le (N : ℕ) (eps : ℝ) (heps : 0 ≤ eps) :

∑ v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), goldbachG11RSquareCount (goldbachDifferenceCarrier N eps) v ≤ 160000 * goldbachS5SquareCount N

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11NCount_sum_le (N : ℕ) (eps : ℝ) (heps : 0 ≤ eps) :

∑ v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), goldbachG11NCount (goldbachDifferenceCarrier N eps) N v ≤ 160000 * goldbachBadCount (goldbachDifferenceCarrier N eps) N

Inspect dependencies

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