Removing the linear term in the Hooley differential inequality

The exact prime root series supplies the integrating factor. After the divisor Euler bound, the derivative majorant contains only the two prime series and explicit constants.

noncomputable def NairTenenbaum.hooleyReducedMoment (Q : Polynomial ℤ) (t : ℝ) (q : ℕ) (σ : ℝ) : ℝ

The Hooley moment after removing the principal singular factor.

Equations

• NairTenenbaum.hooleyReducedMoment Q t q σ = Real.exp (-2 ^ (t / ↑q) * (1 / (↑q - 1)) * NairTenenbaum.rootPrimePowerSum Q σ) * NairTenenbaum.hooleyDirichlet Q t q σ ^ (1 / (↑q - 1))

theorem NairTenenbaum.differentiableAt_hooleyReducedMoment {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {t σ : ℝ} (ht : 0 ≤ t) {q : ℕ} (hq : 0 < q) (hσ : 1 < σ) : DifferentiableAt ℝ (hooleyReducedMoment Q t q) σ

theorem NairTenenbaum.neg_deriv_hooleyReducedMoment_le {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {t σ : ℝ} (ht : 0 ≤ t) {q : ℕ} (hq : 2 < q) (htq : t ≤ ↑q) (hσ : 1 < σ) : -deriv (hooleyReducedMoment Q t q) σ ≤ hooleyPrimeErrorConstant Q q ^ (t / ↑q) / (↑q - 1) * rootPrimeDirichletSum Q σ ^ (1 - t / ↑q) * Real.exp ((2 ^ t - 2 ^ (t / ↑q)) / (↑q - 1) * rootPrimePowerSum Q σ)