Convergence of the squarefree Hooley moment Dirichlet series

Both the series and its logarithmically weighted series converge for every real argument greater than one. The coefficient bounds are proved rather than imposed as hypotheses on the Dirichlet series.

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

The Dirichlet series of the root-weighted Hooley moment.

Equations

• NairTenenbaum.hooleyDirichlet Q t q σ = ∑' (n : ℕ), NairTenenbaum.hooleyMomentCoefficient Q t q n * ↑n ^ (-σ)

theorem NairTenenbaum.summable_hooleyDirichlet {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {t σ : ℝ} (ht : 0 ≤ t) {q : ℕ} (hq : 0 < q) (hσ : 1 < σ) : Summable fun (n : ℕ) => hooleyMomentCoefficient Q t q n * ↑n ^ (-σ)

theorem NairTenenbaum.summable_log_hooleyDirichlet {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {t σ : ℝ} (ht : 0 ≤ t) {q : ℕ} (hq : 0 < q) (hσ : 1 < σ) : Summable fun (n : ℕ) => hooleyMomentCoefficient Q t q n * Real.log ↑n * ↑n ^ (-σ)

theorem NairTenenbaum.hooleyDirichlet_nonneg (Q : Polynomial ℤ) (t : ℝ) (q : ℕ) (σ : ℝ) : 0 ≤ hooleyDirichlet Q t q σ

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