Dependencies

One has

for all \(x \geq 1\).

The Fourier transform is a bijection on the Schwartz class. [Note: only surjectivity is actually used.]

For any \(a\) coprime to \(m\),

One has

If \(a\ (q)\) is a primitive residue class, then one has

The Chebyshev Psi function is defined as

where \(\Lambda (n)\) is the von Mangoldt function.

For \(x{\gt}1\) and \(\sigma {\lt}-3/2\), we have

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\).

If \(\psi :\mathbb {R}\to \mathbb {C}\) is \(C^2\) and obeys the bounds

for all \(t \in \mathbb {R}\), then

for all \(u \in \mathbb {R}\), where \(C\) is an absolute constant.

If \(\psi :\mathbb {R}\to \mathbb {C}\) is absolutely integrable, absolutely continuous, and \(\psi '\) is of bounded variation, then

for all \(u \in \mathbb {R}\).

For any non-principal character \(\chi \) of \(Gal(K/L)\),

We have

for \(\Re (s) {\gt} 1\), where \(\chi \) runs over homomorphisms from \(G\) to \(\mathbb {C}^\times \) and \(L\) is the Artin \(L\)-function.

For any non-principal character \(\chi \) of \(Gal(K/L)\), \(L(\chi ,s)\) does not vanish for \(\Re (s)=1\).

\(\zeta _L\) has a simple pole at \(s=1\).

Let \(\nu \) be a bumpfunction supported in \([1/2,2]\). Then for any \(\epsilon {\gt}0\), we define the delta spike \(\nu _\epsilon \) to be the function from \(\mathbb {R}_{{\gt}0}\) to \(\mathbb {C}\) defined by

For any \(\epsilon {\gt}0\), we have

For any \(s = \sigma + tI \in \mathbb {C}\), \(1/2 \le \sigma \le 2, 3 {\lt} |t|\), and any \(0 {\lt} A {\lt} 1\) sufficiently small, and \(1-A/\log |t| \le \sigma \), we have

Let \(x{\gt}0\). Then for \(0 {\lt} c {\lt} 1 /2\), we have that the function

is bounded above on the rectangle with corners at \(-1-c-i*c\) and \(-1+c+i*c\) (except at \(s=-1\)).

Let \(x{\gt}0\). Then for \(0 {\lt} c {\lt} 1 /2\), we have that the function

is bounded above on the rectangle with corners at \(-c-i*c\) and \(c+i*c\) (except at \(s=0\)).

Any primitive residue class contains an infinite number of primes.

If \(f\) is differentiable on a set \(s\) except at \(c\in s\), and \(f\) is bounded above on \(s\setminus \{ c\} \), then there exists a differentiable function \(g\) on \(s\) such that \(f\) and \(g\) agree on \(s\setminus \{ c\} \).

For any arithmetic function \(f\) and real number \(x\), one has

and

If \(\psi : \mathbb {R}\to \mathbb {C}\) is integrable and \(x {\gt} 0\), then for any \(\sigma {\gt}1\)

For \(x{\gt}1\) and \(\sigma {\gt}0\), we have

For \(x{\gt}0\), \(\sigma {\gt}0\), and \(x{\lt}1\), we have

If \(f\) is holomorphic on a rectangle \(z\) and \(w\), then the integral of \(f\) over the rectangle with corners \(z\) and \(w\) is \(0\).

For any \(N\ge 1\), the function \(\zeta _0(N,s)\) is holomorphic on \(\{ s\in \mathbb {C}\mid \Re (s){\gt}0 ∧ s \ne 1\} \).

The integral

is positive (and hence convergent - since a divergent integral is zero in Lean, by definition).

Let \(x{\gt}0\). Then the function \(f(s) = x^s/(s(s+1))\) is holomorphic on the half-plane \(\{ s\in \mathbb {C}:\Re (s){\gt}0\} \).

Let \(x{\gt}0\) and \(\sigma \in \mathbb {R}\). Then

is integrable.

The set \(\{ s\in \mathbb {C}\mid \Re (s){\gt}0 ∧ s \ne 1\} \) is path-connected.

Let \(x\in \mathbb {R}\) and \(s \ne 0, -1\). Then

We have \(\sum _{n \leq x} \lambda (n) = o(x)\).

If \(\psi : \mathbb {R}\to \mathbb {C}\) is \(C^2\) and compactly supported and \(x \geq 1\), then

With the hypotheses as above, we have

as \(x \to \infty \).

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 \(a:\mathbb {R}\to \mathbb {C}\) be a function, and let \(\sigma {\gt}0\) be a real number. Suppose that, for all \(\sigma , \sigma '{\gt}0\), we have \(a(\sigma ')=a(\sigma )\), and that \(\lim _{\sigma \to \infty }a(\sigma )=0\). Then \(a(\sigma )=0\).

