Divisor windows and moment truncation for Theorem 2

noncomputable def NairTenenbaum.dyadicDivisorCount (n : ℕ) (y : ℝ) : ℕ

The number of divisors in the dyadic interval above half the cutoff.

Equations

• NairTenenbaum.dyadicDivisorCount n y = {d ∈ n.divisors | y / 2 < ↑d ∧ ↑d ≤ y}.card

noncomputable def NairTenenbaum.polynomialDivisorWindowSum (Q : Polynomial ℤ) (x y : ℝ) : ℝ

The sum of dyadic divisor counts over polynomial values in the short interval.

Equations

• NairTenenbaum.polynomialDivisorWindowSum Q x y = ∑ n ∈ NairTenenbaum.shortInterval x y, ↑(NairTenenbaum.dyadicDivisorCount (Polynomial.eval (↑n) Q).natAbs y)

noncomputable def NairTenenbaum.polynomialDivisorHitCount (Q : Polynomial ℤ) (x y : ℝ) : ℕ

The number of polynomial values with at least one divisor in the chosen window.

Equations

• NairTenenbaum.polynomialDivisorHitCount Q x y = {n ∈ NairTenenbaum.shortInterval x y | 0 < NairTenenbaum.dyadicDivisorCount (Polynomial.eval (↑n) Q).natAbs y}.card

theorem NairTenenbaum.dyadicDivisorCount_le_hooleyDelta (n : ℕ) {y : ℝ} (hy : 0 < y) : dyadicDivisorCount n y ≤ hooleyDelta n

theorem NairTenenbaum.self_le_inv_rpow_mul_rpow {w T ε : ℝ} (hT : 0 < T) (hw : T ≤ w) (hε : 0 ≤ ε) : w ≤ T ^ (-ε) * w ^ (1 + ε)

theorem NairTenenbaum.polynomialDivisorWindow_large_sum_le (Q : Polynomial ℤ) {x y T ε : ℝ} (hy : 0 < y) (hT : 0 < T) (hε : 0 ≤ ε) : ∑ n ∈ shortInterval x y with T < ↑(dyadicDivisorCount (Polynomial.eval (↑n) Q).natAbs y), ↑(dyadicDivisorCount (Polynomial.eval (↑n) Q).natAbs y) ≤ T ^ (-ε) * hooleyPolynomialSum Q (1 + ε) x y

theorem NairTenenbaum.polynomialDivisorWindow_small_sum_le (Q : Polynomial ℤ) (x y : ℝ) {T : ℝ} (hT : 0 ≤ T) : ∑ n ∈ shortInterval x y with ↑(dyadicDivisorCount (Polynomial.eval (↑n) Q).natAbs y) ≤ T, ↑(dyadicDivisorCount (Polynomial.eval (↑n) Q).natAbs y) ≤ T * ↑(polynomialDivisorHitCount Q x y)