Differentiating the Hooley moment Dirichlet series #
A summable logarithmic majorant on each smaller half-line justifies the termwise derivative used in the weighted mean proof.
theorem
NairTenenbaum.hasDerivAt_hooleyDirichlet_term
(Q : Polynomial ℤ)
(t : ℝ)
(q n : ℕ)
(σ : ℝ)
:
HasDerivAt (fun (s : ℝ) => hooleyMomentCoefficient Q t q n * ↑n ^ (-s))
(-(hooleyMomentCoefficient Q t q n * Real.log ↑n * ↑n ^ (-σ))) σ
theorem
NairTenenbaum.hasDerivAt_hooleyDirichlet
{Q : Polynomial ℤ}
(hQ : NoFixedPrimeDivisor Q)
{t σ : ℝ}
(ht : 0 ≤ t)
{q : ℕ}
(hq : 0 < q)
(hσ : 1 < σ)
:
HasDerivAt (hooleyDirichlet Q t q) (-∑' (n : ℕ), hooleyMomentCoefficient Q t q n * Real.log ↑n * ↑n ^ (-σ)) σ
theorem
NairTenenbaum.deriv_hooleyDirichlet
{Q : Polynomial ℤ}
(hQ : NoFixedPrimeDivisor Q)
{t σ : ℝ}
(ht : 0 ≤ t)
{q : ℕ}
(hq : 0 < q)
(hσ : 1 < σ)
: