Liu's prime-pair logarithmic kernel

This module rewrites Liu's reciprocal-log pair sum as the exact kernel in the logarithmic prime coordinates log p / log N. It then bounds the contribution from a fixed exponent rectangle by the corresponding ordered-prime reciprocal mass, and aggregates any finite rectangle cover. Overlap in the cover is allowed; no moving-boundary or limit transfer is asserted.

noncomputable def MathlibNt.SieveTheory.LiuWeight.primeLogExponent (N p : ℕ) : ℝ

The logarithmic exponent coordinate of a prime relative to N.

Equations

• MathlibNt.SieveTheory.LiuWeight.primeLogExponent N p = Real.log ↑p / Real.log ↑N

def MathlibNt.SieveTheory.LiuWeight.LiuPairInLogRectangle (N : ℕ) (a₀ a₁ b₀ b₁ : ℝ) (p : ℕ × ℕ) : Prop

Membership in the fixed exponent rectangle (a₀, a₁] × (b₀, b₁].

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuPairInLogRectangle N a₀ a₁ b₀ b₁ p = (a₀ < MathlibNt.SieveTheory.LiuWeight.primeLogExponent N p.1 ∧ MathlibNt.SieveTheory.LiuWeight.primeLogExponent N p.1 ≤ a₁ ∧ b₀ < MathlibNt.SieveTheory.LiuWeight.primeLogExponent N p.2 ∧ MathlibNt.SieveTheory.LiuWeight.primeLogExponent N p.2 ≤ b₁)

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPairsInLogRectangle (N : ℕ) (a₀ a₁ b₀ b₁ : ℝ) : Finset (ℕ × ℕ)

Liu pairs whose logarithmic coordinates lie in one fixed rectangle.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPairsInLogRectangle N a₀ a₁ b₀ b₁ = Finset.filter (MathlibNt.SieveTheory.LiuWeight.LiuPairInLogRectangle N a₀ a₁ b₀ b₁) (MathlibNt.SieveTheory.LiuWeight.liuWeightPairs N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N))

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPairLogKernel (N : ℕ) (p : ℕ × ℕ) : ℝ

The exact normalized logarithmic kernel attached to an ordered pair.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPairLogKernel N p = 1 / (↑p.1 * ↑p.2 * (1 - MathlibNt.SieveTheory.LiuWeight.primeLogExponent N p.1 - MathlibNt.SieveTheory.LiuWeight.primeLogExponent N p.2))

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

The full finite logarithmic-kernel sum over Liu's ordered prime pairs.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPairLogKernelSum N = ∑ p ∈ MathlibNt.SieveTheory.LiuWeight.liuWeightPairs N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N), MathlibNt.SieveTheory.LiuWeight.liuPairLogKernel N p

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPairLogKernelRectangleContribution (N : ℕ) (a₀ a₁ b₀ b₁ : ℝ) : ℝ

The logarithmic-kernel contribution from Liu pairs in one fixed rectangle.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPairLogKernelRectangleContribution N a₀ a₁ b₀ b₁ = ∑ p ∈ MathlibNt.SieveTheory.LiuWeight.liuPairsInLogRectangle N a₀ a₁ b₀ b₁, MathlibNt.SieveTheory.LiuWeight.liuPairLogKernel N p

theorem MathlibNt.SieveTheory.LiuWeight.primeLogExponent_mem_interval_iff {N p : ℕ} (hN : 1 < N) (hp : 0 < p) (a₀ a₁ : ℝ) : a₀ < primeLogExponent N p ∧ primeLogExponent N p ≤ a₁ ↔ ↑N ^ a₀ < ↑p ∧ ↑p ≤ ↑N ^ a₁

Positive bases have the expected power-cutoff interpretation in logarithmic coordinates.

theorem MathlibNt.SieveTheory.LiuWeight.log_div_pair_eq_log_mul_one_sub_exponents {N : ℕ} (hN : 8 ≤ N) {p : ℕ × ℕ} (hp : p ∈ liuWeightPairs N (liuSourceZ10 N) (liuSourceY3 N)) : Real.log (↑N / (↑p.1 * ↑p.2)) = Real.log ↑N * (1 - primeLogExponent N p.1 - primeLogExponent N p.2)

Exact logarithmic change of variables for every Liu source pair.

theorem MathlibNt.SieveTheory.LiuWeight.one_sub_primeLogExponent_pos {N : ℕ} (hN : 8 ≤ N) {p : ℕ × ℕ} (hp : p ∈ liuWeightPairs N (liuSourceZ10 N) (liuSourceY3 N)) : 0 < 1 - primeLogExponent N p.1 - primeLogExponent N p.2

The kernel denominator is positive on every Liu source pair.

theorem MathlibNt.SieveTheory.LiuWeight.log_mul_liuSourceReciprocalLogSum_eq_pairLogKernelSum (N : ℕ) (hN : 8 ≤ N) : Real.log ↑N * liuSourceReciprocalLogSum N = liuPairLogKernelSum N

Multiplying Liu's reciprocal-log sum by log N gives the exact finite logarithmic-kernel sum, with ordered pairs and real division unchanged.

theorem MathlibNt.SieveTheory.LiuWeight.liuPairLogKernel_nonneg {N : ℕ} (hN : 8 ≤ N) {p : ℕ × ℕ} (hp : p ∈ liuWeightPairs N (liuSourceZ10 N) (liuSourceY3 N)) : 0 ≤ liuPairLogKernel N p

