The weighted Hooley differential inequality

The prime recurrence and Hölder interpolation yield an unconditional differential inequality. The prime series and the divisor Dirichlet series are explicit; sharp bounds for them are not assumed here.

theorem NairTenenbaum.hooleyPrimeDirichlet_row_le {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {t σ : ℝ} (ht : 0 ≤ t) {q : ℕ} (hq : 1 < q) (htq : t ≤ ↑q) (hσ : 1 < σ) (n : ℕ) : ∑' (p : Nat.Primes), hooleyPrimeDirichletTerm Q t q σ (↑p) n ≤ 2 ^ (t / ↑q) * rootPrimeDirichletSum Q σ * (hooleyMomentCoefficient Q t q n * ↑n ^ (-σ)) + rootPrimeDirichletSum Q σ ^ (1 - t / ↑q) * hooleyErrorDirichletTerm Q t q σ n

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

The nonlinear differential inequality before the arithmetic bounds on the two auxiliary series. It holds throughout σ>1 and for 0≤t≤q, q>2.