Dependency graph

Legend

Boxes: definitions
Ellipses: theorems and lemmas
Blue border: the statement of this result is ready to be formalized; all prerequisites are done
Orange border: the statement of this result is not ready to be formalized; the blueprint needs more work
Blue 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
Dark green border: this is in Mathlib

Theorem 1

For each fixed \(A \geq 0\),

\[ \sum _{q \le Q} \max _{y \le x} \max _{a \in (\mathbb {Z}/q\mathbb {Z})^*} \left| \psi (y; q, a) - \frac{y}{\varphi (q)} \right| \ll _A \frac{x}{(\log x)^{A}} \]

uniformly for all \(x \ge 2\) and \(1 \le Q \le \frac{\sqrt{x}}{(\log x)^{A+3}}\).

LaTeX Lean

Theorem 33

For \(x, Q \ge 2\), \(U, V \in [1, x]\) and \(r \in \mathbb {N}\),

\[ \sum _{q \le Q} \mathop{{\sum \nolimits ^{*}}}_{\chi \pmod{q}} \frac{q}{\varphi (q)}\, \max _{y \le x} S_r(y, \chi ) \ll \left(x + \frac{Qx}{\sqrt{U}} + \frac{Qx}{\sqrt{V}} + Q^2\sqrt{x}\right)(\log x)^3 \]

LaTeX Lean

Theorem 7

For each fixed \(A \ge 0\) we have

\[ \sum _{q\le Q} \max _{\sqrt x \le y \le x} \max _{a \in (\mathbb {Z}/q\mathbb {Z})^*} \left| \Delta _{\Lambda }(y; q,a) \right| \ll _A \frac{x}{(\log x)^{A}} \]

uniformly for \(x \ge 2\) and \(1 \le Q \le \sqrt{x}/(\log (x))^{A+3}\)

LaTeX Lean

Theorem 35

For each fixed \(A \ge 0\), \(x \ge 2\) and \(1 \le Q \le \sqrt{x}/(\log x)^{A+3}\),

\[ \sum _{q \le Q} \max _{\sqrt{x} \le y \le x} \max _{a \in (\mathbb {Z}/q\mathbb {Z})^*} \left|\Delta _{\Lambda ^\flat }(y;\, q,\, a)\right| \ll _A \frac{x}{(\log x)^A} \]

LaTeX Lean

Theorem 30

\[ \sum _{q \le Q} \max _{\substack {\sqrt{x} \le y \le x \\ a \in (\mathbb {Z}/q\mathbb {Z})^*}} \left|\Delta _{\Lambda ^\flat }(y;\, q,\, a)\right| \le \sum _{r \le Q} \frac{T_r(x,Q)}{\varphi (r)} + O\! \left(\frac{x}{(\log x)^A}\right) \]

LaTeX Lean

Theorem 16

For each fixed \(A \ge 0\), \(x \ge 2\) and \(1 \le Q \le \sqrt{x}/(\log x)^{A+3}\),

\[ \sum _{q \le Q} \max _{\sqrt{x} \le y \le x} \max _{a \in (\mathbb {Z}/q\mathbb {Z})^*} |\Delta _{\Lambda _{\le U}}(y;\, q,\, a)| \le Q\sqrt{x} \ll _A \frac{x}{(\log x)^{A+2}} \]

LaTeX Lean

Theorem 23

For each fixed \(A \ge 0\), \(x \ge 2\) and \(1 \le Q \le \sqrt{x}/(\log x)^{A+3}\),

\[ \sum _{q \le Q} \max _{\sqrt{x} \le y \le x} \max _{a \in (\mathbb {Z}/q\mathbb {Z})^*} |\Delta _{\Lambda ^\sharp }(y;\, q,\, a)| \ll _A \frac{x}{(\log x)^A} \]

LaTeX Lean

Lemma 26

This is a standard result. Let \(f\) be a function from Dirichlet characters. Then

\[ \sum _{\substack {\chi \pmod{q} \\ \chi \ne \chi _0}} f(\chi ) = \sum _{d \mid q} \mathop{{\sum \nolimits ^{*}}}_{\xi \pmod{d}} f(1_{(n,q)=1}\xi ) \]

