The smoothed asymptotic behind Wiener--Ikehara

TauCeti.LSeries.tsum_term_mul_fourier_sub_pole_eq_integral_boundary_of_contDiff writes the difference between a Fourier-weighted Dirichlet series and its pole contribution as an integral along the line Re s = 1, for every scale x > 0. That integral carries the oscillating factor x ^ (it), so the Riemann--Lebesgue lemma makes it vanish as x → ∞. This file records the resulting asymptotic, and then evaluates the pole contribution in the limit.

The pole contribution is A * ∫ u in Ici (-log x), 𝓕 psi (u / 2π). As x → ∞ the cutoff -log x runs off to -∞, so the integral fills up the whole line, where Fourier inversion evaluates it as 2π * psi 0. The Fourier-weighted series therefore has the honest limit 2π * A * psi 0; the constant 2π is the Jacobian of the scaling u ↦ u / 2π fixed by the x ^ (it) parameterization.

Only the pole-subtracted remainder G is assumed continuous on the closed half-plane Re s ≥ 1. Nothing is assumed about LSeries a there, where it is a total function with junk values.

Main results

• TauCeti.LSeries.tendsto_tsum_term_mul_fourier_sub_pole_atTop: the Fourier-weighted Dirichlet series and its pole contribution differ by o(1) as the scale x tends to infinity.
• TauCeti.LSeries.tendsto_tsum_term_mul_fourier_atTop: the Fourier-weighted Dirichlet series itself tends to 2π * A * psi 0.

Both are stated for an integrable, compactly supported test function, with the analytic hypotheses that the two limit arguments actually consume: half-line integrability of 𝓕 psi for the first, and integrability of 𝓕 psi together with continuity of psi at 0 for the Fourier inversion in the second. The hypotheses that vary with the scale x are asked for only eventually as x → ∞, which is all an atTop limit consumes. The suffixed ..._of_contDiff forms specialize both to a smooth test function, for which all of those are automatic.

Provenance

The statement obtained by letting x → ∞ in the boundary Fourier identity follows limiting_cor in PrimeNumberTheoremAnd/Wiener.lean of the Apache-2.0 AxiomMath/PrimeNumberTheoremAnd repository, revision 2667e414c38e5a5dc9aa1946f16f13001e5cd3ed, the same source as the sibling files TauCeti.NumberTheory.LSeries.WienerIkehara.Fourier and TauCeti.NumberTheory.LSeries.WienerIkehara.Limit. The evaluation of the limiting pole contribution by Fourier inversion is not in that source, which keeps the truncated integral.

References

• J. Korevaar, Tauberian Theory: A Century of Developments, Chapter III.

theorem TauCeti.LSeries.tendsto_tsum_term_mul_fourier_sub_pole_atTop {a : ℕ → ℂ} {psi : ℝ → ℂ} {G : ℂ → ℂ} {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 : MeasureTheory.Integrable psi MeasureTheory.volume) (hsupp : HasCompactSupport psi) (hFint : ∀ᶠ (x : ℝ) in Filter.atTop, MeasureTheory.IntegrableOn (fun (u : ℝ) => FourierTransform.fourier psi (u / (2 * Real.pi))) (Set.Ici (-Real.log x)) MeasureTheory.volume) (hFsum : ∀ᶠ (x : ℝ) in Filter.atTop, LSeriesSummable (fun (n : ℕ) => a n * FourierTransform.fourier psi (1 / (2 * Real.pi) * Real.log (↑n / x))) 1) : Filter.Tendsto (fun (x : ℝ) => ∑' (n : ℕ), LSeries.term a 1 n * FourierTransform.fourier psi (1 / (2 * Real.pi) * Real.log (↑n / x)) - A * ∫ (u : ℝ) in Set.Ici (-Real.log x), FourierTransform.fourier psi (u / (2 * Real.pi))) Filter.atTop (nhds 0)

As the scale x tends to infinity, the Fourier-weighted Dirichlet series on the line Re s = 1 and the contribution of the pole term A / (s - 1) at s = 1 differ by o(1).

This is the Riemann--Lebesgue lemma applied to the boundary identity tsum_term_mul_fourier_sub_pole_eq_integral_boundary, whose right-hand side is an integral against the oscillating factor x ^ (it). The test function is only required to be integrable and compactly supported, with its Fourier transform integrable on the half-line Ici (-log x) for all large x, which is where the limit reads that identity off.

theorem TauCeti.LSeries.tendsto_tsum_term_mul_fourier_sub_pole_atTop_of_contDiff {a : ℕ → ℂ} {psi : ℝ → ℂ} {G : ℂ → ℂ} {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) (hFsum : ∀ᶠ (x : ℝ) in Filter.atTop, LSeriesSummable (fun (n : ℕ) => a n * FourierTransform.fourier psi (1 / (2 * Real.pi) * Real.log (↑n / x))) 1) : Filter.Tendsto (fun (x : ℝ) => ∑' (n : ℕ), LSeries.term a 1 n * FourierTransform.fourier psi (1 / (2 * Real.pi) * Real.log (↑n / x)) - A * ∫ (u : ℝ) in Set.Ici (-Real.log x), FourierTransform.fourier psi (u / (2 * Real.pi))) Filter.atTop (nhds 0)

The o(1) estimate of tendsto_tsum_term_mul_fourier_sub_pole_atTop for a smooth, compactly supported test function, whose regularity supplies both its own integrability and the half-line integrability of its Fourier transform.

theorem TauCeti.LSeries.tendsto_tsum_term_mul_fourier_atTop {a : ℕ → ℂ} {psi : ℝ → ℂ} {G : ℂ → ℂ} {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 : MeasureTheory.Integrable psi MeasureTheory.volume) (hsupp : HasCompactSupport psi) (hF : MeasureTheory.Integrable (FourierTransform.fourier psi) MeasureTheory.volume) (hpsi0 : ContinuousAt psi 0) (hFsum : ∀ᶠ (x : ℝ) in Filter.atTop, LSeriesSummable (fun (n : ℕ) => a n * FourierTransform.fourier psi (1 / (2 * Real.pi) * Real.log (↑n / x))) 1) : 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. The Fourier-weighted Dirichlet series on the line Re s = 1 tends to 2π * A * psi 0, where A is the coefficient of the pole term A / (s - 1) that the continuous boundary remainder G subtracts off. The hypotheses allow A = 0, in which case no pole is asserted and the limit is 0.

The factor 2π is the Jacobian of the scaling u ↦ u / 2π that the parameterization s = 1 + it forces on the Fourier variable; by Fourier inversion the limiting pole contribution is A * ∫ u : ℝ, 𝓕 psi (u / 2π) = 2π * A * psi 0. The inversion step is what asks for the integrability of 𝓕 psi and the continuity of psi at the single point 0.

theorem TauCeti.LSeries.tendsto_tsum_term_mul_fourier_atTop_of_contDiff {a : ℕ → ℂ} {psi : ℝ → ℂ} {G : ℂ → ℂ} {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) (hFsum : ∀ᶠ (x : ℝ) in Filter.atTop, LSeriesSummable (fun (n : ℕ) => a n * FourierTransform.fourier psi (1 / (2 * Real.pi) * Real.log (↑n / x))) 1) : 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 a smooth, compactly supported test function, whose regularity supplies its integrability, the integrability of its Fourier transform and its continuity at 0.