@[instance_reducible]

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidablePropB9HighFirstLogGrid (p : Prop) : Decidable p

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidablePropB9HighFirstLogGrid p = Classical.propDecidable p

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighLogGridCells (n : ℕ) : Finset (Fin n × Fin n)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighLogGridCells n = {q ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridCells n | 1 / 10 ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridPoint n (↑q.1 + 1)}

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighLogGridMajorant n N = ∑ q ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighLogGridCells n, 1 / (1 - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridPoint n (↑q.1 + 1) - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BetaGridPoint n (↑q.2 + 1)) * MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.primeReciprocalLogRectangle N (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridPoint n ↑q.1) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridPoint n (↑q.1 + 1)) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BetaGridPoint n ↑q.2) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BetaGridPoint n (↑q.2 + 1))

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighLogGridUpperSum (n : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighLogGridUpperSum n = ∑ q ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighLogGridCells n, 1 / (1 - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridPoint n (↑q.1 + 1) - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BetaGridPoint n (↑q.2 + 1)) * MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.logarithmicRectangleMass (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridPoint n ↑q.1) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridPoint n (↑q.1 + 1)) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BetaGridPoint n ↑q.2) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BetaGridPoint n (↑q.2 + 1))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighLogGridCells_subset (n : ℕ) : goldbachB9HighLogGridCells n ⊆ goldbachB9LogGridCells n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachB9HighLogGridCells_iff {n : ℕ} {q : Fin n × Fin n} : q ∈ goldbachB9HighLogGridCells n ↔ 1 / 10 ≤ goldbachB9AlphaGridPoint n (↑q.1 + 1) ∧ 1 / 3 ≤ goldbachB9BetaGridPoint n (↑q.2 + 1) ∧ goldbachB9AlphaGridPoint n ↑q.1 + 2 * goldbachB9BetaGridPoint n ↑q.2 < 1

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighPairs_subset (N : ℕ) (hN : 2 ≤ N) : goldbachC10Pairs N (↑N ^ (1 / 10)) (↑N ^ (1 / 3)) ⊆ goldbachC10Pairs N (↑N ^ (4 / 53)) (↑N ^ (1 / 3))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighPair_logGeometry {N : ℕ} (hN : 2 ≤ N) {rs : ℕ × ℕ} (hrs : rs ∈ goldbachC10Pairs N (↑N ^ (1 / 10)) (↑N ^ (1 / 3))) : 1 / 10 ≤ LiuWeight.primeLogExponent N rs.1 ∧ LiuWeight.primeLogExponent N rs.1 ≤ 1 / 3 ∧ 1 / 3 ≤ LiuWeight.primeLogExponent N rs.2 ∧ LiuWeight.primeLogExponent N rs.1 + 2 * LiuWeight.primeLogExponent N rs.2 ≤ 1

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachK9High_eq_logCoordinateSum (N : ℕ) (hN : 2 ≤ N) : goldbachK9High N = ∑ rs ∈ goldbachC10Pairs N (↑N ^ (1 / 10)) (↑N ^ (1 / 3)), LiuWeight.liuPairLogKernel N rs

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighPairs_covered_by_logGrid (n N : ℕ) (hn : 0 < n) (hN : 2 ≤ N) {rs : ℕ × ℕ} (hrs : rs ∈ goldbachC10Pairs N (↑N ^ (1 / 10)) (↑N ^ (1 / 3))) : ∃ q ∈ goldbachB9HighLogGridCells n, LiuWeight.LiuPairInLogRectangle N (goldbachB9AlphaGridPoint n ↑q.1) (goldbachB9AlphaGridPoint n (↑q.1 + 1)) (goldbachB9BetaGridPoint n ↑q.2) (goldbachB9BetaGridPoint n (↑q.2 + 1)) rs

The actual closed first-prime endpoint belongs to the selected cover.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachK9High_le_logGridMajorant (n N : ℕ) (hn : 0 < n) (hN : 2 ≤ N) : goldbachK9High N ≤ goldbachB9HighLogGridMajorant n N

Full-family rectangle estimates are used only inside the high selection.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighLogGridMajorant_eq_primeReciprocalProducts (n N : ℕ) : goldbachB9HighLogGridMajorant n N = ∑ q ∈ goldbachB9HighLogGridCells n, 1 / (1 - goldbachB9AlphaGridPoint n (↑q.1 + 1) - goldbachB9BetaGridPoint n (↑q.2 + 1)) * (PrimeReciprocalLogScale.primeReciprocalLogInterval N (goldbachB9AlphaGridPoint n ↑q.1) (goldbachB9AlphaGridPoint n (↑q.1 + 1)) * PrimeReciprocalLogScale.primeReciprocalLogInterval N (goldbachB9BetaGridPoint n ↑q.2) (goldbachB9BetaGridPoint n (↑q.2 + 1)))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.tendsto_goldbachB9HighLogGridMajorant (n : ℕ) (hn : 0 < n) : Filter.Tendsto (goldbachB9HighLogGridMajorant n) Filter.atTop (nhds (goldbachB9HighLogGridUpperSum n))

Apply Mertens to this finite weighted sum, not to a full-sum limit.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachK9High_le_gridUpperSum_eventually (n : ℕ) (hn : 0 < n) (η : ℝ) (hη : 0 < η) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → goldbachK9High N ≤ goldbachB9HighLogGridUpperSum n + η