The Wiener-Ikehara Tauberian theorem

Let f : ℕ → ℝ be non-negative with ∑ n ≤ x, f n ≪ x, whose L-series F extends continuously to Re s ≥ 1 after subtracting A / (s - 1). Then ∑ n < N, f n = A * N + o(N).

The classical theorem does not need the bound ∑ n ≤ x, f n ≪ x, only the convergence of F(s) for Re s > 1 (which the bound implies); it is assumed here because it simplifies the proof.

Main results

• WienerIkehara.tendsto_sum_div, WienerIkehara.tendsto_sum_range_div: the Wiener-Ikehara Tauberian theorem, summing over reals n ≤ x and over naturals n < N respectively.
• WienerIkehara.tendsto_sum_div_smooth, WienerIkehara.tendsto_sum_div_smooth_real: versions for smooth cutoffs.

Proof outline

Writing ψ̂ for the Fourier transform, the proof studies S f A σ ψ̂ x, the difference between ∑' n, term f σ n * ψ̂ (log (n / x) / (2 * π)) and its polar counterpart. Rewriting both halves as Fourier integrals (sum_term_mul_fourier_eq, integral_exp_mul_fourier_eq) cancels the pole and expresses S through G (sum_term_mul_sub_mul_integral_eq); letting σ → 1 and applying the Riemann-Lebesgue lemma gives S f A 1 ψ̂ x → 0, first for compactly supported test functions (tendsto_S_one_fourier_of_hasCompactSupport) and then for all Schwartz functions (tendsto_S_one_fourier). Surjectivity of the Fourier transform on Schwartz space upgrades this to a smoothed form of the theorem (tendsto_sum_div_smooth_real), and non-negativity of f together with a smooth Urysohn lemma (exists_cutoff) replaces the smooth cutoff by the indicator of an interval, whence the theorem (tendsto_sum_div).

This file is adapted from the PrimeNumberTheoremAnd project.

theorem WienerIkehara.tendsto_sum_div_smooth {f : ℕ → ℝ} {C A : ℝ} {G : ℂ → ℂ} (bound : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ C * ↑n) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hG' : Set.EqOn G (fun (s : ℂ) => LSeries (fun (n : ℕ) => ↑(f n)) s - ↑A / (s - 1)) {s : ℂ | 1 < s.re}) (hpos : 0 ≤ f) {ψ : ℝ → ℂ} (hsmooth : ContDiff ℝ (↑⊤) ψ) (hsupp : HasCompactSupport ψ) (hplus : tsupport ψ ⊆ Set.Ioi 0) : Filter.Tendsto (fun (x : ℝ) => (∑' (n : ℕ), ↑(f n) * ψ (↑n / x)) / ↑x) Filter.atTop (nhds (↑A * ∫ (y : ℝ) in Set.Ioi 0, ψ y))

A smoothed Wiener-Ikehara Tauberian Theorem: If f is a nonnegative arithmetic function with ∑ i < n, f i ≤ C * n whose L-series has a simple pole at s = 1 with residue A and otherwise extends continuously to the closed half-plane re s ≥ 1, then f behaves like A asymptotically with respect to smooth weights with compact support in (0, ∞).

theorem WienerIkehara.tendsto_sum_div_smooth_real {f : ℕ → ℝ} {C A : ℝ} {G : ℂ → ℂ} (bound : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ C * ↑n) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hG' : Set.EqOn G (fun (s : ℂ) => LSeries (fun (n : ℕ) => ↑(f n)) s - ↑A / (s - 1)) {s : ℂ | 1 < s.re}) (hpos : 0 ≤ f) {Ψ : ℝ → ℝ} (hsmooth : ContDiff ℝ (↑⊤) Ψ) (hsupp : HasCompactSupport Ψ) (hplus : tsupport Ψ ⊆ Set.Ioi 0) : Filter.Tendsto (fun (x : ℝ) => (∑' (n : ℕ), f n * Ψ (↑n / x)) / x) Filter.atTop (nhds (A * ∫ (y : ℝ) in Set.Ioi 0, Ψ y))

A version of smoothed Wiener-Ikehara for real-valued cutoffs.

theorem WienerIkehara.tendsto_sum_range_div {f : ℕ → ℝ} {C A : ℝ} {G : ℂ → ℂ} (bound : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ C * ↑n) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hG' : Set.EqOn G (fun (s : ℂ) => LSeries (fun (n : ℕ) => ↑(f n)) s - ↑A / (s - 1)) {s : ℂ | 1 < s.re}) (hpos : 0 ≤ f) : Filter.Tendsto (fun (N : ℕ) => (∑ i ∈ Finset.range N, f i) / ↑N) Filter.atTop (nhds A)

The Wiener-Ikehara Tauberian Theorem, summing over naturals n < N; see WienerIkehara.tendsto_sum_div for the version summing over reals n ≤ x.

theorem WienerIkehara.tendsto_sum_div {f : ℕ → ℝ} {C A : ℝ} {G : ℂ → ℂ} (bound : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ C * ↑n) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hG' : Set.EqOn G (fun (s : ℂ) => LSeries (fun (n : ℕ) => ↑(f n)) s - ↑A / (s - 1)) {s : ℂ | 1 < s.re}) (hpos : 0 ≤ f) : Filter.Tendsto (fun (x : ℝ) => (∑ n ∈ Finset.Icc 0 ⌊x⌋₊, f n) / x) Filter.atTop (nhds A)

The Wiener-Ikehara Tauberian Theorem, summing over naturals n ≤ x for real x; see WienerIkehara.tendsto_sum_range_div for the version summing over naturals n < N.