Vanishing exponential damping of a half-line integral

Damping an integrand on the half-line u ≥ -log x by exp (-u (sigma - 1)) and normalizing by x ^ (1 - sigma), the reciprocal of the damping at the left endpoint, leaves the integral of an integrable function unchanged in the limit sigma → 1⁺: the damping factor is bounded on the half-line uniformly in sigma ∈ (1, 2], so dominated convergence applies.

This is the Abelian step of a Tauberian argument, where a Dirichlet series is tested on a vertical line Re s = sigma inside its half-plane of convergence and the line is pushed to the boundary; TauCeti.LSeries.tsum_term_mul_fourier_sub_pole_eq_integral_boundary uses it for the simple-pole term of the Wiener--Ikehara identity.

Main results

• TauCeti.tendsto_integral_exp_mul: the normalized damped integral converges to the undamped one as sigma decreases to 1.

theorem TauCeti.tendsto_integral_exp_mul {f : ℝ → ℂ} {x : ℝ} (hx : 0 < x) (hf : MeasureTheory.IntegrableOn f (Set.Ici (-Real.log x)) MeasureTheory.volume) : Filter.Tendsto (fun (sigma : ℝ) => ↑(x ^ (1 - sigma)) * ∫ (u : ℝ) in Set.Ici (-Real.log x), ↑(Real.exp (-u * (sigma - 1))) * f u) (nhdsWithin 1 (Set.Ioi 1)) (nhds (∫ (u : ℝ) in Set.Ici (-Real.log x), f u))

As sigma decreases to 1, the normalized one-sided Laplace transform of a function integrable on the half-line u ≥ -log x converges to its undamped integral.