noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachQuadrupleDivisorFiber (N n : ℕ) (b : ℝ) : Finset GoldbachG11Label

Equations

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachQuadrupleCoordinates_mem_largePrimeDivisors {N n : ℕ} {b : ℝ} {v : GoldbachG11Label} (hn : n ≠ 0) (hv : v ∈ goldbachQuadrupleDivisorFiber N n b) : 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)))))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachQuadrupleDivisorFiber_card_le {N n : ℕ} {b : ℝ} (hn1 : 1 ≤ n) (hnN : n < N) : (goldbachQuadrupleDivisorFiber N n b).card ≤ 160000

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachQuadrupleRSquareCount_sum_le (N : ℕ) (eps b : ℝ) (heps : 0 ≤ eps) : ∑ v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) b, goldbachG11RSquareCount (goldbachDifferenceCarrier N eps) v ≤ 160000 * goldbachS5SquareCount N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachQuadrupleNCount_sum_le (N : ℕ) (eps b : ℝ) (heps : 0 ≤ eps) : ∑ v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) b, goldbachG11NCount (goldbachDifferenceCarrier N eps) N v ≤ 160000 * goldbachBadCount (goldbachDifferenceCarrier N eps) N