Bounds for the optimized Selberg coefficients

theorem NairTenenbaum.upperDivisorInverse_eq_sum {P d : ℕ} (hP : P ≠ 0) (hd : d ∣ P) (y : ℕ → ℝ) : upperDivisorInverse P y d = upperDivisorSum P (fun (e : ℕ) => ↑(ArithmeticFunction.moebius (e / d)) * y e) d

theorem NairTenenbaum.upperDivisorSum_multiplicative (f : ArithmeticFunction ℝ) (hf : f.IsMultiplicative) {P d : ℕ} (hP : Squarefree P) (hd : d ∣ P) : upperDivisorSum P (⇑f) d = f d * ∑ k ∈ (P / d).divisors, f k

theorem NairTenenbaum.selberg_upper_sum_le (s : BoundingSieve) {d : ℕ} (hd : d ∣ s.prodPrimes) : upperDivisorSum s.prodPrimes (⇑BoundingSieve.selbergTerms) d ≤ BoundingSieve.selbergTerms d * selbergFullSum s

theorem NairTenenbaum.selbergDiagonal_abs_le (s : BoundingSieve) {R : ℝ} (hR : 1 ≤ R) {d : ℕ} (hd : d ∣ s.prodPrimes) : |selbergDiagonal s R d| ≤ BoundingSieve.selbergTerms d / selbergDenominator s R

theorem NairTenenbaum.selbergWeights_abs_le_ratio (s : BoundingSieve) {R : ℝ} (hR : 1 ≤ R) {d : ℕ} (hd : d ∣ s.prodPrimes) : |selbergWeights s R d| ≤ selbergFullSum s / selbergDenominator s R * ∏ p ∈ d.primeFactors, (1 - s.nu p)⁻¹

A coefficient costs only its local sifting correction, times the ratio between the full and truncated denominators.

theorem NairTenenbaum.selbergWeights_abs_le_four (s : BoundingSieve) {z g : ℝ} (hz : 2 ≤ z) (hzlog : 16 ≤ Real.log z) (hg : 0 < g) (hprimes : ∀ p ∈ s.prodPrimes.primeFactors, ↑p ≤ z) (hdim : ∀ p ∈ s.prodPrimes.primeFactors, s.nu p ≤ g / ↑p) {d : ℕ} (hd : d ∣ s.prodPrimes) : |selbergWeights s (z ^ (2 * g)) d| ≤ 4 * ∏ p ∈ d.primeFactors, (1 - s.nu p)⁻¹

theorem NairTenenbaum.sieve_local_correction_le {g t : ℝ} {p : ℕ} (hg : 1 ≤ g) (hp : 0 < p) (ht : t < 1) (hdim : t ≤ g / ↑p) (hgap : t ≤ 1 - 1 / ↑p) : (1 - t)⁻¹ ≤ 2 * g

Integral root densities have a gap of at least 1/p from one. Together with the degree bound this bounds each local correction by 2g.

theorem NairTenenbaum.exists_selberg_weighted_coefficient_bound {g η : ℝ} (hg : 1 ≤ g) (hη : 0 < η) : ∃ (K : ℝ), 1 ≤ K ∧ ∀ (s : BoundingSieve) (z : ℝ), 2 ≤ z → 16 ≤ Real.log z → (∀ p ∈ s.prodPrimes.primeFactors, ↑p ≤ z) → (∀ p ∈ s.prodPrimes.primeFactors, s.nu p ≤ g / ↑p) → (∀ p ∈ s.prodPrimes.primeFactors, s.nu p ≤ 1 - 1 / ↑p) → ∀ (d : ℕ), d ∣ s.prodPrimes → |selbergWeights s (z ^ (2 * g)) d| * g ^ d.primeFactors.card ≤ K * ↑d ^ η

Weighted Selberg coefficients admit arbitrarily small power majorants, with a constant depending only on the dimension and the chosen exponent.