LaTeX Lean

Lemma 27

Let \(f\) be an arithmetic function. For \(r \le x\), \(q {\gt} 1\) and \((a, q) = 1\),

\[ \mathop{{\sum \nolimits ^{*}}}_{\xi \pmod{q}} \bar\xi (a) \sum _{n \le y} \xi (n) f_r(n) = \sum _{d \mid q} \mu (q/d)\, \varphi (d)\, \Delta _{f_{rq}}(y;\, d,\, a) \]

LaTeX Lean

Definition 4

\[ \Delta _f(x ;q, a) := \sum _{n \le x, ~ n \equiv a \pmod q} f(n) ~ - \frac{1}{\varphi (q)} \sum _{n \le x, (n, q) = 1} f(n) \]

for \(x \ge 1\), \(q \in \mathbb {N}\)

LaTeX Lean

Lemma 19

If \(g\) is continuously differentiable on \([1, x]\) then

\[ \Delta _g(x;\, q,\, a) = \Delta _1(x;\, q,\, a)\, g(x) - \int _1^x \Delta _1(t;\, q,\, a)\, g'(t)\, \mathrm{d}t \]

LaTeX Lean

Lemma 17

If \(f\) is an arithmetic function supported on \([1, y]\) then

\[ \Delta _{f*g}(x;\, q,\, a) = \sum _{\substack {k \le y \\ (k,q)=1}} f(k)\, \Delta _g\! \left(\frac{x}{k};\, q,\, a\bar{k}\right) \]

LaTeX Lean

Theorem 5

\[ \Delta _f(y ;q, a) = \frac{1}{\varphi (q)} \sum _{\chi \pmod{q}, \chi \ne \chi _0} \bar\chi (a) \sum _{n \le y} f(n) \chi (n) \]

LaTeX Lean

Theorem 21

Let \(v \ge 0\) and let \(f\) be an arithmetic function supported on \([1, x]\). For \(x \ge 2\), \(q \in \mathbb {N}\) and \(a \in (\mathbb {Z}/q\mathbb {Z})^*\),

\[ |\Delta _{f * \log ^v}(x;\, q,\, a)| \le 2(\log x)^v \sum _{k \le x} |f(k)| \]

LaTeX Lean

Theorem 8

\[ \Delta _{\Lambda }(x; q, a) = \psi (x; q,a) - \frac{1}{\varphi (q)} \sum _{n \le x, n \not\mid q} \Lambda (n) \]

LaTeX Lean

Lemma 28

\[ \left|\Delta _{\Lambda ^\flat }(y;\, q,\, a)\right| \le \frac{1}{\varphi (q)} \left|\sum _{\substack {d \mid q \\ 1 {\lt} d \le (\log x)^C}} \sum _{s \mid d} \mu (d/s)\, \varphi (s)\, \Delta _{\Lambda ^\flat _q}(y;\, s,\, a)\right| + \frac{1}{\varphi (q)} \sum _{\substack {d \mid q \\ d {\gt} (\log x)^C}} \mathop{{\sum \nolimits ^{*}}}_{\xi \pmod{d}} S_{q/d}(y, \xi ) \]

LaTeX Lean

Theorem 29

\[ \frac{1}{\varphi (q)} \left|\sum _{\substack {d \mid q \\ 1 {\lt} d \le (\log x)^C}} \sum _{s \mid d} \mu (d/s)\, \varphi (s)\, \Delta _{\Lambda ^\flat _q}(y;\, s,\, a)\right| \ll _{A,C} \frac{x}{\varphi (q)\, (\log x)^{A+1}} \]

LaTeX Lean

Lemma 15

For \(y, U {\gt} 0\), \(q \in \mathbb {N}\) and \(a \in \mathbb {Z}/q\mathbb {Z}\),

\[ |\Delta _{\Lambda _{\le U}}(y;\, q,\, a)| \ll U \log {x} \]

LaTeX Lean

Theorem 22

For \(U, V \ge 1\), \(x \ge 2\), \(q \in \mathbb {N}\), \(r \le x\) and \(a \in (\mathbb {Z}/q\mathbb {Z})^*\),

\[ \max _{y \le x} \max _{a \in (\mathbb {Z}/q\mathbb {Z})^*} |\Delta _{\Lambda ^\sharp _r}(y;\, q,\, a)| \ll UV \log x \]

LaTeX Lean

Lemma 20

If \(g\) is continuously differentiable and monotone on \([1, x]\) with \(g(1) = 0\), then for all \(t \ge 1\) and \(a \in (\mathbb {Z}/q\mathbb {Z})^*\),

\[ |\Delta _g(x;\, q,\, a)| \le 2g(x) \]

LaTeX Lean

Lemma 18

For \(x \ge 1\), \(q \in \mathbb {N}\) and \(a \in (\mathbb {Z}/q\mathbb {Z})^*\),

\[ |\Delta _1(x;\, q,\, a)| \le 1 \]

LaTeX Lean

Theorem 13

Decompose \(\Lambda = \Lambda ^\sharp + \Lambda ^\flat + \Lambda _{\le U}\)

LaTeX Lean

Definition 11

\(\Lambda ^\flat = (\Lambda _{{\gt}U} * 1) * \mu _{{\gt}V}\)

LaTeX Lean

Lemma 32

\[ \Lambda ^\flat (n) = \sum _{U {\lt} 2^j \le 2x/V} (f_j * g_j)(n) \quad \text{for } n \le x, \]

where \(f_j(k) = (\Lambda _{{\gt}U} * 1)(k)\, 1_{2^{j-1} {\lt} k \le 2^j}\) and \(g_j(\ell ) = \mu (\ell )\, 1_{V {\lt} \ell \le x/2^{j-1}}\).

LaTeX Lean

Definition 12

\(\Lambda _{\le U} = 1_{≤ U} \cdot \Lambda \)

LaTeX Lean

Definition 10

\(\Lambda ^\sharp = \mu _{\le V} * \log - (\Lambda _{\le U} * \mu _{\le V}) * 1\)

LaTeX Lean

Theorem 31

Let \(f\) and \(g\) be arithmetic functions supported on \([1, M]\) and \([1, N]\) respectively. For \(x, Q \ge 1\),

\[ \sum _{q \le Q} \mathop{{\sum \nolimits ^{*}}}_{\chi \pmod{q}} \frac{q}{\varphi (q)} \max _{y \le x}\left|\sum _{n \le y} (f*g)(n)\chi (n)\right| \ll \left(\sqrt{MN} + \sqrt{M}\, Q + \sqrt{N}\, Q + Q^2\right)(\log x)\, \| f\| _2\, \| g\| _2 \]

LaTeX Lean

Definition 6

For \(f : \mathbb {N}\rightarrow \mathbb {R}\) and \(r : \mathbb {N}\) we use \(f_r\) to denote \(n \mapsto f(n) 1_{(n, r) = 1}\)

LaTeX Lean

Definition 24

\[ S_r(y, \xi ) := \left|\sum _{n \le y} \Lambda _r^\flat (n)\, \xi (n)\right| \]

LaTeX Lean

Lemma 14

\[ \sum _{n \le y} \Lambda (n) \ll U \log {x} \]

LaTeX Lean

Theorem 9

For all \(A \in \mathbb {N}\),

\[ \sum _{n \le x, n \not\mid q} \Lambda (n) = x + O_A(x/\log (x)^A+\log q \log x) \]

LaTeX Lean

Definition 25

\[ T_r(x, Q) := \sum _{(\log x)^C {\lt} d \le Q/r} \frac{1}{\varphi (d)} \mathop{{\sum \nolimits ^{*}}}_{\xi \pmod{d}} \max _{\sqrt{x} \le y \le x} S_r(y, \xi ) \]

LaTeX Lean

Theorem 34

\[ T_r(x,Q) \ll \frac{x}{(\log x)^{C-3}} + \frac{x(\log x)^4}{\sqrt{U}} + \frac{x(\log x)^4}{\sqrt{V}} + \frac{Q\sqrt{x}\, (\log x)^3}{r} \]

LaTeX Lean