The canonical logarithmic grid tends to Liu's source integral

This file interprets each logarithmic rectangle mass as an actual integral, checks the half-open grid partition, and compares the resulting upper sum with the integral on Liu's triangular source region.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuLogDensity (x : ℝ × ℝ) : ℝ

The logarithmic density in the two exponent coordinates.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuLogDensity x = 1 / (x.1 * x.2)

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuLogKernel (x : ℝ × ℝ) : ℝ

Liu's remaining kernel in logarithmic coordinates.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuLogKernel x = 1 / (1 - x.1 - x.2)

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuLogIntegrand (x : ℝ × ℝ) : ℝ

The full density occurring in Liu's source integral.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuLogIntegrand x = MathlibNt.SieveTheory.LiuWeight.liuLogKernel x * MathlibNt.SieveTheory.LiuWeight.liuLogDensity x

def MathlibNt.SieveTheory.LiuWeight.liuLogGridCell (n : ℕ) (q : Fin n × Fin n) : Set (ℝ × ℝ)

A half-open canonical grid cell.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuLogGridCell n q = Set.Ioc (MathlibNt.SieveTheory.LiuWeight.liuAlphaGridPoint n ↑q.1) (MathlibNt.SieveTheory.LiuWeight.liuAlphaGridPoint n (↑q.1 + 1)) ×ˢ Set.Ioc (MathlibNt.SieveTheory.LiuWeight.liuBetaGridPoint n ↑q.2) (MathlibNt.SieveTheory.LiuWeight.liuBetaGridPoint n (↑q.2 + 1))

def MathlibNt.SieveTheory.LiuWeight.liuLogGridRegion (n : ℕ) : Set (ℝ × ℝ)

The union of the cells selected by their lower-left corners.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuLogGridRegion n = ⋃ q ∈ MathlibNt.SieveTheory.LiuWeight.liuLogGridCells n, MathlibNt.SieveTheory.LiuWeight.liuLogGridCell n q

def MathlibNt.SieveTheory.LiuWeight.liuLogSourceRegion : Set (ℝ × ℝ)

The exact half-open source region from Liu's integral.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuLogSourceRegion = {x : ℝ × ℝ | x.1 ∈ Set.Ioc (1 / 10) (1 / 3) ∧ x.2 ∈ Set.Ioc (1 / 3) ((1 - x.1) / 2)}

theorem MathlibNt.SieveTheory.LiuWeight.logarithmicRectangleMass_eq_iteratedIntegral {a₀ a₁ b₀ b₁ : ℝ} (ha₀ : 0 < a₀) (ha : a₀ < a₁) (hb₀ : 0 < b₀) (hb : b₀ < b₁) : PrimeReciprocalLogRectangle.logarithmicRectangleMass a₀ a₁ b₀ b₁ = ∫ (α : ℝ) in a₀..a₁, ∫ (β : ℝ) in b₀..b₁, 1 / (α * β)

A logarithmic rectangle mass is exactly the iterated integral of the logarithmic density.

theorem MathlibNt.SieveTheory.LiuWeight.logarithmicRectangleMass_eq_setIntegral {a₀ a₁ b₀ b₁ : ℝ} (ha₀ : 0 < a₀) (ha : a₀ < a₁) (hb₀ : 0 < b₀) (hb : b₀ < b₁) : PrimeReciprocalLogRectangle.logarithmicRectangleMass a₀ a₁ b₀ b₁ = ∫ (x : ℝ × ℝ) in Set.Ioc a₀ a₁ ×ˢ Set.Ioc b₀ b₁, liuLogDensity x

The same identity as a product-set integral.

theorem MathlibNt.SieveTheory.LiuWeight.measurableSet_liuLogGridCell (n : ℕ) (q : Fin n × Fin n) : MeasurableSet (liuLogGridCell n q)

Canonical half-open cells are measurable.

theorem MathlibNt.SieveTheory.LiuWeight.liuLogGridCell_pairwiseDisjoint {n : ℕ} (hn : 0 < n) : Set.univ.Pairwise (Function.onFun Disjoint (liuLogGridCell n))

The strict-left/non-strict-right convention makes distinct cells genuinely disjoint, including on all grid lines.

theorem MathlibNt.SieveTheory.LiuWeight.liuLogSourceRegion_subset_gridRegion {n : ℕ} (hn : 0 < n) : liuLogSourceRegion ⊆ liuLogGridRegion n

