Siegel–Walfisz theorem

TheoremSiegel–Walfisz theorem for Chebyshev's function in residue classes#●ready to prove

For every real \(N > 0\) there are real constants \(c > 0\), \(C > 0\) and \(X_0 > 1\) such that for every real \(x \ge X_0\), every positive integer \(q\) with \(q \le (\log x)^N\) and every unit \(a\) of \(\mathbb{Z}/q\mathbb{Z}\),

\[\left|\psi(x; q, a) - \frac{x}{\varphi(q)}\right| \le C x \exp\left(-c \sqrt{\log x}\right),\]

where \(\psi(x; q, a)\) is Chebyshev's function in the residue class \(a\) modulo \(q\) and \(\varphi\) is Euler's totient function.

The constants may depend on \(N\), but not on \(x\), \(q\), or \(a\).

public theorem_wanted siegel_walfisz (N : ℝ) (hN : 0 < N) :
    ∃ (c C X₀ : ℝ), 0 < c ∧ 0 < C ∧ 1 < X₀ ∧
      ∀ x : ℝ, X₀ ≤ x →
        ∀ q : ℕ, 0 < q →
          ∀ a : ZMod q, IsUnit a →
            (q : ℝ) ≤ (Real.log x) ^ N →
              |Chebyshev.psiResidueClass a x - x / (Nat.totient q : ℝ)| ≤
                C * x * Real.exp (-c * Real.sqrt (Real.log x))

Sources

• P. Holdridge, Random Diophantine Equations in the Primes, arXiv:2305.06306v2, Theorem 4.2, citing H. Davenport, Multiplicative Number Theory, 2nd ed., revised by H. L. Montgomery, Springer, 1980, Chapter 22.

Uses 1

Statement usesChebyshev's function in a residue class

TheoremSiegel–Walfisz theorem for primes in arithmetic progressions#●ready to prove

Let \(\varphi\) be Euler's totient function and let \(\mathrm{Li}(x) = \int_2^x du / \log u\). For every real \(B > 0\) there are real constants \(c > 0\), \(C > 0\) and \(X_0 \ge 2\) such that for every real \(x \ge X_0\) and all natural numbers \(q > 0\) and \(b\) with \(\gcd(b, q) = 1\) and \(q \le (\log x)^B\), the number \(\pi(x; q, b)\) of primes \(p \le x\) with \(p \equiv b \pmod q\) satisfies

\[\left|\pi(x; q, b) - \frac{\mathrm{Li}(x)}{\varphi(q)}\right| \le C x e^{-c \sqrt{\log x}}.\]

The constants may depend on \(B\), but not on \(x\), \(q\), or \(b\). The logarithmic integral is taken from \(2\), as in the source, rather than as the principal value from \(0\).

public theorem_wanted uniform_prime_counting_arithmetic_progression (B : ℝ) (hB : 0 < B) :
    ∃ (c C X₀ : ℝ), 0 < c ∧ 0 < C ∧ 2 ≤ X₀ ∧
      ∀ x : ℝ, X₀ ≤ x →
        ∀ q b : ℕ, 0 < q → Nat.Coprime b q →
          (q : ℝ) ≤ (Real.log x) ^ B →
            |(((Finset.range (Nat.floor x + 1)).filter fun p =>
                Nat.Prime p ∧ Nat.ModEq q p b).card : ℝ) -
              (∫ u in (2 : ℝ)..x, (Real.log u)⁻¹) / (Nat.totient q : ℝ)| ≤
                C * x * Real.exp (-c * Real.sqrt (Real.log x))

Sources

• A. Guo, Exceptional sets for compositions involving Euler's function, the divisor-sum function and Dedekind's function, arXiv:2608.19972v1, Lemma siegel, main.tex lines 289–295.

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.