An explicit power majorant for irreducible polynomial moments

The proved prime-root logarithmic bound turns the differential majorant into a pure power of σ−1. The constants are uniform in the moment order.

noncomputable def NairTenenbaum.hooleyPoleCoefficient (Q : Polynomial ℤ) (t : ℝ) (q : ℕ) (C : ℝ) : ℝ

The coefficient in the Hooley Dirichlet-series pole majorant.

Equations

• One or more equations did not get rendered due to their size.

theorem NairTenenbaum.hooleyPoleCoefficient_nonneg (Q : Polynomial ℤ) (t C : ℝ) {q : ℕ} (hq : 2 < q) : 0 ≤ hooleyPoleCoefficient Q t q C

theorem NairTenenbaum.exp_mul_le_of_log_pole {R C δ κ : ℝ} (hδ : 0 < δ) (hκ : 0 ≤ κ) (hR : R ≤ C - Real.log δ) : Real.exp (κ * R) ≤ Real.exp (κ * C) * δ ^ (-κ)

theorem NairTenenbaum.hooleyReducedMomentMajorant_le_power {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {t σ C : ℝ} (ht : 0 ≤ t) {q : ℕ} (hq : 2 < q) (htq : t ≤ ↑q) (hσ : 1 < σ) (hσ₂ : σ ≤ 2) (hR : rootPrimePowerSum Q σ ≤ C - Real.log (σ - 1)) : hooleyReducedMomentMajorant Q t q σ ≤ hooleyPoleCoefficient Q t q C * (σ - 1) ^ (-1 - hooleyMomentExponentGap t q)