@[instance_reducible]

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachS4CarrierGeometry (P : Prop) : Decidable P

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachS4CarrierGeometry P = Classical.propDecidable P

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachS4Pairs_iff {N : ℕ} {u : ℝ} {rs : ℕ × ℕ} : rs ∈ goldbachS4Pairs N u ↔ Nat.Prime rs.1 ∧ Nat.Prime rs.2 ∧ (rs.1 * rs.2).Coprime N ∧ u ≤ ↑rs.1 ∧ rs.1 ≤ rs.2 ∧ rs.1 * rs.2 ^ 2 ≤ N

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8Prod (rs : ℕ × ℕ) : ℕ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8Prod rs = rs.1 * rs.2

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8Prod_pos {N : ℕ} {u : ℝ} {rs : ℕ × ℕ} (hrs : rs ∈ goldbachS4Pairs N u) : 0 < goldbachC8Prod rs

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Pair_power_geometry {N : ℕ} {u : ℝ} {rs : ℕ × ℕ} (hrs : rs ∈ goldbachS4Pairs N u) : rs.1 ^ 3 ≤ N ∧ goldbachC8Prod rs ^ 2 ≤ rs.1 * N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8Prod_le_two_thirds {N : ℕ} {u : ℝ} {rs : ℕ × ℕ} (hN : 2 ≤ N) (hrs : rs ∈ goldbachS4Pairs N u) : ↑(goldbachC8Prod rs) ≤ ↑N ^ (2 / 3)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8Prod_support_bounds {N : ℕ} {rs : ℕ × ℕ} (hN : 2 ≤ N) (hrs : rs ∈ goldbachS4Pairs N (↑N ^ (3 / 11))) : ↑N ^ (6 / 11) ≤ ↑(goldbachC8Prod rs) ∧ ↑(goldbachC8Prod rs) ≤ ↑N ^ (2 / 3)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Cutoff_fourth_gt {N : ℕ} (hN : 2 ≤ N) : ↑N < (↑N ^ (3 / 11)) ^ 4

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8Prod_injOn {N : ℕ} {u : ℝ} : Set.InjOn goldbachC8Prod ↑(goldbachS4Pairs N u)

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8ProductSupport N = Finset.image MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8Prod (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Pairs N (↑N ^ (3 / 11)))

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8ProductFiber (N m : ℕ) : Finset (ℕ × ℕ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8ProductFiber N m = {rs ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Pairs N (↑N ^ (3 / 11)) | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8Prod rs = m}

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8Coeff N m = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8ProductFiber N m).card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8Coeff_le_one (N m : ℕ) : goldbachC8Coeff N m ≤ 1

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8Coeff_pos_iff {N m : ℕ} : 0 < goldbachC8Coeff N m ↔ m ∈ goldbachC8ProductSupport N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8ProductSupport_bounds {N m : ℕ} (hN : 2 ≤ N) (hm : m ∈ goldbachC8ProductSupport N) : ↑N ^ (6 / 11) ≤ ↑m ∧ ↑m ≤ ↑N ^ (2 / 3)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Pair_mem_largePrimeDivisors {N n : ℕ} {u : ℝ} {rs : ℕ × ℕ} (hn : n ≠ 0) (hrs : rs ∈ goldbachS4Pairs N u) (hd : goldbachC8Prod rs ∣ n) : rs ∈ (largePrimeDivisors n u).product (largePrimeDivisors n u)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Pair_dvdFiber_card_le_fourHundred {N n : ℕ} (hn1 : 1 ≤ n) (hnN : n < N) : {rs ∈ goldbachS4Pairs N (↑N ^ (3 / 11)) | goldbachC8Prod rs ∣ n}.card ≤ 400