A canonical logarithmic grid for Liu's prime pairs

This module partitions the fixed source box (1/10, 1/3] × (1/3, 9/20] into an n × n grid. Cells are selected from their lower-left corners using the exact source boundary α + 2β ≤ 1. The resulting finite rectangle majorant converges, for each fixed positive n, to its logarithmic upper sum.

No limit as the mesh tends to zero is asserted here.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuAlphaGridPoint (n i : ℕ) : ℝ

The ith point of the canonical alpha grid from 1/10 to 1/3.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuAlphaGridPoint n i = 1 / 10 + ↑i / ↑n * (7 / 30)

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuBetaGridPoint (n j : ℕ) : ℝ

The jth point of the canonical beta grid from 1/3 to 9/20.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuBetaGridPoint n j = 1 / 3 + ↑j / ↑n * (7 / 60)

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuAlphaGridStep (n : ℕ) : ℝ

The alpha width of a cell in the canonical grid.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuAlphaGridStep n = 7 / 30 / ↑n

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuBetaGridStep (n : ℕ) : ℝ

The beta width of a cell in the canonical grid.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuBetaGridStep n = 7 / 60 / ↑n

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuLogGridCells (n : ℕ) : Finset (Fin n × Fin n)

The selected cells are those whose lower-left corner lies strictly below the exact source line β = (1 - α) / 2.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuLogGridCells n = {q : Fin n × Fin n | MathlibNt.SieveTheory.LiuWeight.liuBetaGridPoint n ↑q.2 < (1 - MathlibNt.SieveTheory.LiuWeight.liuAlphaGridPoint n ↑q.1) / 2}

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuLogGridMajorant (n N : ℕ) : ℝ

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

Equations

• MathlibNt.SieveTheory.LiuWeight.liuLogGridMajorant n N = ∑ q ∈ MathlibNt.SieveTheory.LiuWeight.liuLogGridCells n, 1 / (1 - MathlibNt.SieveTheory.LiuWeight.liuAlphaGridPoint n (↑q.1 + 1) - MathlibNt.SieveTheory.LiuWeight.liuBetaGridPoint n (↑q.2 + 1)) * MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.primeReciprocalLogRectangle N (MathlibNt.SieveTheory.LiuWeight.liuAlphaGridPoint n ↑q.1) (MathlibNt.SieveTheory.LiuWeight.liuAlphaGridPoint n (↑q.1 + 1)) (MathlibNt.SieveTheory.LiuWeight.liuBetaGridPoint n ↑q.2) (MathlibNt.SieveTheory.LiuWeight.liuBetaGridPoint n (↑q.2 + 1))

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuLogGridUpperSum (n : ℕ) : ℝ

The fixed-grid logarithmic upper sum corresponding to liuLogGridMajorant.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuLogGridUpperSum n = ∑ q ∈ MathlibNt.SieveTheory.LiuWeight.liuLogGridCells n, 1 / (1 - MathlibNt.SieveTheory.LiuWeight.liuAlphaGridPoint n (↑q.1 + 1) - MathlibNt.SieveTheory.LiuWeight.liuBetaGridPoint n (↑q.2 + 1)) * MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.logarithmicRectangleMass (MathlibNt.SieveTheory.LiuWeight.liuAlphaGridPoint n ↑q.1) (MathlibNt.SieveTheory.LiuWeight.liuAlphaGridPoint n (↑q.1 + 1)) (MathlibNt.SieveTheory.LiuWeight.liuBetaGridPoint n ↑q.2) (MathlibNt.SieveTheory.LiuWeight.liuBetaGridPoint n (↑q.2 + 1))

theorem MathlibNt.SieveTheory.LiuWeight.liuAlphaGridStep_pos {n : ℕ} (hn : 0 < n) : 0 < liuAlphaGridStep n

theorem MathlibNt.SieveTheory.LiuWeight.liuBetaGridStep_pos {n : ℕ} (hn : 0 < n) : 0 < liuBetaGridStep n

theorem MathlibNt.SieveTheory.LiuWeight.liuAlphaGridPoint_eq_step {n i : ℕ} (hn : 0 < n) : liuAlphaGridPoint n i = 1 / 10 + ↑i * liuAlphaGridStep n

theorem MathlibNt.SieveTheory.LiuWeight.liuBetaGridPoint_eq_step {n i : ℕ} (hn : 0 < n) : liuBetaGridPoint n i = 1 / 3 + ↑i * liuBetaGridStep n

theorem MathlibNt.SieveTheory.LiuWeight.liuAlphaGridPoint_succ {n i : ℕ} (hn : 0 < n) : liuAlphaGridPoint n (i + 1) = liuAlphaGridPoint n i + liuAlphaGridStep n