Every source point is in a selected half-open cell. This is the geometric counterpart of the prime-pair cover and fixes all boundary conventions.

theorem MathlibNt.SieveTheory.LiuWeight.liuLogGridRegion_geometry {n : ℕ} (hn : 0 < n) {x : ℝ × ℝ} (hx : x ∈ liuLogGridRegion n) : x.1 ∈ Set.Ioc (1 / 10) (1 / 3) ∧ x.2 ∈ Set.Ioc (1 / 3) (9 / 20) ∧ x.1 + 2 * x.2 < 1 + 7 / (15 * ↑n)

Every selected cell stays in the fixed source box and in a strip of width 7/(15n) above the oblique source boundary.

def MathlibNt.SieveTheory.LiuWeight.liuLogAmbientBox : Set (ℝ × ℝ)

The fixed compact box containing every source point and every selected cell.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuLogAmbientBox = Set.Icc (1 / 10) (1 / 3) ×ˢ Set.Icc (1 / 3) (9 / 20)

theorem MathlibNt.SieveTheory.LiuWeight.measurableSet_liuLogAmbientBox : MeasurableSet liuLogAmbientBox

theorem MathlibNt.SieveTheory.LiuWeight.isCompact_liuLogAmbientBox : IsCompact liuLogAmbientBox

theorem MathlibNt.SieveTheory.LiuWeight.liuLogSourceRegion_subset_ambientBox : liuLogSourceRegion ⊆ liuLogAmbientBox

theorem MathlibNt.SieveTheory.LiuWeight.liuLogGridRegion_subset_ambientBox {n : ℕ} (hn : 0 < n) : liuLogGridRegion n ⊆ liuLogAmbientBox

theorem MathlibNt.SieveTheory.LiuWeight.measurableSet_liuLogGridRegion (n : ℕ) : MeasurableSet (liuLogGridRegion n)

theorem MathlibNt.SieveTheory.LiuWeight.measurableSet_liuLogSourceRegion : MeasurableSet liuLogSourceRegion

theorem MathlibNt.SieveTheory.LiuWeight.liuLogDensity_nonneg {x : ℝ × ℝ} (hx : x ∈ liuLogAmbientBox) : 0 ≤ liuLogDensity x

theorem MathlibNt.SieveTheory.LiuWeight.liuLogKernel_nonneg {x : ℝ × ℝ} (hx : x ∈ liuLogAmbientBox) : 0 ≤ liuLogKernel x

theorem MathlibNt.SieveTheory.LiuWeight.liuLogIntegrand_nonneg {x : ℝ × ℝ} (hx : x ∈ liuLogAmbientBox) : 0 ≤ liuLogIntegrand x

theorem MathlibNt.SieveTheory.LiuWeight.continuousOn_liuLogDensity : ContinuousOn liuLogDensity liuLogAmbientBox

theorem MathlibNt.SieveTheory.LiuWeight.continuousOn_liuLogKernel : ContinuousOn liuLogKernel liuLogAmbientBox

theorem MathlibNt.SieveTheory.LiuWeight.continuousOn_liuLogIntegrand : ContinuousOn liuLogIntegrand liuLogAmbientBox

theorem MathlibNt.SieveTheory.LiuWeight.integrableOn_liuLogDensity {s : Set (ℝ × ℝ)} (hs : MeasurableSet s) (hsub : s ⊆ liuLogAmbientBox) : MeasureTheory.IntegrableOn liuLogDensity s MeasureTheory.volume

theorem MathlibNt.SieveTheory.LiuWeight.integrableOn_liuLogIntegrand {s : Set (ℝ × ℝ)} (hs : MeasurableSet s) (hsub : s ⊆ liuLogAmbientBox) : MeasureTheory.IntegrableOn liuLogIntegrand s MeasureTheory.volume

theorem MathlibNt.SieveTheory.LiuWeight.liuLogIntegrand_eq_sourceInner {α β : ℝ} (hα : α ∈ Set.Icc (1 / 10) (1 / 3)) (hβ : β ∈ Set.Icc (1 / 3) ((1 - α) / 2)) : liuLogIntegrand (α, β) = 1 / α * liuSourceInnerIntegrand α β

