Mellin inversion: the smoothed partial sum $\sum a(n)\widetilde{1_\varepsilon}(n/X)$ as a vertical contour integral of $\sum a(n)n^{-s}$

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. Let $a(n)$ be complex coefficients with $|a(n)|\le\Lambda(n)$ (the von Mangoldt function), let $X>3$ and $0<\varepsilon<1$, and put $\sigma_0=1+1/\log X$. Then

This is the smoothed Perron formula: Mellin inversion applied termwise to the absolutely convergent Dirichlet series on the line $\sigma_0$, where $\sum|a(n)|n^{-\sigma_0}\le\sum\Lambda(n)n^{-\sigma_0}<\infty$. It is the starting point of the contour method for partial sums of $a(n)$; the platform theorem SmoothedChebyshevDirichlet is the special case $a=\Lambda$, and the present statement is used with $a(n)=\Lambda(n)\chi(n)$ in the character prime number theorem.

Formalization Note. VerticalIntegral' f σ is $\frac1{2\pi i}\int_{\mathbb R}f(\sigma+it)\,i\,dt$; LSeries a s is $\sum_{n\ge1}a(n)n^{-s}$; the right-hand side is a tsum over $n\in\mathbb N$ (the $n=0$ term vanishes since $a(0)=0$ is forced by $|a(0)|\le\Lambda(0)=0$).