Let \(a:\mathbb {R}\to \mathbb {C}\) be a function, and let \(\sigma {\lt}-3/2\) be a real number. Suppose that, for all \(\sigma , \sigma '{\gt}0\), we have \(a(\sigma ')=a(\sigma )\), and that \(\lim _{\sigma \to -\infty }a(\sigma )=0\). Then \(a(\sigma )=0\).

We have that, for \(\Re (s){\gt}1\),

There is an \(A{\gt}0\) so that for \(1-A/\log ^9 |t| \le \sigma {\lt} 1\) and \(3 {\lt} |t|\),

There is an \(A{\gt}0\) so that for \(1-A/\log ^9 |t| \le \sigma {\lt} 1\) and \(|t|\to \infty \),

(Same statement but using big-Oh and filters.)

We have

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 {R}\) or \(\mathbb {C}\), for \(x\neq 0\),

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\)).

Let \(f\) be a twice differentiable function from \(\mathbb {R}_{{\gt}0}\) to \(\mathbb {C}\), and let \(\sigma \) be sufficiently large. Then

The Mellin transform of \(1_{(0,1]}\) is

For any \(\epsilon {\gt}0\), the Mellin transform of \(\nu _\epsilon \) is

For any \(\epsilon {\gt}0\), we have

As \(\epsilon \to 0\), we have

The Mellin transform of \(\nu \) is

as \(|s|\to \infty \) with \(\sigma _1 \le \Re (s) \le 2\).

Fix \(\epsilon {\gt}0\). Then the Mellin transform of \(\widetilde{1_{\epsilon }}\) is

Given \(0{\lt}\sigma _1\le \sigma _2\), for any \(s\) such that \(\sigma _1\le \mathcal Re(s)\le \sigma _2\), we have

At \(s=1\), we have

Let \(f\) be a function from \(\mathbb {R}_{{\gt}0}\) to \(\mathbb {C}\). We define the Mellin transform of \(f\) to be the function \(\mathcal{M}(f)\) from \(\mathbb {C}\) to \(\mathbb {C}\) defined by

We have \(\sum _{n \leq x} \mu (n) = o(x)\).

We have \(\sum _{n \leq x} \mu (n)/n = o(1)\).

We have \(|\sum _{n \leq x} \frac{\mu (n)}{n}| \leq 1\).

Let \(f, g\) be once differentiable functions from \(\mathbb {R}_{{\gt}0}\) to \(\mathbb {C}\) so that \(fg'\) and \(f'g\) are both integrable, and \(f\cdot g (x)\to 0\) as \(x\to 0^+,\infty \). Then

Let \(0 {\lt} x {\lt} t\) and \(\sigma {\gt}0\). Then the inverse Mellin transform of the Perron function is equal to

Let \(0 {\lt} t {\lt} x\) and \(\sigma {\gt}0\). Then the inverse Mellin transform of the Perron function

is equal to

One has

as \(x \to \infty \).

There exists a function \(c(x)\) such that \(c(x) = o(1)\) as \(x \to \infty \) and

for all \(x\) large enough.

One has

as \(n \to \infty \).

We have \(p_{n+1} - p_n = o(p_n)\) as \(n \to \infty \).

If \(\psi :\mathbb {R}\to \mathbb {C}\) is absolutely integrable then

for all \(u \in \mathbb {R}\). where \(C\) is an absolute constant.