theorem MathlibNt.SieveTheory.LiuWeight.liuSourceMainIntegral_eq_iteratedSetIntegral : liuSourceMainIntegral = ∫ (α : ℝ) in Set.Ioc (1 / 10) (1 / 3), ∫ (β : ℝ) in Set.Ioc (1 / 3) ((1 - α) / 2), liuLogIntegrand (α, β)

theorem MathlibNt.SieveTheory.LiuWeight.liuSourceMainIntegral_eq_setIntegral : liuSourceMainIntegral = ∫ (x : ℝ × ℝ) in liuLogSourceRegion, liuLogIntegrand x

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuLogGridUpperIntegrand (n : ℕ) (x : ℝ × ℝ) : ℝ

The piecewise upper-corner density whose integral is the finite upper sum.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuLogGridUpperIntegrand n x = ∑ 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.LiuWeight.liuLogGridCell n q).indicator MathlibNt.SieveTheory.LiuWeight.liuLogDensity x

theorem MathlibNt.SieveTheory.LiuWeight.integrable_indicator_of_integrableOn {f : ℝ × ℝ → ℝ} {s : Set (ℝ × ℝ)} (hs : MeasurableSet s) (hf : MeasureTheory.IntegrableOn f s MeasureTheory.volume) : MeasureTheory.Integrable (s.indicator f) MeasureTheory.volume

theorem MathlibNt.SieveTheory.LiuWeight.liuLogGridCell_subset_ambientBox {n : ℕ} (hn : 0 < n) {q : Fin n × Fin n} (hq : q ∈ liuLogGridCells n) : liuLogGridCell n q ⊆ liuLogAmbientBox

theorem MathlibNt.SieveTheory.LiuWeight.liuLogGridUpperSum_eq_integral (n : ℕ) (hn : 0 < n) : liuLogGridUpperSum n = ∫ (x : ℝ × ℝ), liuLogGridUpperIntegrand n x

theorem MathlibNt.SieveTheory.LiuWeight.integrable_liuLogGridUpperIntegrand (n : ℕ) (hn : 0 < n) : MeasureTheory.Integrable (liuLogGridUpperIntegrand n) MeasureTheory.volume

theorem MathlibNt.SieveTheory.LiuWeight.liuLogGridUpperIntegrand_nonneg {n : ℕ} (hn : 0 < n) (x : ℝ × ℝ) : 0 ≤ liuLogGridUpperIntegrand n x

theorem MathlibNt.SieveTheory.LiuWeight.liuLogGridUpperIntegrand_eq_of_mem {n : ℕ} (hn : 0 < n) {q : Fin n × Fin n} (hq : q ∈ liuLogGridCells n) {x : ℝ × ℝ} (hx : x ∈ liuLogGridCell n q) : liuLogGridUpperIntegrand n x = 1 / (1 - liuAlphaGridPoint n (↑q.1 + 1) - liuBetaGridPoint n (↑q.2 + 1)) * liuLogDensity x

At a point of a selected cell, pairwise disjointness reduces the upper integrand to that cell's single summand.

theorem MathlibNt.SieveTheory.LiuWeight.liuLogIntegrand_le_liuLogGridUpperIntegrand {n : ℕ} (hn : 0 < n) {x : ℝ × ℝ} (hx : x ∈ liuLogSourceRegion) : liuLogIntegrand x ≤ liuLogGridUpperIntegrand n x

theorem MathlibNt.SieveTheory.LiuWeight.liuSourceMainIntegral_le_liuLogGridUpperSum (n : ℕ) (hn : 0 < n) : liuSourceMainIntegral ≤ liuLogGridUpperSum n

theorem MathlibNt.SieveTheory.LiuWeight.liuLogGrid_upperKernel_sub_le {n : ℕ} (hn : 0 < n) {q : Fin n × Fin n} (_hq : q ∈ liuLogGridCells n) {x : ℝ × ℝ} (hx : x ∈ liuLogGridCell n q) : 0 ≤ 1 / (1 - liuAlphaGridPoint n (↑q.1 + 1) - liuBetaGridPoint n (↑q.2 + 1)) - liuLogKernel x ∧ 1 / (1 - liuAlphaGridPoint n (↑q.1 + 1) - liuBetaGridPoint n (↑q.2 + 1)) - liuLogKernel x ≤ 25 / ↑n

