Fourier identities for Wiener--Ikehara

The Fourier proof of Wiener--Ikehara starts by testing a Dirichlet series against an integrable function on a vertical line. This file records the two exact identities used in that step. The first exchanges the Dirichlet series with the integral. The second computes the contribution of the simple pole at s = 1. Their combination expresses the difference as the integral of the pole-subtracted remainder, a function agreeing with LSeries a - A / (s - 1) on the open vertical line Re s = sigma; nothing about its boundary behaviour is asserted or used here.

Main results

• TauCeti.LSeries.tsum_term_mul_fourier_eq_integral is the Fourier identity for a convergent Dirichlet series.
• TauCeti.LSeries.integral_exp_mul_fourier_eq computes the pole term.
• TauCeti.LSeries.tsum_term_mul_fourier_sub_pole_eq_integral combines the two when a named function agrees with the pole-subtracted remainder on the vertical line.

Provenance

The proofs are adapted from PrimeNumberTheoremAnd/Wiener.lean in the Apache-2.0 AxiomMath/PrimeNumberTheoremAnd repository, revision 2667e414c38e5a5dc9aa1946f16f13001e5cd3ed. The source declarations are first_fourier, second_fourier, and limiting_fourier_aux. The statements here use Mathlib's LSeriesSummable directly, remove the source project's local nterm wrapper, and rely on Mathlib's APIs together with the local vertical-line continuity theorem TauCeti.LSeries.continuous_LSeries_vertical.

References

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

theorem TauCeti.LSeries.tsum_term_mul_fourier_eq_integral {a : ℕ → ℂ} {psi : ℝ → ℂ} {x sigma : ℝ} (hpsi : MeasureTheory.Integrable psi MeasureTheory.volume) (hx : 0 < x) (hsigma : LSeriesSummable a ↑sigma) : ∑' (n : ℕ), LSeries.term a (↑sigma) n * FourierTransform.fourier psi (1 / (2 * Real.pi) * Real.log (↑n / x)) = ∫ (t : ℝ), LSeries a (↑sigma + ↑t * Complex.I) * psi t * ↑x ^ (↑t * Complex.I)

Testing an absolutely convergent Dirichlet series against an integrable function on the vertical line Re s = sigma can be done term by term. The Fourier transform is evaluated at the logarithmic scale (2π)⁻¹ log (n / x) dictated by the factor x ^ (it).

The simple-pole term

theorem TauCeti.LSeries.integral_exp_mul_fourier_eq {psi : ℝ → ℂ} {x sigma : ℝ} (hpsi : MeasureTheory.Integrable psi MeasureTheory.volume) (hx : 0 < x) (hsigma : 1 < sigma) : ∫ (u : ℝ) in Set.Ici (-Real.log x), ↑(Real.exp (-u * (sigma - 1))) * FourierTransform.fourier psi (u / (2 * Real.pi)) = ↑(x ^ (sigma - 1)) * ∫ (t : ℝ), 1 / (↑sigma + ↑t * Complex.I - 1) * psi t * ↑x ^ (↑t * Complex.I)

The one-sided Laplace transform ∫ u in Ici (-log x), exp (-u * (sigma - 1)) * 𝓕 psi (u / 2π) equals x ^ (sigma - 1) times the Fourier integral of the simple pole 1 / (s - 1) on the line Re s = sigma. This is the pole term subtracted in the Wiener--Ikehara boundary argument, and the factor x ^ (sigma - 1) is the normalization that makes it match the Dirichlet-series identity.

Subtracting the pole

theorem TauCeti.LSeries.tsum_term_mul_fourier_sub_pole_eq_integral {a : ℕ → ℂ} {psi : ℝ → ℂ} {x sigma : ℝ} {G : ℂ → ℂ} {A : ℂ} (hG : ∀ (t : ℝ), G (↑sigma + ↑t * Complex.I) = LSeries a (↑sigma + ↑t * Complex.I) - A / (↑sigma + ↑t * Complex.I - 1)) (hpsi : MeasureTheory.Integrable psi MeasureTheory.volume) (hx : 0 < x) (hsigma : 1 < sigma) (hsigmaSum : LSeriesSummable a ↑sigma) : ∑' (n : ℕ), LSeries.term a (↑sigma) n * FourierTransform.fourier psi (1 / (2 * Real.pi) * Real.log (↑n / x)) - A * ↑(x ^ (1 - sigma)) * ∫ (u : ℝ) in Set.Ici (-Real.log x), ↑(Real.exp (-u * (sigma - 1))) * FourierTransform.fourier psi (u / (2 * Real.pi)) = ∫ (t : ℝ), G (↑sigma + ↑t * Complex.I) * psi t * ↑x ^ (↑t * Complex.I)

Subtracting the simple-pole Fourier identity from the Dirichlet-series identity leaves exactly the integral of the pole-subtracted remainder G. Only the values of G on the vertical line Re s = sigma enter, so no continuity or limiting behaviour of G on the boundary line is assumed here. This is the form used before sending sigma to 1 in the Wiener--Ikehara argument.