- 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
A positive integer \(N\) is called highly abundant (HA) if
for all positive integers \(m {\lt} N\), where \(\sigmafunc (n)\) denotes the sum of the positive divisors of \(n\).
For each integer \(n \ge 1\), define
We call \((L_n)_{n \ge 1}\) the least common multiple sequence.
We say that \(L_n\) is highly abundant if \(L_n\) is a highly abundant integer in the sense above, i.e.
There exist integers \(m \ge 0\) and \(r\) satisfying \(0 {\lt} r {\lt} 4 p_1 p_2 p_3\) and
For \(n \ge X_0^2\), define \(\varepsilon := 1/n\). 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 \(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 105.
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
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 \(f : \mathbb {C} \to \mathbb {C}\) be a complex differentiable function at \(p \in \mathbb {C}\) with derivative \(a\). Then the function \(g(z) = \overline{f(\overline{z})}\) is complex differentiable at \(\overline{p}\) with derivative \(\overline{a}\).
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 Theorem 34 and \(B_f\) is from Definition 25.
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'\)
Let \(n \ge X_0^2\). Set \(x := \sqrt{n}\). Then, by repeated application of Theorem 50, there exist primes \(p_1,p_2,p_3\) with
and \(p_1 {\lt} p_2 {\lt} p_3\). Moreover, \(\sqrt{n} {\lt} p_1\) (for \(n\) sufficiently large).
Let \(n \ge X_0^2\). Then there exist primes \(q_1 {\lt} q_2 {\lt} q_3\) with
for \(i = 1,2,3\), and \(q_1 {\lt} q_2 {\lt} q_3 {\lt} n\).
If
then
Suppose
Then \(\sigmafunc (M) \ge \sigmafunc (L_n)\).
Let \(k\) be the largest integer such that \(2^k \le n\). Then the exponent of \(2\) in \(L'\) is at least \(k\), and the exponent of \(2\) in \(M\) is at least \(k+2\). Consequently,
Fix \(i \in \{ 1,2,3\} \). Suppose that in passing from \(L'\) to \(M\) we increase the exponent of \(p_i\) by exactly \(1\). Then the normalised divisor sum is multiplied by a factor
For all \(n \ge X_0^2 = 89693^2\) we have
For \(0 \le \varepsilon \le 1/89693^2\), we have
There exists a positive integer \(L'\) such that
and each prime \(q_i\) divides \(L_n\) exactly once and does not divide \(L'\).
With notation as above, we have:
\(0 {\lt} r {\lt} 4 p_1 p_2 p_3\).
\(M {\lt} L_n\).
- \[ 1 {\lt} \frac{L_n}{M} = \Bigl(1 - \frac{r}{q_1 q_2 q_3}\Bigr)^{-1} {\lt} \Bigl(1 - \frac{4 p_1 p_2 p_3}{q_1 q_2 q_3}\Bigr)^{-1}. \]
The extra factor \(m\) in the definition of \(M\) can only increase the normalised divisor sum:
With \(p_i\) as in Lemma 139, we have for large \(n\)
For \(0 \le \varepsilon \le 1/89693^2\), we have
and
With notation as above,
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 \(t\in \mathbb {R}\) with \(|t|\geq 2\) and \(0 {\lt} r' {\lt} r {\lt} R' {\lt} R{\lt}1\). If \(f(z)=\zeta (z+3/2+it)\), then for all \(z\in \overline{\mathbb {D}_R'}\setminus \mathcal{K}_f(R')\) we have that
There exists a constant \(F\in (0,1/2)\) such that for all \(t\in \mathbb {R}\) with \(|t|\geq 3\) one has
where the implied constant is uniform in \(\sigma \).
There exists a constant \(F\in (0,1/2)\) such that for all \(t\in \mathbb {R}\) with \(|t|\geq 3\) one has
where the implied constant is uniform in \(\sigma \).
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)|=\Re 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\)
There exists \(C{\gt}0\) such that for all \(\delta \in (0,1)\) and \(t\in \mathbb {R}\) with \(|t|\geq 3\); if \(\zeta (\rho )=0\) with \(\rho =\sigma +it\), then
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 \(n \geq 1\). Suppose that primes \(p_1,p_2,p_3,q_1,q_2,q_3\) satisfy
and the key criterion
Then \(L_n\) is not highly abundant.
There exists a constant \(X_0\) (one may take \(X_0 = 89693\)) with the following property: for every real \(x \ge X_0\), there exists a prime \(p\) with
For every integer \(n \ge 89693^2\), the integer \(L_n\) is not highly abundant.
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