Truncated Selberg weights

Möbius inversion over multiples constructs the Selberg coefficients from the diagonal variables. This supplies the optimizing weights missing from the quadratic-form identity in Mathlib.

noncomputable def NairTenenbaum.upperDivisorSum (P : ℕ) (f : ℕ → ℝ) (d : ℕ) : ℝ

The sum of the sieve coefficients over divisors of an integer.

Equations

• NairTenenbaum.upperDivisorSum P f d = ∑ e ∈ P.divisors, if d ∣ e then f e else 0

theorem NairTenenbaum.upperDivisorSum_eq_complement {P d : ℕ} (hP : P ≠ 0) (hd : d ∣ P) (f : ℕ → ℝ) : upperDivisorSum P f d = ∑ k ∈ (P / d).divisors, f (P / k)

Complementation reverses the divisor order.

noncomputable def NairTenenbaum.upperDivisorInverse (P : ℕ) (y : ℕ → ℝ) (d : ℕ) : ℝ

Inverse of summing over multiples, written using complementary divisors.

Equations

• NairTenenbaum.upperDivisorInverse P y d = ∑ k ∈ (P / d).divisors, ↑(ArithmeticFunction.moebius (P / d / k)) * y (P / k)

theorem NairTenenbaum.upperDivisorSum_inverse {P d : ℕ} (hP : P ≠ 0) (hd : d ∣ P) (y : ℕ → ℝ) : upperDivisorSum P (upperDivisorInverse P y) d = y d

theorem NairTenenbaum.upperDivisorInverse_one (P : ℕ) (y : ℕ → ℝ) : upperDivisorInverse P y 1 = ∑ d ∈ P.divisors, ↑(ArithmeticFunction.moebius d) * y d

noncomputable def NairTenenbaum.selbergDenominator (s : BoundingSieve) (R : ℝ) : ℝ

The truncated denominator of the Selberg sieve.

Equations

• NairTenenbaum.selbergDenominator s R = ∑ d ∈ s.prodPrimes.divisors, if ↑d ≤ R then BoundingSieve.selbergTerms d else 0

theorem NairTenenbaum.selbergDenominator_pos (s : BoundingSieve) {R : ℝ} (hR : 1 ≤ R) : 0 < selbergDenominator s R

noncomputable def NairTenenbaum.selbergDiagonal (s : BoundingSieve) (R : ℝ) (d : ℕ) : ℝ

The diagonal quadratic form associated with the Selberg weights.

Equations

• NairTenenbaum.selbergDiagonal s R d = if ↑d ≤ R then ↑(ArithmeticFunction.moebius d) * BoundingSieve.selbergTerms d / NairTenenbaum.selbergDenominator s R else 0

noncomputable def NairTenenbaum.selbergWeights (s : BoundingSieve) (R : ℝ) (d : ℕ) : ℝ

Coefficients normalized to be one at 1.

Equations

• NairTenenbaum.selbergWeights s R d = if d ∣ s.prodPrimes then NairTenenbaum.upperDivisorInverse s.prodPrimes (NairTenenbaum.selbergDiagonal s R) d / s.nu d else 0

theorem NairTenenbaum.selbergWeights_transform (s : BoundingSieve) (R : ℝ) {l : ℕ} (hl : l ∣ s.prodPrimes) : (∑ d ∈ s.prodPrimes.divisors, if l ∣ d then s.nu d * selbergWeights s R d else 0) = selbergDiagonal s R l

theorem NairTenenbaum.selbergWeights_one (s : BoundingSieve) {R : ℝ} (hR : 1 ≤ R) : selbergWeights s R 1 = 1

theorem NairTenenbaum.selbergWeights_mainSum (s : BoundingSieve) {R : ℝ} (hR : 1 ≤ R) : BoundingSieve.mainSum (BoundingSieve.lambdaSquared (selbergWeights s R)) = (selbergDenominator s R)⁻¹

The optimized main quadratic form is exactly the reciprocal denominator.

theorem NairTenenbaum.selbergWeights_eq_zero_of_lt (s : BoundingSieve) {R : ℝ} {d : ℕ} (hRd : R < ↑d) : selbergWeights s R d = 0

The coefficients vanish beyond the chosen cutoff.

theorem NairTenenbaum.selberg_siftedSum_le (s : BoundingSieve) {R : ℝ} (hR : 1 ≤ R) : BoundingSieve.siftedSum ≤ s.totalMass / selbergDenominator s R + BoundingSieve.errSum (BoundingSieve.lambdaSquared (selbergWeights s R))

An upper bound with the optimized main term and the explicit remainder sum. Further estimates of the denominator and remainder are separate analytic steps.