- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Orange (dashed) border
- the statement of this result is ready to be formalized; all prerequisites are done
- Red border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Orange (gradient) background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
If \(\psi : \mathbb {R}\to \mathbb {C}\) is \(C^2\) and compactly supported with \(f\) and \(\hat\psi \) non-negative, then there exists a constant \(B\) such that
for all \(x \geq 1\).
Let \(\psi \) be a bumpfunction supported in \([1/2,2]\). Then for any \(\epsilon {\gt}0\), we define the delta spike \(\psi _\epsilon \) to be the function from \(\mathbb {R}_{{\gt}0}\) to \(\mathbb {C}\) defined by
If \(\psi : \mathbb {R}\to \mathbb {C}\) is continuous and integrable and \(x {\gt} 0\), then for any \(\sigma {\gt}1\)
If \(\psi : \mathbb {R}\to \mathbb {C}\) is \(C^2\) and compactly supported and \(x \geq 1\), then
If \(\psi : \mathbb {R}\to \mathbb {C}\) is \(C^2\) and compactly supported with \(f\) and \(\hat\psi \) non-negative, and \(x \geq 1\), then
Let \(f\) and \(g\) be functions from \(\mathbb {R}_{{\gt}0}\) to \(\mathbb {C}\). Then we define the Mellin convolution of \(f\) and \(g\) to be the function \(f\ast g\) from \(\mathbb {R}_{{\gt}0}\) to \(\mathbb {C}\) defined by
Let \(f\) and \(g\) be functions from \(\mathbb {R}_{{\gt}0}\) to \(\mathbb {C}\) such that
is absolutely integrable on \([0,\infty )^2\). Then
Let \(F\) be a function from \(\mathbb {C}\) to \(\mathbb {C}\). We define the Mellin inverse transform of \(F\) to be the function \(\mathcal{M}^{-1}(F)\) from \(\mathbb {R}_{{\gt}0}\) to \(\mathbb {C}\) defined by
where \(\sigma \) is sufficiently large (say \(\sigma {\gt}2\)).
For any arithmetic function \(f\) and real number \(x\), one has
and
Suppose that \(f\) is a holomorphic function on a rectangle, except for a simple pole at \(p\). By the latter, we mean that there is a function \(g\) holomorphic on the rectangle such that, \(f = g + A/(s-p)\) for some \(A\in \mathbb {C}\). Then the integral of \(f\) over the rectangle is \(A\).
If \(\psi : \mathbb {R}\to \mathbb {C}\) is continuous and compactly supported and \(x {\gt} 0\), then for any \(\sigma {\gt}1\)
Fix \(\epsilon {\gt}0\), and a bumpfunction \(\psi \) supported in \([1/2,2]\). Then we define the smoothed Chebyshev function \(\psi _{\epsilon }\) from \(\mathbb {R}_{{\gt}0}\) to \(\mathbb {C}\) by
We have that
Let \(a {\lt} b\), and let \(\phi \) be continuously differentiable on \([a, b]\). Then
Let \(k \le a {\lt} b\le k+1\), with \(k\) an integer, and let \(\phi \) be continuously differentiable on \([a, b]\). Then
The rectangle integral over \([1-\delta ,2] \times _{ℂ} [-T,T]\) of the integrand in \(\psi _{\epsilon }\) is
Let \(0 {\lt} a {\lt} b\) be natural numbers and \(s\in \mathbb {C}\) with \(s \ne 1\) and \(s \ne 0\). Then