noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10AlphaGridStart : ℝ

The ambient left endpoint used to cover the closed lower bound u = β.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10AlphaGridStart = 1 / 10

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridStart : ℝ

The ambient lower endpoint used to cover the closed lower bound v = γ.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridStart = 1 / 4

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridEnd : ℝ

The exact top endpoint forced by u ≥ β and u + 2v ≤ 1.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridEnd = 29 / 66

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10AlphaGridWidth : ℝ

The u-width of the ambient B10 logarithmic box.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10AlphaGridWidth = 19 / 110

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridWidth : ℝ

The v-width of the ambient B10 logarithmic box.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridWidth = 25 / 132

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

The ith point of the ambient u-grid from 1/10 to 3/11.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10AlphaGridPoint n i = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10AlphaGridStart + ↑i / ↑n * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10AlphaGridWidth

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

The jth point of the ambient v-grid from 1/4 to 29/66.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridPoint n j = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridStart + ↑j / ↑n * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridWidth

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

The u-step of the ambient B10 logarithmic grid.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10AlphaGridStep n = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10AlphaGridWidth / ↑n

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

The v-step of the ambient B10 logarithmic grid.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridStep n = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridWidth / ↑n

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

The selected cells are those which intersect the closed-lower B10 source triangle β ≤ u, γ ≤ v, u + 2v ≤ 1.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10LogGridCells n = {q : Fin n × Fin n | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Beta ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10AlphaGridPoint n (↑q.1 + 1) ∧ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Gamma ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridPoint n (↑q.2 + 1) ∧ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10AlphaGridPoint n ↑q.1 + 2 * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridPoint n ↑q.2 < 1}

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

The finite-N upper-corner majorant on the selected B10 cells.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10LogGridMajorant n N = ∑ q ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10LogGridCells n, 1 / (1 - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10AlphaGridPoint n (↑q.1 + 1) - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridPoint n (↑q.2 + 1)) * MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.primeReciprocalLogRectangle N (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10AlphaGridPoint n ↑q.1) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10AlphaGridPoint n (↑q.1 + 1)) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridPoint n ↑q.2) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridPoint n (↑q.2 + 1))

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

The fixed-grid logarithmic upper sum corresponding to the B10 majorant.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10LogGridUpperSum n = ∑ q ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10LogGridCells n, 1 / (1 - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10AlphaGridPoint n (↑q.1 + 1) - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridPoint n (↑q.2 + 1)) * MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.logarithmicRectangleMass (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10AlphaGridPoint n ↑q.1) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10AlphaGridPoint n (↑q.1 + 1)) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridPoint n ↑q.2) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridPoint n (↑q.2 + 1))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10AlphaGridStep_pos {n : ℕ} (hn : 0 < n) : 0 < goldbachB10AlphaGridStep n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridStep_pos {n : ℕ} (hn : 0 < n) : 0 < goldbachB10BetaGridStep n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10AlphaGridPoint_eq_step {n i : ℕ} (hn : 0 < n) : goldbachB10AlphaGridPoint n i = goldbachB10AlphaGridStart + ↑i * goldbachB10AlphaGridStep n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridPoint_eq_step {n i : ℕ} (hn : 0 < n) : goldbachB10BetaGridPoint n i = goldbachB10BetaGridStart + ↑i * goldbachB10BetaGridStep n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10AlphaGridPoint_succ {n i : ℕ} (hn : 0 < n) : goldbachB10AlphaGridPoint n (i + 1) = goldbachB10AlphaGridPoint n i + goldbachB10AlphaGridStep n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridPoint_succ {n i : ℕ} (hn : 0 < n) : goldbachB10BetaGridPoint n (i + 1) = goldbachB10BetaGridPoint n i + goldbachB10BetaGridStep n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10AlphaGridPoint_pos {n i : ℕ} (hn : 0 < n) : 0 < goldbachB10AlphaGridPoint n i

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridPoint_pos {n i : ℕ} (hn : 0 < n) : 0 < goldbachB10BetaGridPoint n i

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10AlphaGridPoint_lt_succ {n i : ℕ} (hn : 0 < n) : goldbachB10AlphaGridPoint n i < goldbachB10AlphaGridPoint n (i + 1)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridPoint_lt_succ {n i : ℕ} (hn : 0 < n) : goldbachB10BetaGridPoint n i < goldbachB10BetaGridPoint n (i + 1)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10AlphaGridPoint_mono {n i j : ℕ} (hn : 0 < n) (hij : i ≤ j) : goldbachB10AlphaGridPoint n i ≤ goldbachB10AlphaGridPoint n j

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridPoint_mono {n i j : ℕ} (hn : 0 < n) (hij : i ≤ j) : goldbachB10BetaGridPoint n i ≤ goldbachB10BetaGridPoint n j

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10AlphaGridPoint_succ_le_end {n i : ℕ} (hn : 0 < n) (hi : i < n) : goldbachB10AlphaGridPoint n (i + 1) ≤ goldbachB10Gamma

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BetaGridPoint_succ_le_end {n i : ℕ} (hn : 0 < n) (hi : i < n) : goldbachB10BetaGridPoint n (i + 1) ≤ goldbachB10BetaGridEnd

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10LogGridCell_upperCorner_lt_one {n : ℕ} (hn : 0 < n) {q : Fin n × Fin n} (_hq : q ∈ goldbachB10LogGridCells n) : goldbachB10AlphaGridPoint n (↑q.1 + 1) + goldbachB10BetaGridPoint n (↑q.2 + 1) < 1

Every selected cell has its upper-right corner strictly below the kernel singularity u + v = 1.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Pairs_covered_by_logGrid (n N : ℕ) (hn : 0 < n) (hN : 2 ≤ N) {rs : ℕ × ℕ} (hrs : rs ∈ goldbachC10Pairs N (↑N ^ goldbachB10Beta) (↑N ^ goldbachB10Gamma)) : ∃ q ∈ goldbachB10LogGridCells n, goldbachB10PairInLogRectangle N (goldbachB10AlphaGridPoint n ↑q.1) (goldbachB10AlphaGridPoint n (↑q.1 + 1)) (goldbachB10BetaGridPoint n ↑q.2) (goldbachB10BetaGridPoint n (↑q.2 + 1)) rs

Every actual C10 pair lies in a selected ambient B10 logarithmic cell.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PairLogKernelSum_le_logGridMajorant (n N : ℕ) (hn : 0 < n) (hN : 2 ≤ N) : goldbachB10PairLogKernelSum N ≤ goldbachB10LogGridMajorant n N

The selected B10 logarithmic grid majorizes the full actual C10 logarithmic-kernel sum.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.tendsto_goldbachB10LogGridMajorant (n : ℕ) (hn : 0 < n) : Filter.Tendsto (fun (N : ℕ) => goldbachB10LogGridMajorant n N) Filter.atTop (nhds (goldbachB10LogGridUpperSum n))

For every fixed positive grid size, the finite-N B10 majorant tends to its logarithmic upper sum.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.eventually_abs_goldbachB10LogGridMajorant_sub_lt (n : ℕ) (hn : 0 < n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, |goldbachB10LogGridMajorant n N - goldbachB10LogGridUpperSum n| < ε

Eventual epsilon form of fixed B10-grid convergence.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.exists_abs_goldbachB10LogGridMajorant_sub_lt (n : ℕ) (hn : 0 < n) {ε : ℝ} (hε : 0 < ε) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → |goldbachB10LogGridMajorant n N - goldbachB10LogGridUpperSum n| < ε

Threshold form of fixed B10-grid convergence.