@[instance_reducible]

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

Equations

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

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9Pairs N = {rs ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Pairs N (↑N ^ (4 / 53)) | ↑rs.1 ≤ ↑N ^ (1 / 3) ∧ ↑N ^ (1 / 3) ≤ ↑rs.2}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachC9Pairs_iff {N : ℕ} {rs : ℕ × ℕ} : rs ∈ goldbachC9Pairs N ↔ Nat.Prime rs.1 ∧ Nat.Prime rs.2 ∧ (rs.1 * rs.2).Coprime N ∧ ↑N ^ (4 / 53) ≤ ↑rs.1 ∧ rs.1 ≤ rs.2 ∧ rs.1 * rs.2 ^ 2 ≤ N ∧ ↑rs.1 ≤ ↑N ^ (1 / 3) ∧ ↑N ^ (1 / 3) ≤ ↑rs.2

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9Pairs_subset_S4Pairs (N : ℕ) : goldbachC9Pairs N ⊆ goldbachS4Pairs N (↑N ^ (4 / 53))

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9Prod rs = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8Prod rs

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9Prod_pos {N : ℕ} {rs : ℕ × ℕ} (hrs : rs ∈ goldbachC9Pairs N) : 0 < goldbachC9Prod rs

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9Prod_injOn (N : ℕ) : Set.InjOn goldbachC9Prod ↑(goldbachC9Pairs N)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9Prod_support_bounds {N : ℕ} {rs : ℕ × ℕ} (hN : 2 ≤ N) (hrs : rs ∈ goldbachC9Pairs N) : ↑N ^ (65 / 159) ≤ ↑(goldbachC9Prod rs) ∧ ↑(goldbachC9Prod rs) ≤ ↑N ^ (2 / 3)

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9ProductSupport N = Finset.image MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9Prod (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9Pairs N)

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9ProductFiber N m = {rs ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9Pairs N | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9Prod rs = m}

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9Coeff N m = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9ProductFiber N m).card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9Coeff_le_one (N m : ℕ) : goldbachC9Coeff N m ≤ 1

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9Coeff_pos_iff {N m : ℕ} : 0 < goldbachC9Coeff N m ↔ m ∈ goldbachC9ProductSupport N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9ProductSupport_bounds {N m : ℕ} (hN : 2 ≤ N) (hm : m ∈ goldbachC9ProductSupport N) : ↑N ^ (65 / 159) ≤ ↑m ∧ ↑m ≤ ↑N ^ (2 / 3)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5Cutoff_twentieth_gt {N : ℕ} (hN : 2 ≤ N) : ↑N < (↑N ^ (4 / 53)) ^ 20

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9Pair_dvdFiber_card_le_fourHundred {N n : ℕ} (hn1 : 1 ≤ n) (hnN : n < N) : {rs ∈ goldbachC9Pairs N | goldbachC9Prod rs ∣ n}.card ≤ 400