The limiting Fourier identity for Wiener--Ikehara

TauCeti.LSeries.tsum_term_mul_fourier_sub_pole_eq_integral tests a Dirichlet series against an integrable function on a vertical line Re s = sigma strictly inside the half-plane of convergence. This file lets sigma decrease to 1 and records the resulting identity on the boundary line itself.

Each of the three terms of that identity has its own limit argument, and each is stated separately so that a later step can reuse it: the Dirichlet series converges by the uniform convergence of a summable Dirichlet series on a closed half-plane, while the two integrals converge by dominated convergence, the pole term because the exponential damping exp (-u (sigma - 1)) is bounded on the half-line of integration, and the vertical integral because a test function with compact support confines the integrand to a compact box on which G is continuous.

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 and TauCeti.LSeries.tendsto_integral_vertical are two of the three one-sided limits; the third, for the pole term, is the general TauCeti.tendsto_integral_exp_mul.
• TauCeti.LSeries.tsum_term_mul_fourier_sub_pole_eq_integral_boundary is the identity they combine into, and TauCeti.LSeries.tsum_term_mul_fourier_sub_pole_eq_integral_boundary_of_contDiff is its form for a smooth test function, where the half-line integrability hypothesis is automatic by TauCeti.integrable_fourier_of_contDiff_of_hasCompactSupport.

Provenance

The decomposition into three separate one-sided limits, and the shape of the identity they combine into, follow limiting_fourier_lim1, limiting_fourier_lim2, limiting_fourier_lim3 and limiting_fourier in PrimeNumberTheoremAnd/Wiener.lean of the Apache-2.0 AxiomMath/PrimeNumberTheoremAnd repository, revision 2667e414c38e5a5dc9aa1946f16f13001e5cd3ed, the same source as the sibling file TauCeti.NumberTheory.LSeries.WienerIkehara.Fourier. The proofs here are written against Mathlib's uniform- and dominated-convergence lemmas, and the hypotheses differ: the Chebyshev-type bound of the source is replaced by the summability of the Fourier-weighted series at s = 1, which is what the limit actually consumes.

References

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

The Dirichlet series

theorem TauCeti.LSeries.tendsto_tsum_term_mul_fourier {a : ℕ → ℂ} {psi : ℝ → ℂ} {x : ℝ} (hFsum : LSeriesSummable (fun (n : ℕ) => a n * FourierTransform.fourier psi (1 / (2 * Real.pi) * Real.log (↑n / x))) 1) : Filter.Tendsto (fun (sigma : ℝ) => ∑' (n : ℕ), LSeries.term a (↑sigma) n * FourierTransform.fourier psi (1 / (2 * Real.pi) * Real.log (↑n / x))) (nhdsWithin 1 (Set.Ioi 1)) (nhds (∑' (n : ℕ), LSeries.term a 1 n * FourierTransform.fourier psi (1 / (2 * Real.pi) * Real.log (↑n / x))))

As sigma decreases to 1, the Fourier-weighted Dirichlet series converges to its value on the boundary line, provided the weighted series is summable there.

The integral along the vertical line

theorem TauCeti.LSeries.tendsto_integral_vertical {psi : ℝ → ℂ} {G : ℂ → ℂ} {x : ℝ} (hx : 0 < x) (hG : ContinuousOn G {z : ℂ | 1 ≤ z.re}) (hpsi : MeasureTheory.Integrable psi MeasureTheory.volume) (hsupp : HasCompactSupport psi) : Filter.Tendsto (fun (sigma : ℝ) => ∫ (t : ℝ), G (↑sigma + ↑t * Complex.I) * psi t * ↑x ^ (↑t * Complex.I)) (nhdsWithin 1 (Set.Ioi 1)) (nhds (∫ (t : ℝ), G (1 + ↑t * Complex.I) * psi t * ↑x ^ (↑t * Complex.I)))

As sigma decreases to 1, the integral of G along the vertical line Re s = sigma against a compactly supported test function converges to the same integral along the boundary line, because the integrand is confined to a compact box on which G is continuous.

The identity on the boundary line

theorem TauCeti.LSeries.tsum_term_mul_fourier_sub_pole_eq_integral_boundary {a : ℕ → ℂ} {psi : ℝ → ℂ} {G : ℂ → ℂ} {A : ℂ} {x : ℝ} (hx : 0 < x) (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 : MeasureTheory.IntegrableOn (fun (u : ℝ) => FourierTransform.fourier psi (u / (2 * Real.pi))) (Set.Ici (-Real.log x)) MeasureTheory.volume) (hFsum : LSeriesSummable (fun (n : ℕ) => a n * FourierTransform.fourier psi (1 / (2 * Real.pi) * Real.log (↑n / x))) 1) : ∑' (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)) = ∫ (t : ℝ), G (1 + ↑t * Complex.I) * psi t * ↑x ^ (↑t * Complex.I)

The Fourier identity of tsum_term_mul_fourier_sub_pole_eq_integral on the boundary line Re s = 1. The Dirichlet series is tested against an integrable, compactly supported psi, and the pole term has lost its exponential damping.

The principal analytic inputs for the passage to the limit are that the Fourier-weighted series is summable at s = 1, the Fourier transform of psi is integrable on the half-line, and the pole-subtracted remainder G extends continuously to Re s ≥ 1. The additional hypotheses make x positive, supply the interior identity through the formula for G and summability of the original series, and give the integrability and compact support of the test function.

theorem TauCeti.LSeries.tsum_term_mul_fourier_sub_pole_eq_integral_boundary_of_contDiff {a : ℕ → ℂ} {psi : ℝ → ℂ} {G : ℂ → ℂ} {A : ℂ} {x : ℝ} (hx : 0 < x) (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 : LSeriesSummable (fun (n : ℕ) => a n * FourierTransform.fourier psi (1 / (2 * Real.pi) * Real.log (↑n / x))) 1) : ∑' (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)) = ∫ (t : ℝ), G (1 + ↑t * Complex.I) * psi t * ↑x ^ (↑t * Complex.I)

The boundary Fourier identity for a smooth, compactly supported test function. Its regularity supplies both its own integrability and the integrability of its Fourier transform, discharging both explicit integrability hypotheses from tsum_term_mul_fourier_sub_pole_eq_integral_boundary; summability of the Fourier-weighted series is still required.