Tails $|t|>T$ of the smoothed Perron integral on $\sigma_0=1+1/\log X$ are $O(X\log X/(\varepsilon T))$

Throughout, $\nu$ is a fixed smoothing kernel: a $C^1$ function on $\mathbb R$ supported in $[1/2,2]$, nonnegative on $(0,\infty)$, with $\int_0^\infty\nu(x)\,dx/x=1$; $\widetilde{1_\varepsilon}=$ Smooth1 ν ε is the smoothed indicator of $(0,1]$ obtained by Mellin convolution with the delta-spike $\nu(x^{1/\varepsilon})/\varepsilon$ (it equals $1$ on $(0,1-\varepsilon\log2]$, $0$ on $[1+2\varepsilon\log 2,\infty)$, and lies in $[0,1]$), and $\mathcal M\widetilde{1_\varepsilon}(s)=\int_0^\infty\widetilde{1_\varepsilon}(x)x^{s-1}dx$ is its Mellin transform (Mathlib's mellin).

Statement. There is a constant $C>0$ (depending only on $\nu$) such that for all coefficients $a(n)$ with $|a(n)|\le\Lambda(n)$, all $X>3$, $0<\varepsilon<1$ and $T>3$, with $\sigma_0=1+1/\log X$ and $F(s)=\bigl(\sum_{n\ge1}a(n)n^{-s}\bigr)\mathcal M\widetilde{1_\varepsilon}(s)X^{s}$,

On the line $\sigma_0$ the Dirichlet series is bounded by $\sum\Lambda(n)n^{-\sigma_0}=-\zeta'/\zeta(\sigma_0)\ll\log X$, $|X^{s}|=eX$, and $|\mathcal M\widetilde{1_\varepsilon}(s)|\ll1/(\varepsilon t^2)$, so the two tails $|t|\ge T$ contribute $\ll X\log X/(\varepsilon T)$. This is the truncation step of the contour method; with $T=\exp(\sqrt{\log X})$ it is negligible.

Formalization Note. VerticalIntegral' f σ is $\frac1{2\pi i}\int_{\mathbb R}f(\sigma+it)\,i\,dt$, and the truncated integral is written as $\frac1{2\pi i}\cdot i\int_{-T}^{T}F(\sigma_0+it)\,dt$; LSeries a s is $\sum_{n\ge1}a(n)n^{-s}$.