- 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
Let \(0 {\lt} r {\lt} R{\lt}1\), and \(f:\overline{\mathbb {D}_1}\to \mathbb {C}\) be analytic on neighborhoods of points in \(\overline{\mathbb {D}_1}\) with \(f(0)\neq 0\). We define a function \(B_f:\overline{\mathbb {D}_R}\to \mathbb {C}\) as follows.
Let \(0 {\lt} r {\lt} R{\lt}1\), and \(f:\overline{\mathbb {D}_1}\to \mathbb {C}\) be analytic on neighborhoods of points in \(\overline{\mathbb {D}_1}\) with \(f(0)\neq 0\). Then
Let \(0 {\lt} r {\lt} R{\lt}1\), and \(f:\overline{\mathbb {D}_1}\to \mathbb {C}\) be analytic on neighborhoods of points in \(\overline{\mathbb {D}_1}\) with \(f(0)\neq 0\). We define a function \(C_f:\overline{\mathbb {D}_R}\to \mathbb {C}\) as follows. This function is constructed by dividing \(f(z)\) by a polynomial whose roots are the zeros of \(f\) inside \(\overline{\mathbb {D}_r}\).
where \(h_z(z)\) comes from Lemma 101.
For any \(a\) coprime to \(m\),
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 {\gt} 0\).
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\).
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
Let \(R,\, M{\gt}0\) and \(0 {\lt} r {\lt} r' {\lt} R\). Let \(f\) be analytic on \(|z|\leq R\) such that \(f(0)=0\) and suppose \(\mathfrak {R}f(z)\leq M\) for all \(|z|\leq R\). Then we have that
for all \(|z|\leq r\).
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 \(B{\gt}1\) and \(0 {\lt} r' {\lt} r {\lt} R' {\lt} R{\lt}1\). If \(f:\mathbb {C}\to \mathbb {C}\) is a function analytic on neighborhoods of points in \(\overline{\mathbb {D}_1}\) with \(f(0)=1\) and \(|f(z)|\leq B\) for all \(|z|\leq R\), then for all \(z\in \overline{\mathbb {D}_{R'}}\setminus \mathcal{K}_f(R')\) we have
Let \(B{\gt}1\) and \(0 {\lt} R{\lt}1\). If \(f:\mathbb {C}\to \mathbb {C}\) is a function analytic on neighborhoods of points in \(\overline{\mathbb {D}_1}\) with \(f(0)=1\), define \(L_f(z)=J_{B_f}(z)\) where \(J\) is from Lemma 100 and \(B_f\) is from Definition 23.
Let \(B{\gt}1\) and \(0 {\lt} r' {\lt} r {\lt} R{\lt}1\). If \(f:\mathbb {C}\to \mathbb {C}\) is a function analytic on neighborhoods of points in \(\overline{\mathbb {D}_1}\) with \(f(0)=1\) and \(|f(z)|\leq B\) for all \(|z|\leq R\), then for all \(|z|\leq r'\)
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 \(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\).
Let \(0 {\lt} r {\lt} R{\lt}1\). Let \(B:\overline{\mathbb {D}_R}\to \mathbb {C}\) be analytic on neighborhoods of points in \(\overline{\mathbb {D}_R}\) with \(B(z)\neq 0\) for all \(z\in \overline{\mathbb {D}_R}\). Then there exists \(J_B:\overline{\mathbb {D}_r}\to \mathbb {C}\) that is analytic on neighborhoods of points in \(\overline{\mathbb {D}_r}\) such that
\(J_B(0)=0\)
\(J_B'(z)=B'(z)/B(z)\)
\(\log |B(z)|-\log |B(0)|=\mathfrak {R}J_B(z)\)
for all \(z\in \overline{\mathbb {D}_r}\).
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, 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
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}\).
If \(f\) has a simple pole at \(p\) with residue \(A\), and \(g\) is holomorphic near \(p\), then the residue of \(f \cdot g\) at \(p\) is \(A \cdot g(p)\). That is, we assume that
near \(p\), and that \(g\) is holomorphic near \(p\). Then
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 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\).
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
where we’ll take \(\sigma = 1 + 1 / \log X\).
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\), and \(\sigma \in (1, 2]\), the function
is integrable on \(\mathbb {R}\).
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\) and \(\sigma \in (1,2]\), the function \(x \mapsto \sum _{n=1}^\infty \frac{\Lambda (n)}{n^{\sigma +it}} \mathcal{M}(\widetilde{1_{\epsilon }})(\sigma +it) x^{\sigma +it}\) is equal to \(\sum _{n=1}^\infty \int _{(0,\infty )} \frac{\Lambda (n)}{n^{\sigma +it}} \mathcal{M}(\widetilde{1_{\epsilon }})(\sigma +it) x^{\sigma +it}\).
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
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\).
Let \(f:\overline{\mathbb {D}_1}\to \mathbb {C}\) be analytic on neighborhoods of points in \(\overline{\mathbb {D}_1}\) with \(f(0)\neq 0\). For all \(\rho \in \mathcal{K}_f(1)\) there exists \(h_\rho (z)\) that is analytic at \(\rho \), \(h_\rho (\rho )\neq 0\), and \(f(z)=(z-\rho )^{m_f(\rho )}\, h_\rho (z)\).
Let \(B{\gt}1\) and \(0{\lt} r {\lt} R{\lt}1\). If \(f:\mathbb {C}\to \mathbb {C}\) is a function analytic on neighborhoods of points in \(\overline{\mathbb {D}_1}\) with \(f(0)=1\) and \(|f(z)|\leq B\) for \(|z|\leq R\), then
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 all \(\epsilon {\gt} 0\) sufficiently close to \(0\), the rectangle integral over \([1-\delta ,2] \times _{ℂ} [-T,T]\) of the integrand in \(\psi _{\epsilon }\) is
where the implicit constant is independent of \(X\).
Let \(0 {\lt} a {\lt} b\) be natural numbers and \(s\in \mathbb {C}\) with \(s \ne 1\) and \(s \ne 0\). Then