theorem MathlibNt.SieveTheory.LiuWeight.liuLogDensity_le_thirty {x : ℝ × ℝ} (hx : x ∈ liuLogAmbientBox) : liuLogDensity x ≤ 30

The logarithmic density is uniformly bounded on the ambient box.

theorem MathlibNt.SieveTheory.LiuWeight.liuLogGrid_upperKernel_le_five {n : ℕ} (hn : 0 < n) {q : Fin n × Fin n} (_hq : q ∈ liuLogGridCells n) : 1 / (1 - liuAlphaGridPoint n (↑q.1 + 1) - liuBetaGridPoint n (↑q.2 + 1)) ≤ 5

Every selected upper corner has remaining kernel at most five.

theorem MathlibNt.SieveTheory.LiuWeight.liuLogGridUpperIntegrand_eq_zero_of_notMem {n : ℕ} {x : ℝ × ℝ} (hx : x ∉ liuLogGridRegion n) : liuLogGridUpperIntegrand n x = 0

The upper integrand vanishes off the selected grid region.

theorem MathlibNt.SieveTheory.LiuWeight.liuLogGridUpperIntegrand_le_oneHundredFifty {n : ℕ} (hn : 0 < n) {x : ℝ × ℝ} (hx : x ∈ liuLogGridRegion n) : liuLogGridUpperIntegrand n x ≤ 150

The selected upper integrand is uniformly bounded by 150 on its grid.

def MathlibNt.SieveTheory.LiuWeight.liuLogExcessStrip (n : ℕ) : Set (ℝ × ℝ)

The thin oblique strip swept out above Liu's source boundary.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuLogExcessStrip n = {x : ℝ × ℝ | x.1 ∈ Set.Icc (1 / 10) (1 / 3) ∧ (1 - x.1) / 2 < x.2 ∧ x.2 < (1 - x.1) / 2 + 7 / (30 * ↑n)}

theorem MathlibNt.SieveTheory.LiuWeight.measurableSet_liuLogExcessStrip (n : ℕ) : MeasurableSet (liuLogExcessStrip n)

theorem MathlibNt.SieveTheory.LiuWeight.liuLogGridRegion_diff_source_subset_excessStrip {n : ℕ} (hn : 0 < n) : liuLogGridRegion n \ liuLogSourceRegion ⊆ liuLogExcessStrip n

A selected grid point outside the source belongs to the excess strip.

theorem MathlibNt.SieveTheory.LiuWeight.volume_liuLogExcessStrip {n : ℕ} (hn : 0 < n) : MeasureTheory.volume (liuLogExcessStrip n) = ENNReal.ofReal (49 / (900 * ↑n))

The excess strip has width 7/(30n) in every vertical section.

theorem MathlibNt.SieveTheory.LiuWeight.liuLogGridUpperIntegrand_le_integrand_add {n : ℕ} (hn : 0 < n) {x : ℝ × ℝ} (hx : x ∈ liuLogSourceRegion) : liuLogGridUpperIntegrand n x ≤ liuLogIntegrand x + 750 / ↑n

On the source, replacing the kernel by the selected upper corner costs at most 750/n.

theorem MathlibNt.SieveTheory.LiuWeight.liuLogGridUpperIntegrand_majorized {n : ℕ} (hn : 0 < n) (x : ℝ × ℝ) : liuLogGridUpperIntegrand n x ≤ liuLogSourceRegion.indicator liuLogIntegrand x + (Set.Icc 0 1 ×ˢ Set.Icc 0 1).indicator (fun (x : ℝ × ℝ) => 750 / ↑n) x + (liuLogExcessStrip n).indicator (fun (x : ℝ × ℝ) => 150) x

A global integrable majorant separates the source error from the thin geometric excess strip.

theorem MathlibNt.SieveTheory.LiuWeight.liuLogGridUpperSum_sub_source_le (n : ℕ) (hn : 0 < n) : liuLogGridUpperSum n - liuSourceMainIntegral ≤ 759 / ↑n

The grid upper sum exceeds Liu's source integral by at most 759/n.

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_liuLogGridUpperSum_sourceMainIntegral : Filter.Tendsto (fun (n : ℕ) => liuLogGridUpperSum (n + 1)) Filter.atTop (nhds liuSourceMainIntegral)

The canonical logarithmic-grid upper sums converge to Liu's source integral as the mesh tends to zero.