A growth bound for nonnegative coefficients, and the summability it supplies

The smoothed Wiener--Ikehara asymptotic TauCeti.LSeries.tendsto_tsum_term_mul_fourier_atTop still carries a summability hypothesis: the Fourier-weighted series ∑ a n 𝓕 psi (log (n / x) / 2π) / n has to converge on the boundary line Re s = 1, where the coefficients are no longer damped by n ^ (-(sigma - 1)). This file removes that hypothesis for nonnegative coefficients, which is the only case Wiener--Ikehara is about.

The input is coefficient nonnegativity together with the boundary remainder data on the real segment sigma ∈ (1, 2]; the growth bound for the partial sums is derived from them, not assumed. Nonnegativity turns the boundary data into the one-sided estimate ∑ ‖a n‖ / n ^ sigma ≤ B / (sigma - 1) on (1, 2], and inserting sigma = 1 + 1 / log t into it bounds ∑_{n ≤ t} ‖a n‖ by a multiple of t log t. That is weaker than the Chebyshev bound O(t) which Wiener--Ikehara ultimately proves, but it is available before any Tauberian argument, and one logarithm to spare is all the summability needs: the Fourier transform of a smooth compactly supported function decays faster than |v| ^ (-3), so the factor attached to a n is O((log n) ^ (-3)), and the Abel-summation bound TauCeti.LSeries.LSeriesSummable_mul_of_norm_le converts O(t log t) partial sums into a convergent series.

Only the values of the boundary remainder on the real segment sigma ∈ (1, 2] enter the growth bound, so the results below are stated with the boundary data restricted to that segment; the final asymptotic specializes the half-plane hypotheses it inherits from TauCeti.LSeries.tendsto_tsum_term_mul_fourier_atTop_of_contDiff.

Main results

• TauCeti.LSeries.tsum_norm_term_le_of_boundary: nonnegative coefficients with a boundary remainder continuous on the segment [1, 2] have a convergent norm series with ∑ ‖term a sigma n‖ ≤ B / (sigma - 1) on (1, 2].
• TauCeti.LSeries.isBigO_sum_Icc_norm_of_boundary: the resulting O(t log t) bound for the partial sums.
• TauCeti.LSeries.LSeriesSummable_mul_fourier_of_nonneg: the Fourier weight is small enough for that bound to force summability at s = 1, at every scale x > 0.
• TauCeti.LSeries.tendsto_tsum_term_mul_fourier_atTop_of_nonneg: the smoothed Wiener--Ikehara asymptotic for nonnegative coefficients, with no summability hypothesis left.

References

• J. Korevaar, Tauberian Theory: A Century of Developments, Chapter III.
• G. Tenenbaum, Introduction to Analytic and Probabilistic Number Theory, Chapter II.

The one-sided bound coming from the boundary data

