The Wiener--Ikehara theorem

Let a n ≥ 0 have Dirichlet series F s = ∑ a n n⁻ˢ convergent on Re s > 1, and suppose that F s - κ / (s - 1) agrees on Re s > 1 with a function G continuous on Re s ≥ 1. The Wiener--Ikehara theorem says that the partial sums then grow like κ x: x⁻¹ ∑_{1 ≤ n ≤ x} a n → κ as x → ∞.

The analytic input is the smoothed asymptotic TauCeti.LSeries.tendsto_tsum_term_mul_fourier_schwartz_atTop, which evaluates the limit of ∑ a n / n * 𝓕 g (log (n / x) / 2π) for a Schwartz function g. This file makes two passes.

• Smooth cutoffs. For a smooth function Ψ with compact support inside (0, ∞), the weight W v = e^{2πv} Ψ(e^{2πv}) is smooth and compactly supported, hence the Fourier transform of the Schwartz function g = 𝓕⁻ W, and a n / n * W (log (n / x) / 2π) = x⁻¹ a n Ψ (n / x). Since g 0 = ∫ W = (2π)⁻¹ ∫_{(0, ∞)} Ψ, this gives x⁻¹ ∑ a n Ψ (n / x) → A ∫_{(0, ∞)} Ψ.
• The sharp cutoff. The indicator of (0, 1] is squeezed between two bump functions. The lower bump is supported in (0, 1); the upper bump equals 1 on [ε, 1], and the coefficients with n ≤ ε x that it misses are controlled by the Chebyshev bound TauCeti.LSeries.isBigO_sum_Icc_norm_id_of_boundary. Letting ε → 0 gives the theorem.

The coefficients are real and nonnegative, the hypothesis on the series is LSeriesHasSum on the open half-plane (Mathlib's LSeries is a total function, zero where the series diverges), and the continuous extension is a separately named function G, so no junk value of F at s = 1 or on the line Re s = 1 is ever used. The sign of κ is not assumed: it is forced by the conclusion.

Main results

• TauCeti.LSeries.tendsto_inv_mul_tsum_mul_div_atTop: the smoothed asymptotic x⁻¹ ∑ a n Ψ (n / x) → A ∫_{(0, ∞)} Ψ for a smooth Ψ with compact support in (0, ∞).
• TauCeti.LSeries.wienerIkehara: the Wiener--Ikehara theorem, x⁻¹ ∑_{1 ≤ n ≤ x} a n → κ.
• TauCeti.LSeries.wienerIkehara_zero: the case κ = 0, in which F itself extends continuously to Re s ≥ 1 and the partial sums are o(x).

Provenance

The passage from Schwartz test functions to smooth cutoffs on (0, ∞) and then to the sharp cutoff follows WienerIkeharaSmooth, WienerIkeharaInterval and WienerIkeharaTheorem' in PrimeNumberTheoremAnd/Wiener.lean of the Apache-2.0 AxiomMath/PrimeNumberTheoremAnd repository, revision 2667e414c38e5a5dc9aa1946f16f13001e5cd3ed, the same source as the sibling files in this directory. Here the smooth step is derived from the Schwartz-function asymptotic by Fourier inversion on 𝓢(ℝ, ℂ), and the sharp step squeezes directly between two ContDiffBumps, spending the Chebyshev bound only on the initial segment n ≤ ε x.

References

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

Smooth cutoffs on the positive half-line

theorem TauCeti.LSeries.tendsto_inv_mul_tsum_mul_div_atTop {Ψ : ℝ → ℂ} {a : ℕ → ℂ} {A : ℂ} {G : ℂ → ℂ} (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) (hΨ : ContDiff ℝ (↑⊤) Ψ) (hΨc : HasCompactSupport Ψ) (hΨpos : tsupport Ψ ⊆ Set.Ioi 0) : Filter.Tendsto (fun (x : ℝ) => (↑x)⁻¹ * ∑' (n : ℕ), a n * Ψ (↑n / x)) Filter.atTop (nhds (A * ∫ (y : ℝ) in Set.Ioi 0, Ψ y))

The smoothed Wiener--Ikehara asymptotic for a cutoff on (0, ∞). Let a be nonnegative, with Dirichlet series summable on Re s > 1 and a boundary remainder G = LSeries a - A / (s - 1) continuous on Re s ≥ 1. For every smooth Ψ whose support is a compact subset of (0, ∞), x⁻¹ ∑ a n Ψ (n / x) → A ∫_{(0, ∞)} Ψ as x → ∞.

Bump functions on the positive half-line

The sharp cutoff

theorem TauCeti.LSeries.wienerIkehara {a : ℕ → ℝ} {F G : ℂ → ℂ} {κ : ℝ} (ha : 0 ≤ a) (hF : ∀ (s : ℂ), 1 < s.re → LSeriesHasSum (fun (n : ℕ) => ↑(a n)) s (F s)) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hGF : ∀ (s : ℂ), 1 < s.re → G s = F s - ↑κ / (s - 1)) : Filter.Tendsto (fun (x : ℝ) => x⁻¹ * ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, a n) Filter.atTop (nhds κ)

The Wiener--Ikehara theorem. Let a n ≥ 0 have Dirichlet series with sum F s on Re s > 1, and let G be continuous on Re s ≥ 1 with G s = F s - κ / (s - 1) on Re s > 1. Then x⁻¹ ∑_{1 ≤ n ≤ x} a n → κ as x → ∞.

theorem TauCeti.LSeries.wienerIkehara_zero {a : ℕ → ℝ} {F G : ℂ → ℂ} (ha : 0 ≤ a) (hF : ∀ (s : ℂ), 1 < s.re → LSeriesHasSum (fun (n : ℕ) => ↑(a n)) s (F s)) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hGF : ∀ (s : ℂ), 1 < s.re → G s = F s) : Filter.Tendsto (fun (x : ℝ) => x⁻¹ * ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, a n) Filter.atTop (nhds 0)

The Wiener--Ikehara theorem with zero residue. If the Dirichlet series F of a n ≥ 0 extends continuously from Re s > 1 to Re s ≥ 1, then x⁻¹ ∑_{1 ≤ n ≤ x} a n → 0.