Every kernel summand on the Liu pair set is nonnegative.

theorem MathlibNt.SieveTheory.LiuWeight.liuPairLogKernelRectangleContribution_nonneg (N : ℕ) (hN : 8 ≤ N) (a₀ a₁ b₀ b₁ : ℝ) : 0 ≤ liuPairLogKernelRectangleContribution N a₀ a₁ b₀ b₁

The kernel contribution of any fixed exponent rectangle is nonnegative.

noncomputable def MathlibNt.SieveTheory.LiuWeight.primeLogRectanglePairs (N : ℕ) (a₀ a₁ b₀ b₁ : ℝ) : Finset (ℕ × ℕ)

The finite product carrier underlying primeReciprocalLogRectangle.

Equations

• MathlibNt.SieveTheory.LiuWeight.primeLogRectanglePairs N a₀ a₁ b₀ b₁ = {p₁ ∈ Finset.range (MathlibNt.SieveTheory.PrimeReciprocalLogScale.rpowFloor N a₁ + 1) | Nat.Prime p₁ ∧ ↑N ^ a₀ < ↑p₁ ∧ ↑p₁ ≤ ↑N ^ a₁} ×ˢ {p₂ ∈ Finset.range (MathlibNt.SieveTheory.PrimeReciprocalLogScale.rpowFloor N b₁ + 1) | Nat.Prime p₂ ∧ ↑N ^ b₀ < ↑p₂ ∧ ↑p₂ ≤ ↑N ^ b₁}

theorem MathlibNt.SieveTheory.LiuWeight.sum_primeLogRectanglePairs_eq_primeReciprocalLogRectangle (N : ℕ) (a₀ a₁ b₀ b₁ : ℝ) : ∑ p ∈ primeLogRectanglePairs N a₀ a₁ b₀ b₁, 1 / (↑p.1 * ↑p.2) = PrimeReciprocalLogRectangle.primeReciprocalLogRectangle N a₀ a₁ b₀ b₁

The product-carrier reciprocal sum is exactly the existing ordered-prime rectangle mass.

theorem MathlibNt.SieveTheory.LiuWeight.liuPairsInLogRectangle_subset_primeLogRectanglePairs {N : ℕ} (hN : 1 < N) (a₀ a₁ b₀ b₁ : ℝ) : liuPairsInLogRectangle N a₀ a₁ b₀ b₁ ⊆ primeLogRectanglePairs N a₀ a₁ b₀ b₁

Liu pairs selected by exponent coordinates form a subset of the existing ordered-prime rectangle carrier.

theorem MathlibNt.SieveTheory.LiuWeight.liuPairLogKernel_le_rectangleCorner {N : ℕ} {p : ℕ × ℕ} (hp : p ∈ liuWeightPairs N (liuSourceZ10 N) (liuSourceY3 N)) {a₀ a₁ b₀ b₁ : ℝ} (hrect : LiuPairInLogRectangle N a₀ a₁ b₀ b₁ p) (hupper : a₁ + b₁ < 1) : liuPairLogKernel N p ≤ 1 / (1 - a₁ - b₁) * (1 / (↑p.1 * ↑p.2))

On a rectangle below α + β = 1, each kernel value is bounded by the upper-right-corner kernel times the reciprocal pair weight.

theorem MathlibNt.SieveTheory.LiuWeight.liuPairLogKernelRectangleContribution_le (N : ℕ) (hN : 8 ≤ N) (a₀ a₁ b₀ b₁ : ℝ) (hupper : a₁ + b₁ < 1) : liuPairLogKernelRectangleContribution N a₀ a₁ b₀ b₁ ≤ 1 / (1 - a₁ - b₁) * PrimeReciprocalLogRectangle.primeReciprocalLogRectangle N a₀ a₁ b₀ b₁

A fixed rectangle below the singular boundary contributes at most its upper-right-corner kernel times the full ordered-prime rectangle mass.

theorem MathlibNt.SieveTheory.LiuWeight.liuPairLogKernelSum_le_sum_rectangleMajorants_of_cover {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (a₀ a₁ b₀ b₁ : ι → ℝ) (N : ℕ) (hN : 8 ≤ N) (_ha₀ : ∀ i ∈ s, 0 < a₀ i) (_ha : ∀ i ∈ s, a₀ i < a₁ i) (_hb₀ : ∀ i ∈ s, 0 < b₀ i) (_hb : ∀ i ∈ s, b₀ i < b₁ i) (hupper : ∀ i ∈ s, a₁ i + b₁ i < 1) (hcover : ∀ p ∈ liuWeightPairs N (liuSourceZ10 N) (liuSourceY3 N), ∃ i ∈ s, LiuPairInLogRectangle N (a₀ i) (a₁ i) (b₀ i) (b₁ i) p) : liuPairLogKernelSum N ≤ ∑ i ∈ s, 1 / (1 - a₁ i - b₁ i) * PrimeReciprocalLogRectangle.primeReciprocalLogRectangle N (a₀ i) (a₁ i) (b₀ i) (b₁ i)

A finite family of positive rectangles may overlap: if it covers every Liu pair and stays below α + β = 1, the full kernel sum is bounded by the sum of the rectangle majorants.