Approximating the test function in the smoothed Wiener--Ikehara asymptotic

TauCeti.LSeries.tendsto_tsum_term_mul_fourier_atTop_of_nonneg evaluates the limit of ∑ a n / n * 𝓕 psi (log (n / x) / 2π) for a smooth compactly supported test function psi. The Tauberian step of Wiener--Ikehara needs the same limit for weights W that are not of this form. A nonzero smooth compactly supported weight W is one: it is the Fourier transform of a Schwartz function, but never of a compactly supported one, since a nonzero function and its Fourier transform cannot both have compact support. This file passes the limit from 𝓕 psi to any weight W that such transforms approximate in the weighted sup norm sup_v (1 + v ^ 2) ‖W v - 𝓕 psi v‖.

The approximation step rests on a uniform bound. If the partial sums of ‖a‖ satisfy the Chebyshev bound ∑_{1 ≤ n ≤ N} ‖a n‖ ≤ C N, then ∑ ‖a n‖ / n * (1 + (log (n / x) / 2π) ^ 2)⁻¹ ≤ C (1 + 2π²) for every scale x > 0. The weight t ↦ (t (1 + (log (t / x) / 2π) ^ 2))⁻¹ is antitone on t > 0, so Abel's inequality TauCeti.sum_range_mul_le_sum_range_mul bounds the weighted sum by C times the sum of the weight, and the integral test bounds the latter by 1 + ∫ = 1 + 2π (arctan - arctan) ≤ 1 + 2π². Consequently a weight W with ‖W v‖ ≤ M (1 + v ^ 2)⁻¹ gives a series of size at most M C (1 + 2π²), uniformly in x, and a small error in the weighted sup norm costs little in the limit. For nonnegative coefficients with Wiener--Ikehara boundary data the Chebyshev bound is TauCeti.LSeries.isBigO_sum_Icc_norm_id_of_boundary.

Main results

• TauCeti.LSeries.tsum_norm_term_mul_inv_one_add_sq_le: the uniform bound on the logarithmically weighted series, from a Chebyshev bound.
• TauCeti.LSeries.LSeriesSummable_mul_comp_log_div and TauCeti.LSeries.norm_tsum_term_mul_comp_log_div_le: summability and the uniform bound for a weight W with ‖W v‖ ≤ M (1 + v ^ 2)⁻¹.
• TauCeti.LSeries.tendsto_tsum_term_mul_atTop_of_approx_fourier: the smoothed Wiener--Ikehara asymptotic for a weight W approximable by Fourier transforms of smooth compactly supported functions psi whose values psi 0 approximate L; the limit is 2π A L.

Provenance

The uniform bound and the truncation argument follow bound_sum_log, bound_I1 and limiting_cor_W21 in PrimeNumberTheoremAnd/Wiener.lean of the Apache-2.0 AxiomMath/PrimeNumberTheoremAnd repository, revision 2667e414c38e5a5dc9aa1946f16f13001e5cd3ed, the same source as the sibling files in this directory. Here the summation by parts is the general TauCeti.sum_range_mul_le_sum_range_mul, the integral of the weight is bounded on finite intervals by the fundamental theorem of calculus rather than evaluated on (0, ∞), and the approximation hypothesis is stated for an arbitrary weight W instead of a fixed truncation of a W^{2,1} function. For a Schwartz function g (limiting_cor_schwartz there) the approximants are the truncations χ (R⁻¹ • ·) • g, which converge to g in the Schwartz topology (SchwartzMap.tendsto_smulLeftCLM_comp_inv_smul_atTop); the weighted sup norm of a Fourier transform is bounded by two Schwartz seminorms, so it is the continuity of the Fourier transform on 𝓢(ℝ, ℂ) that makes the truncation error small.

References

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

The logarithmic weight

The uniform bound

theorem TauCeti.LSeries.summable_norm_term_mul_inv_one_add_sq {a : ℕ → ℂ} {C x : ℝ} (hC : ∀ (N : ℕ), ∑ n ∈ Finset.Icc 1 N, ‖a n‖ ≤ C * ↑N) (hx : 0 < x) : Summable fun (n : ℕ) => ‖LSeries.term a 1 n‖ * (1 + (1 / (2 * Real.pi) * Real.log (↑n / x)) ^ 2)⁻¹

Under a Chebyshev bound the logarithmically weighted norm series converges at every scale x > 0.

theorem TauCeti.LSeries.tsum_norm_term_mul_inv_one_add_sq_le {a : ℕ → ℂ} {C x : ℝ} (hC : ∀ (N : ℕ), ∑ n ∈ Finset.Icc 1 N, ‖a n‖ ≤ C * ↑N) (hx : 0 < x) : ∑' (n : ℕ), ‖LSeries.term a 1 n‖ * (1 + (1 / (2 * Real.pi) * Real.log (↑n / x)) ^ 2)⁻¹ ≤ C * (1 + 2 * Real.pi ^ 2)

The uniform logarithmic bound. If ∑_{1 ≤ n ≤ N} ‖a n‖ ≤ C N for every N, then ∑ ‖a n‖ / n * (1 + (log (n / x) / 2π) ^ 2)⁻¹ ≤ C (1 + 2π²) for every scale x > 0.

