The prime root series and its logarithmic derivative

The two prime series in the weighted mean argument are related by R′=-P. This identity also permits using the exact prime series as an integrating factor in the differential inequality.

theorem NairTenenbaum.rootPrimeLogWeight_antitone (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) {σ τ : ℝ} (hστ : σ ≤ τ) : rootPrimeLogWeight Q τ p ≤ rootPrimeLogWeight Q σ p

theorem NairTenenbaum.hasDerivAt_rootPrimePowerTerm (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) (σ : ℝ) : HasDerivAt (fun (s : ℝ) => ↑(rootCount Q p) * ↑p ^ (-s)) (-rootPrimeLogWeight Q σ p) σ

theorem NairTenenbaum.hasDerivAt_rootPrimePowerSum {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {σ : ℝ} (hσ : 1 < σ) : HasDerivAt (rootPrimePowerSum Q) (-rootPrimeDirichletSum Q σ) σ

theorem NairTenenbaum.antitoneOn_rootPrimeDirichletSum {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) : AntitoneOn (rootPrimeDirichletSum Q) (Set.Ioi 1)