If \(\psi :\mathbb {R}\to \mathbb {C}\) is absolutely integrable and of bounded variation, and \(\psi '\) is bounded variation, then

for all non-zero \(u \in \mathbb {R}\).

If \(\psi :\mathbb {R}\to \mathbb {C}\) is absolutely integrable, absolutely continuous, and \(\psi '\) is of bounded variation, then

for all non-zero \(u \in \mathbb {R}\).

For every \(\epsilon {\gt}0\), there is a prime between \(x\) and \((1+\epsilon )x\) for all sufficiently large \(x\).

We have

A Rectangle’s border, given corners \(z\) and \(w\) is the union of the four sides.

A RectangleIntegral of a function \(f\) is one over a rectangle determined by \(z\) and \(w\) in \(\mathbb {C}\). We will sometimes denote it by \(\int _{z}^{w} f\). (There is also a primed version, which is \(1/(2\pi i)\) times the original.)

If \(f\) is holomorphic on a rectangle \(z\) and \(w\) except at a point \(p\), then the integral of \(f\) over the rectangle with corners \(z\) and \(w\) is the same as the integral of \(f\) over a small square centered at \(p\).

Let \(x{\gt}0\). Then for all sufficiently small \(c{\gt}0\), we have that

Let \(x{\gt}0\). Then for all sufficiently small \(c{\gt}0\), we have that

For \(x{\gt}1\) (of course \(x{\gt}0\) would suffice) and \(\sigma {\gt}0\), we have

For \(x{\gt}1\), we have

The rectangle (square) integral of \(f(s) = 1/s\) with corners \(-1-i\) and \(1+i\) is equal to \(2\pi i\).

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\).

For any natural \(N\ge 1\), we define

The previous corollary also holds for functions \(\psi \) that are assumed to be in the Schwartz class, as opposed to being \(C^2\) and compactly supported.

If \(\psi : \mathbb {R}\to \mathbb {C}\) is continuous and compactly supported and \(x {\gt} 0\), then for any \(\sigma {\gt}1\)

If \(I\) is a closed interval contained in an open interval \(J\), then there exists a smooth function \(\Psi : \mathbb {R}\to \mathbb {R}\) with \(1_I \leq \Psi \leq 1_J\).

Let \(\epsilon {\gt}0\). Then we define the smooth function \(\widetilde{1_{\epsilon }}\) from \(\mathbb {R}_{{\gt}0}\) to \(\mathbb {C}\) by

Fix a nonnegative, continuously differentiable function \(F\) on \(\mathbb {R}\) with support in \([1/2,2]\). Then for any \(\epsilon {\gt}0\), the function \(x \mapsto \int _{(0,\infty )} x^{1+it} \widetilde{1_{\epsilon }}(x) dx\) is continuous at any \(y{\gt}0\).

If \(\nu \) is nonnegative and has mass one, then \(\widetilde{1_{\epsilon }}(x)\le 1\), \(\forall x{\gt}0\).

If \(\nu \) is nonnegative, then \(\widetilde{1_{\epsilon }}(x)\) is nonnegative.

Fix \(0{\lt}\epsilon {\lt}1\). There is an absolute constant \(c{\gt}0\) so that: if \(x\geq (1+c\epsilon )\), then

Fix \(\epsilon {\gt}0\). There is an absolute constant \(c{\gt}0\) so that: If \(0 {\lt} x \leq (1-c\epsilon )\), then

Fix \(\epsilon {\gt}0\), and a bumpfunction 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

We have that

Fix a nonnegative, continuously differentiable function \(F\) on \(\mathbb {R}\) with support in \([1/2,2]\), and total mass one, \(\int _{(0,\infty )} F(x)/x dx = 1\). Then for any \(\epsilon {\gt}0\), the function

is integrable on \(\mathbb {R}\). ** Conditions are overkill; can remove some assumptions... **

Fix a nonnegative, continuously differentiable function \(F\) on \(\mathbb {R}\) with support in \([1/2,2]\), and total mass one, \(\int _{(0,\infty )} F(x)/x dx = 1\). Then for any \(\epsilon {\gt}0\), the function \(x \mapsto \sum _{n=1}^\infty \frac{\Lambda (n)}{n^{2+it}} \mathcal{M}(\widetilde{1_{\epsilon }})(2+it) x^{2+it}\) is equal to \(\sum _{n=1}^\infty \int _{(0,\infty )} \frac{\Lambda (n)}{n^{2+it}} \mathcal{M}(\widetilde{1_{\epsilon }})(2+it) x^{2+it}\). ** Conditions are overkill; can remove some assumptions...**

We have that

There exists a smooth (once differentiable would be enough), nonnegative “bumpfunction” \(\nu \), supported in \([1/2,2]\) with total mass one:

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

Let \(x{\gt}1\). Then

Let \(x{\gt}0\) and \(x{\lt}1\). Then

Let \(x{\gt}0\) and \(\sigma ',\sigma ''\in \mathbb {R}\). Then

goes to \(0\) as \(t\to -\infty \).

Let \(x{\gt}0\) and \(\sigma ',\sigma ''\in \mathbb {R}\). Then

goes to \(0\) as \(t\to \infty \).

Let \(f\) be a function from \(\mathbb {C}\) to \(\mathbb {C}\), and let \(\sigma \) be a real number. Then we define

Let \(x{\gt}0\) and \(\sigma {\gt}1\). Then

Let \(x{\gt}1\) and \(\sigma {\lt}-3/2\). Then

We have

If \(q ≥ 1\) and \(a\) is coprime to \(q\), we have

If \(q ≥ 1\) and \(a\) is coprime to \(q\), the Dirichlet series \(\sum _{n \leq x: n = a\ (q)} {\Lambda (n)}{n^s}\) converges for \(\mathrm{Re}(s) {\gt} 1\) to \(\frac{1}{\varphi (q)} \frac{1}{s-1} + G(s)\) where \(G\) has a continuous extension to \(\mathrm{Re}(s)=1\).

If \(q ≥ 1\) and \(a\) is coprime to \(q\), and \(\mathrm{Re} s {\gt} 1\), we have

We have

For any closed interval \(I \subset (0,+\infty )\), we have

If \(\Psi : (0,\infty ) \to \mathbb {C}\) is smooth and compactly supported away from the origin, then,

as \(x \to \infty \).

We have

For \(\Re (s){\gt}0\), \(s\ne 1\), and for any \(N\),

For any \(A{\gt}0\) sufficiently small, there is a constant \(C{\gt}0\) so that whenever \(1- A / \log t \le \sigma _1 {\lt} \sigma _2\le 2\) and \(3 {\lt} |t|\), we have that:

For any \(t\ne 0\) (so we don’t pass through the pole), and \(\sigma _1 {\lt} \sigma _2\),

For any \(N\ge 1\) and \(s = \sigma + tI \in \mathbb {C}\), \(\sigma =\in (0,2], 2 {\lt} |t|\),

For any \(0 {\lt} a {\lt} b\) and \(s \in \mathbb {C}\) with \(\sigma =\Re (s){\gt}0\),

For any \(N\ge 1\) and \(s = \sigma + tI \in \mathbb {C}\), \(\sigma {\gt} 0\),

For any \(N\ge 1\) and \(s = \sigma + tI \in \mathbb {C}\), \(\sigma =\in (0,2], 2 {\lt} |t|\),

Given \(n ≤ t\) and \(\sigma \) with \(1-A/\log t \le \sigma \), we have that

The rectangle integral over \([1-\delta ,2] \times _{ℂ} [-T,T]\) of the integrand in \(\psi _{\epsilon }\) is

For any \(s = \sigma + tI \in \mathbb {C}\), \(1/2 \le \sigma \le 2, 3 {\lt} |t|\), there is an \(A{\gt}0\) so that for \(1-A/\log t \le \sigma \), we have

For any \(A{\gt}0\) sufficiently small, there is a constant \(C{\gt}0\) so that whenever \(1- A / \log ^9 |t| \le \sigma {\lt} 1\) and \(3 {\lt} |t|\), we have that:

For all \(\sigma {\gt}1\),

For \(\sigma {\gt}1\) (and \(\sigma \le 2\)),

as \(|t|\to \infty \).

There exists a \(c{\gt}0\) such that for all \(1 {\lt} \sigma ≤ 2\),

As \(\sigma \to 1^+\),

Let \(0 {\lt} a {\lt} b\) be natural numbers and \(s\in \mathbb {C}\) with \(s \ne 1\) and \(s \ne 0\). Then

Let \(N\) be a natural number and \(s\in \mathbb {C}\), \(\Re (s){\gt}1\). Then

For any \(s = \sigma + tI \in \mathbb {C}\), \(1/2 \le \sigma \le 2, 3 {\lt} |t|\) and any \(0 {\lt} A {\lt} 1\) sufficiently small, and \(1-A/\log |t| \le \sigma \), we have