Riemann--Lebesgue along a vertical line

Testing a function on the vertical line Re s = c against a Dirichlet series produces the oscillating factor x ^ (i t), which is the Fourier character of frequency -(2π)⁻¹ log x in the variable t. Letting x → ∞ therefore pushes the frequency out of every compact set, and the Riemann--Lebesgue lemma makes the integral vanish.

Main declarations

• TauCeti.tendsto_integral_mul_cpow_mul_I_atTop: the integral ∫ t, f t * x ^ (t * I) tends to 0 as x → ∞, for an arbitrary f : ℝ → ℂ.

theorem TauCeti.tendsto_integral_mul_cpow_mul_I_atTop (f : ℝ → ℂ) : Filter.Tendsto (fun (x : ℝ) => ∫ (t : ℝ), f t * ↑x ^ (↑t * Complex.I)) Filter.atTop (nhds 0)

Riemann--Lebesgue on a vertical line: the integral of f against the oscillating factor x ^ (i t) tends to 0 as x → ∞.

No hypothesis is needed on f. A limit along atTop only sees x > 0, and there the factor x ^ (i t) has modulus 1, so the integrand is integrable exactly when f is; when f is not integrable both the left-hand side and the limit are 0. (For x ≤ 0 the equivalence fails — at x = 0 the integrand vanishes almost everywhere, and for x < 0 the branch of the complex power contributes a factor of modulus exp (-π t) — but those scales are irrelevant here.)