theorem MathlibNt.SieveTheory.LiuWeight.liuBetaGridPoint_succ {n i : ℕ} (hn : 0 < n) : liuBetaGridPoint n (i + 1) = liuBetaGridPoint n i + liuBetaGridStep n

theorem MathlibNt.SieveTheory.LiuWeight.liuAlphaGridPoint_pos {n i : ℕ} (hn : 0 < n) : 0 < liuAlphaGridPoint n i

theorem MathlibNt.SieveTheory.LiuWeight.liuBetaGridPoint_pos {n i : ℕ} (hn : 0 < n) : 0 < liuBetaGridPoint n i

theorem MathlibNt.SieveTheory.LiuWeight.liuAlphaGridPoint_lt_succ {n i : ℕ} (hn : 0 < n) : liuAlphaGridPoint n i < liuAlphaGridPoint n (i + 1)

theorem MathlibNt.SieveTheory.LiuWeight.liuBetaGridPoint_lt_succ {n i : ℕ} (hn : 0 < n) : liuBetaGridPoint n i < liuBetaGridPoint n (i + 1)

theorem MathlibNt.SieveTheory.LiuWeight.liuAlphaGridPoint_succ_le_end {n i : ℕ} (hn : 0 < n) (hi : i < n) : liuAlphaGridPoint n (i + 1) ≤ 1 / 3

theorem MathlibNt.SieveTheory.LiuWeight.liuAlphaGridStep_le {n : ℕ} (hn : 0 < n) : liuAlphaGridStep n ≤ 7 / 30

theorem MathlibNt.SieveTheory.LiuWeight.exists_nat_cell (n : ℕ) {x a d : ℝ} (hd : 0 < d) (hx : a < x) (hxu : x ≤ a + ↑n * d) : ∃ i < n, a + ↑i * d < x ∧ x ≤ a + ↑(i + 1) * d

Natural ceilings give the unique endpoint convention needed by the grid: strict on the left and non-strict on the right.

theorem MathlibNt.SieveTheory.LiuWeight.primeLogExponent_add_two_mul_le_one {N : ℕ} (hN : 8 ≤ N) {p : ℕ × ℕ} (hp : p ∈ liuWeightPairs N (liuSourceZ10 N) (liuSourceY3 N)) : primeLogExponent N p.1 + 2 * primeLogExponent N p.2 ≤ 1

The exact root-free source condition p₁ p₂² ≤ N becomes the triangular inequality α + 2β ≤ 1 in logarithmic coordinates.

theorem MathlibNt.SieveTheory.LiuWeight.liuLogGridCell_upperCorner_lt_one {n : ℕ} (hn : 0 < n) {q : Fin n × Fin n} (hq : q ∈ liuLogGridCells n) : liuAlphaGridPoint n (↑q.1 + 1) + liuBetaGridPoint n (↑q.2 + 1) < 1

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

theorem MathlibNt.SieveTheory.LiuWeight.liuWeightPairs_covered_by_logGrid (n N : ℕ) (hn : 0 < n) (hN : 8 ≤ N) {p : ℕ × ℕ} (hp : p ∈ liuWeightPairs N (liuSourceZ10 N) (liuSourceY3 N)) : ∃ q ∈ liuLogGridCells n, LiuPairInLogRectangle N (liuAlphaGridPoint n ↑q.1) (liuAlphaGridPoint n (↑q.1 + 1)) (liuBetaGridPoint n ↑q.2) (liuBetaGridPoint n (↑q.2 + 1)) p

Every Liu source pair belongs to a selected canonical cell. The natural ceiling construction handles points on upper grid boundaries without changing the source's strict-lower/non-strict-upper convention.

theorem MathlibNt.SieveTheory.LiuWeight.liuPairLogKernelSum_le_logGridMajorant (n N : ℕ) (hn : 0 < n) (hN : 8 ≤ N) : liuPairLogKernelSum N ≤ liuLogGridMajorant n N

The canonical selected grid majorizes the full finite Liu logarithmic kernel sum.

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_liuLogGridMajorant (n : ℕ) (hn : 0 < n) : Filter.Tendsto (fun (N : ℕ) => liuLogGridMajorant n N) Filter.atTop (nhds (liuLogGridUpperSum n))

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

theorem MathlibNt.SieveTheory.LiuWeight.eventually_abs_liuLogGridMajorant_sub_lt (n : ℕ) (hn : 0 < n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, |liuLogGridMajorant n N - liuLogGridUpperSum n| < ε

Eventual epsilon form of fixed canonical-grid convergence.

theorem MathlibNt.SieveTheory.LiuWeight.exists_abs_liuLogGridMajorant_sub_lt (n : ℕ) (hn : 0 < n) {ε : ℝ} (hε : 0 < ε) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → |liuLogGridMajorant n N - liuLogGridUpperSum n| < ε

Threshold form of fixed canonical-grid convergence.