Weights with quadratic decay

theorem TauCeti.LSeries.LSeriesSummable_mul_comp_log_div {a : ℕ → ℂ} {C x : ℝ} {W : ℝ → ℂ} {M : ℝ} (hC : ∀ (N : ℕ), ∑ n ∈ Finset.Icc 1 N, ‖a n‖ ≤ C * ↑N) (hW : ∀ (v : ℝ), ‖W v‖ ≤ M * (1 + v ^ 2)⁻¹) (hx : 0 < x) : LSeriesSummable (fun (n : ℕ) => a n * W (1 / (2 * Real.pi) * Real.log (↑n / x))) 1

Under a Chebyshev bound, a weight W with ‖W v‖ ≤ M (1 + v ^ 2)⁻¹ gives a Dirichlet series ∑ a n W (log (n / x) / 2π) n⁻ˢ that converges at s = 1, at every scale x > 0.

theorem TauCeti.LSeries.norm_tsum_term_mul_comp_log_div_le {a : ℕ → ℂ} {C x : ℝ} {W : ℝ → ℂ} {M : ℝ} (hC : ∀ (N : ℕ), ∑ n ∈ Finset.Icc 1 N, ‖a n‖ ≤ C * ↑N) (hW : ∀ (v : ℝ), ‖W v‖ ≤ M * (1 + v ^ 2)⁻¹) (hx : 0 < x) : ‖∑' (n : ℕ), LSeries.term a 1 n * W (1 / (2 * Real.pi) * Real.log (↑n / x))‖ ≤ M * (C * (1 + 2 * Real.pi ^ 2))

The uniform bound for a decaying weight. Under a Chebyshev bound ∑_{1 ≤ n ≤ N} ‖a n‖ ≤ C N, a weight W with ‖W v‖ ≤ M (1 + v ^ 2)⁻¹ gives ‖∑ a n / n * W (log (n / x) / 2π)‖ ≤ M C (1 + 2π²) for every scale x > 0.

Passing the smoothed asymptotic to approximable weights

theorem TauCeti.LSeries.tendsto_tsum_term_mul_atTop_of_approx_fourier {a : ℕ → ℂ} {W : ℝ → ℂ} {G : ℂ → ℂ} {A L : ℂ} (ha : 0 ≤ 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) (happrox : ∀ ε > 0, ∃ (psi : ℝ → ℂ), ContDiff ℝ (↑⊤) psi ∧ HasCompactSupport psi ∧ (∀ (v : ℝ), ‖W v - FourierTransform.fourier psi v‖ ≤ ε * (1 + v ^ 2)⁻¹) ∧ ‖L - psi 0‖ ≤ ε) : Filter.Tendsto (fun (x : ℝ) => ∑' (n : ℕ), LSeries.term a 1 n * W (1 / (2 * Real.pi) * Real.log (↑n / x))) Filter.atTop (nhds (2 * ↑Real.pi * A * L))

The smoothed Wiener--Ikehara asymptotic for an approximable weight. Let a be nonnegative, with Dirichlet series summable on Re s > 1 and a boundary remainder G = LSeries a - A / (s - 1) continuous on Re s ≥ 1. Suppose that for every ε > 0 some smooth compactly supported psi satisfies ‖W v - 𝓕 psi v‖ ≤ ε (1 + v ^ 2)⁻¹ for all v and ‖L - psi 0‖ ≤ ε. Then ∑ a n / n * W (log (n / x) / 2π) → 2π A L as x → ∞.

For W = 𝓕 psi itself this is TauCeti.LSeries.tendsto_tsum_term_mul_fourier_atTop_of_nonneg with L = psi 0; the point is that W need not be the Fourier transform of a compactly supported function.

Schwartz test functions

theorem TauCeti.LSeries.tendsto_tsum_term_mul_fourier_schwartz_atTop {a : ℕ → ℂ} {G : ℂ → ℂ} {A : ℂ} (ha : 0 ≤ 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) (g : SchwartzMap ℝ ℂ) : Filter.Tendsto (fun (x : ℝ) => ∑' (n : ℕ), LSeries.term a 1 n * FourierTransform.fourier (⇑g) (1 / (2 * Real.pi) * Real.log (↑n / x))) Filter.atTop (nhds (2 * ↑Real.pi * A * g 0))

The smoothed Wiener--Ikehara asymptotic for a Schwartz test function. Let a be nonnegative, with Dirichlet series summable on Re s > 1 and a boundary remainder G = LSeries a - A / (s - 1) continuous on Re s ≥ 1. For every Schwartz function g on ℝ, ∑ a n / n * 𝓕 g (log (n / x) / 2π) → 2π A g 0 as x → ∞.

This extends TauCeti.LSeries.tendsto_tsum_term_mul_fourier_atTop_of_nonneg from smooth compactly supported test functions to Schwartz functions. In particular it applies to every smooth compactly supported weight W, since W = 𝓕 (𝓕⁻ W) with 𝓕⁻ W a Schwartz function.