theorem TauCeti.LSeries.tsum_norm_term_le_of_boundary {a : ℕ → ℂ} {A : ℂ} {G : ℂ → ℂ} (ha : 0 ≤ a) (hG : ContinuousOn (fun (sigma : ℝ) => G ↑sigma) (Set.Icc 1 2)) (hG' : ∀ (sigma : ℝ), 1 < sigma → sigma ≤ 2 → G ↑sigma = LSeries a ↑sigma - A / (↑sigma - 1)) (hsum : ∀ (sigma : ℝ), 1 < sigma → sigma ≤ 2 → LSeriesSummable a ↑sigma) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ (sigma : ℝ), 1 < sigma → sigma ≤ 2 → (Summable fun (n : ℕ) => ‖LSeries.term a (↑sigma) n‖) ∧ ∑' (n : ℕ), ‖LSeries.term a (↑sigma) n‖ ≤ B / (sigma - 1)

For nonnegative coefficients, a boundary remainder G continuous on the real segment [1, 2] bounds the Dirichlet series on (1, 2] by B / (sigma - 1): the remainder is bounded on the compact segment, and the pole term contributes ‖A‖ / (sigma - 1).

No analytic continuation is used, only the values of G on that segment and the identity G = LSeries a - A / (s - 1) on its interior.

The partial-sum bound

theorem TauCeti.LSeries.isBigO_sum_Icc_norm_of_boundary {a : ℕ → ℂ} {A : ℂ} {G : ℂ → ℂ} (ha : 0 ≤ a) (hG : ContinuousOn (fun (sigma : ℝ) => G ↑sigma) (Set.Icc 1 2)) (hG' : ∀ (sigma : ℝ), 1 < sigma → sigma ≤ 2 → G ↑sigma = LSeries a ↑sigma - A / (↑sigma - 1)) (hsum : ∀ (sigma : ℝ), 1 < sigma → sigma ≤ 2 → LSeriesSummable a ↑sigma) : (fun (t : ℝ) => ∑ k ∈ Finset.Icc 1 ⌊t⌋₊, ‖a k‖) =O[Filter.atTop] fun (t : ℝ) => t * Real.log t

A crude growth bound for the partial sums. Nonnegative coefficients whose Dirichlet series has a boundary remainder continuous on the segment [1, 2] satisfy ∑_{1 ≤ n ≤ t} ‖a n‖ = O(t log t).

The proof inserts sigma = 1 + 1 / log t into tsum_norm_term_le_of_boundary: the truncation n ≤ t costs a factor t ^ sigma = e t, and the bound B / (sigma - 1) is B log t. This is one logarithm short of the Chebyshev bound O(t) that Wiener--Ikehara eventually delivers, but it needs no Tauberian input.

The Fourier weight

theorem TauCeti.LSeries.LSeriesSummable_mul_fourier_of_nonneg {a : ℕ → ℂ} {A : ℂ} {G : ℂ → ℂ} {psi : ℝ → ℂ} {x : ℝ} (ha : 0 ≤ a) (hG : ContinuousOn (fun (sigma : ℝ) => G ↑sigma) (Set.Icc 1 2)) (hG' : ∀ (sigma : ℝ), 1 < sigma → sigma ≤ 2 → G ↑sigma = LSeries a ↑sigma - A / (↑sigma - 1)) (hsum : ∀ (sigma : ℝ), 1 < sigma → sigma ≤ 2 → LSeriesSummable a ↑sigma) (hpsi : ContDiff ℝ (↑⊤) psi) (hsupp : HasCompactSupport psi) (hx : 0 < x) : LSeriesSummable (fun (n : ℕ) => a n * FourierTransform.fourier psi (1 / (2 * Real.pi) * Real.log (↑n / x))) 1

The Fourier-weighted series converges on the boundary line. For nonnegative coefficients with a boundary remainder continuous on the segment [1, 2] and a smooth compactly supported test function, the series tested at scale x > 0 is summable at s = 1. This discharges the standing summability hypothesis of TauCeti.LSeries.tendsto_tsum_term_mul_fourier_atTop_of_contDiff.

theorem TauCeti.LSeries.tendsto_tsum_term_mul_fourier_atTop_of_nonneg {a : ℕ → ℂ} {A : ℂ} {G : ℂ → ℂ} {psi : ℝ → ℂ} (ha : 0 ≤ a) (hG : ContinuousOn G {z : ℂ | 1 ≤ z.re}) (hG' : ∀ (z : ℂ), 1 < z.re → G z = LSeries a z - A / (z - 1)) (hsum : ∀ (sigma : ℝ), 1 < sigma → LSeriesSummable a ↑sigma) (hpsi : ContDiff ℝ (↑⊤) psi) (hsupp : HasCompactSupport psi) : Filter.Tendsto (fun (x : ℝ) => ∑' (n : ℕ), LSeries.term a 1 n * FourierTransform.fourier psi (1 / (2 * Real.pi) * Real.log (↑n / x))) Filter.atTop (nhds (2 * ↑Real.pi * A * psi 0))

The smoothed Wiener--Ikehara asymptotic for nonnegative coefficients. Testing the Dirichlet series of a nonnegative coefficient system against a smooth compactly supported function on the line Re s = 1 gives the limit 2π A psi 0, where A is the residue subtracted off by the continuous boundary remainder G.

This is TauCeti.LSeries.tendsto_tsum_term_mul_fourier_atTop_of_contDiff with its summability hypothesis discharged: for nonnegative coefficients the boundary data itself forces the Fourier-weighted series to converge at every large scale. The hypotheses are now exactly the analytic input of Wiener--Ikehara.