Documentation

TauCeti.NumberTheory.LSeries.Summable

Summability at s = 1 of a logarithmically damped Dirichlet series #

A Dirichlet series whose coefficients have O(t log t) partial sums need not converge on the line Re s = 1, but it does converge there once each coefficient is weighted by a factor of size O((1 + log n) ^ (-3)): in the Abel-summation bound TauCeti.summable_div_mul_one_add_log_cube, one of the three logarithms absorbs the log t in the growth of the partial sums, and the remaining two leave the integrable majorant (t (1 + log t) ^ 2)⁻¹.

Such a weight arises whenever a Dirichlet series is tested against a smooth compactly supported function, whose Fourier transform decays faster than every power.

Main declarations #

theorem TauCeti.LSeries.LSeriesSummable_mul_of_norm_le {a W : ℕ → ℂ} {D : ℝ} (hgrowth : (fun (t : ℝ) => ∑ k ∈ Finset.Icc 1 ⌊t⌋₊, ‖a k‖) =O[Filter.atTop] fun (t : ℝ) => t * Real.log t) (hW : ∀ᶠ (n : ℕ) in Filter.atTop, ‖W n‖ ≤ D / (1 + Real.log ↑n) ^ 3) :
LSeriesSummable (fun (n : ℕ) => a n * W n) 1

Weighting coefficients with an O((1 + log n) ^ (-3)) factor leaves a Dirichlet series that converges at s = 1, as soon as the partial sums of ‖a‖ are O(t log t).