@[instance_reducible]

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

Equations

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

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2PrimePairs (N : ℕ) (ε T : ℝ) : Finset (ℕ × ℕ)

The actual ordered prime-pair carrier attached to S2 on the literal difference set: n = r*q with r ≤ q, both primes retained as labels, and N - r*q a strict prime partner.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2PrimePairs N ε T = {rq ∈ (Finset.range (N + 1)).product (Finset.range (N + 1)) | Nat.Prime rq.1 ∧ Nat.Prime rq.2 ∧ T ≤ ↑rq.1 ∧ ↑rq.1 ≤ ↑rq.2 ∧ rq.1 ^ 2 ≤ N ∧ (rq.1 * rq.2).Coprime N ∧ ε * ↑N < ↑rq.1 * ↑rq.2 ∧ ↑rq.1 * ↑rq.2 < ↑N ∧ Nat.Prime (N - rq.1 * rq.2)}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachS2PrimePairs_iff {N : ℕ} {ε T : ℝ} {rq : ℕ × ℕ} : rq ∈ goldbachS2PrimePairs N ε T ↔ Nat.Prime rq.1 ∧ Nat.Prime rq.2 ∧ T ≤ ↑rq.1 ∧ ↑rq.1 ≤ ↑rq.2 ∧ rq.1 ^ 2 ≤ N ∧ (rq.1 * rq.2).Coprime N ∧ ε * ↑N < ↑rq.1 * ↑rq.2 ∧ ↑rq.1 * ↑rq.2 < ↑N ∧ Nat.Prime (N - rq.1 * rq.2)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2PrimePairs_point_le_one (N n : ℕ) (T : ℝ) : goldbachS2Point N T n ≤ 1

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2PrimePairs_bridge (N : ℕ) (ε T : ℝ) (hN : 2 ≤ N) (hε : 0 < ε) (hε1 : ε < 1) (hT : 0 < T) (hcube : ↑N < T ^ 3) (hsqrt : √↑N ≤ ε * ↑N) : ↑(goldbachS2PrimePairs N ε T).card ≤ goldbachS2 (goldbachDifferenceCarrier N ε) N T ∧ goldbachS2 (goldbachDifferenceCarrier N ε) N T ≤ ↑(goldbachS2PrimePairs N ε T).card + ↑N.primeFactors.card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2PrimePairs_bridge_eventually (ε : ℝ) (hε : 0 < ε) (hε15 : ε < 2 / 15) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → have T := ↑N ^ (9 / 19 - ε); ↑(goldbachS2PrimePairs N ε T).card ≤ goldbachS2 (goldbachDifferenceCarrier N ε) N T ∧ goldbachS2 (goldbachDifferenceCarrier N ε) N T ≤ ↑(goldbachS2PrimePairs N ε T).card + ↑N.primeFactors.card