Quantitative control of the Selberg remainder

theorem NairTenenbaum.sum_lcm_expand {P d : ℕ} (hP : P ≠ 0) (hd : d ∣ P) (f : ℕ → ℕ → ℝ) : (∑ a ∈ d.divisors, ∑ b ∈ d.divisors, if d = a.lcm b then f a b else 0) = ∑ a ∈ P.divisors, ∑ b ∈ P.divisors, if d = a.lcm b then f a b else 0

A pair with least common multiple d consists of divisors of d, so extending both inner sums to all divisors of P adds only zero terms.

theorem NairTenenbaum.lambdaSquared_weighted_abs_le {P : ℕ} (hP : P ≠ 0) (w E : ℕ → ℝ) (hE : ∀ (d : ℕ), d ∣ P → 0 ≤ E d) : ∑ d ∈ P.divisors, |BoundingSieve.lambdaSquared w d| * E d ≤ ∑ a ∈ P.divisors, ∑ b ∈ P.divisors, |w a| * |w b| * E (a.lcm b)

The weighted absolute sum of squared sieve coefficients is bounded by a quadratic sum over the original coefficients.

theorem NairTenenbaum.selberg_errSum_le_square (s : BoundingSieve) (w E : ℕ → ℝ) {C : ℝ} (hC : 0 ≤ C) (hE : ∀ (d : ℕ), d ∣ s.prodPrimes → 0 ≤ E d) (hlcm : ∀ (a : ℕ), a ∣ s.prodPrimes → ∀ (b : ℕ), b ∣ s.prodPrimes → E (a.lcm b) ≤ E a * E b) (herr : ∀ (d : ℕ), d ∣ s.prodPrimes → |BoundingSieve.rem d| ≤ C * E d) : BoundingSieve.errSum (BoundingSieve.lambdaSquared w) ≤ C * (∑ d ∈ s.prodPrimes.divisors, |w d| * E d) ^ 2

A submultiplicative majorant for the local remainders yields a square of a single coefficient sum.

theorem NairTenenbaum.coefficient_sum_le_rpow {P : ℕ} (w E : ℕ → ℝ) {R K η : ℝ} (hR : 1 ≤ R) (hK : 0 ≤ K) (hη : 0 ≤ η) (hsupport : ∀ (d : ℕ), R < ↑d → w d = 0) (hbound : ∀ (d : ℕ), d ∣ P → d ≠ 0 → |w d| * E d ≤ K * ↑d ^ η) : ∑ d ∈ P.divisors, |w d| * E d ≤ K * R ^ (1 + η)

A coefficient sum supported up to R inherits a pointwise power bound.

theorem NairTenenbaum.selberg_errSum_le_rpow (s : BoundingSieve) (w E : ℕ → ℝ) {C R K η : ℝ} (hC : 0 ≤ C) (hR : 1 ≤ R) (hK : 0 ≤ K) (hη : 0 ≤ η) (hE : ∀ (d : ℕ), d ∣ s.prodPrimes → 0 ≤ E d) (hlcm : ∀ (a : ℕ), a ∣ s.prodPrimes → ∀ (b : ℕ), b ∣ s.prodPrimes → E (a.lcm b) ≤ E a * E b) (herr : ∀ (d : ℕ), d ∣ s.prodPrimes → |BoundingSieve.rem d| ≤ C * E d) (hsupport : ∀ (d : ℕ), R < ↑d → w d = 0) (hbound : ∀ (d : ℕ), d ∣ s.prodPrimes → d ≠ 0 → |w d| * E d ≤ K * ↑d ^ η) : BoundingSieve.errSum (BoundingSieve.lambdaSquared w) ≤ C * K ^ 2 * R ^ (2 + 2 * η)

The error is of order R^(2+2η) whenever the weighted coefficients have a uniform d^η majorant.

theorem NairTenenbaum.exists_selberg_upper_bound {g η : ℝ} (hg : 1 ≤ g) (hη : 0 < η) : ∃ (K : ℝ), 1 ≤ K ∧ ∀ (s : BoundingSieve) (z C : ℝ), 2 ≤ z → 16 ≤ Real.log z → 0 ≤ C → 0 ≤ s.totalMass → (∀ 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 → |BoundingSieve.rem d| ≤ C * g ^ d.primeFactors.card) → BoundingSieve.siftedSum ≤ 4 * s.totalMass * ∏ p ∈ s.prodPrimes.primeFactors, (1 - s.nu p) + C * K * z ^ (4 * g * (1 + η))

A quantitative Selberg upper bound, uniform in the sieve and its prime set. The constant depends only on the dimension and the error exponent.