Variants of the Wiener--Ikehara theorem

TauCeti.LSeries.wienerIkehara treats nonnegative coefficients whose Dirichlet series has a simple pole at s = 1, and reads the partial sums at a real cutoff. This file derives three variants that arise when the theorem is applied.

• Finitely many negative coefficients. Only eventual nonnegativity of the coefficients is needed: changing finitely many coefficients subtracts a finite Dirichlet polynomial from both the series and its boundary remainder, which keeps the remainder continuous, and changes the partial sums by a bounded amount, which is invisible after division by x.
• Natural cutoffs. The same limit along the natural numbers N → ∞.
• A pole at a positive abscissa. If the series converges on Re s > σ for some σ > 0 and F s - κ / (s - σ) extends continuously to Re s ≥ σ, then x ^ (-σ) ∑_{1 ≤ n ≤ x} a n → κ / σ. The coefficients a n n ^ (1 - σ) have the series F (s + σ - 1), which has its pole at 1, so the theorem at 1 shows that their partial sums grow like κ x; Abel summation against t ^ (σ - 1), in the form TauCeti.tendsto_rpow_inv_mul_sum_Icc_rpow_mul, then recovers the partial sums of a itself.

As in TauCeti.LSeries.wienerIkehara, the series hypothesis is LSeriesHasSum on the open half-plane and the continuous boundary remainder is a separately named function G.

Main results

• TauCeti.LSeries.wienerIkehara_of_eventually_nonneg: the theorem for eventually nonnegative coefficients.
• TauCeti.LSeries.wienerIkehara_nat: the same conclusion along natural cutoffs.
• TauCeti.LSeries.wienerIkehara_rpow: the theorem for a pole at σ > 0, x ^ (-σ) ∑_{1 ≤ n ≤ x} a n → κ / σ.

References

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

theorem TauCeti.LSeries.wienerIkehara_of_eventually_nonneg {a : ℕ → ℝ} {F G : ℂ → ℂ} {κ : ℝ} (ha : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ a n) (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 for eventually nonnegative coefficients. Let a n ≥ 0 for all large n, let the Dirichlet series of a have 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_nat {a : ℕ → ℝ} {F G : ℂ → ℂ} {κ : ℝ} (ha : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ a n) (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 (N : ℕ) => (↑N)⁻¹ * ∑ n ∈ Finset.Icc 1 N, a n) Filter.atTop (nhds κ)

The Wiener--Ikehara theorem at natural cutoffs. Under the hypotheses of TauCeti.LSeries.wienerIkehara_of_eventually_nonneg, N⁻¹ ∑_{1 ≤ n ≤ N} a n → κ as N → ∞ through the natural numbers.

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

The Wiener--Ikehara theorem for a pole at a positive abscissa. Let σ > 0, let a n ≥ 0 for all large n, let the Dirichlet series of a have sum F s on Re s > σ, and let G be continuous on Re s ≥ σ with G s = F s - κ / (s - σ) on Re s > σ. Then x ^ (-σ) ∑_{1 ≤ n ≤ x} a n → κ / σ as x → ∞.

For σ = 1 this is TauCeti.LSeries.wienerIkehara_of_eventually_nonneg.