Bombieri–Vinogradov theorem

DefinitionResidue-class error of Chebyshev's function#✓fully proved

For natural numbers \(y\), \(q\) and \(a\), the residue-class error is \(E(y; q, a) = \left|\psi(y; q, a) - y/\varphi(q)\right|\), where \(\psi(y; q, a)\) is Chebyshev's function in the residue class of \(a\) modulo \(q\) and \(\varphi\) is Euler's totient function.

public noncomputable def bombieriVinogradovResidueError (y q a : ℕ) : ℝ :=
  |Chebyshev.psiResidueClass (a : ZMod q) (y : ℝ) -
    (y : ℝ) / (Nat.totient q : ℝ)|

Sources

• S. Baier and L. Zhao, Bombieri-Vinogradov Type Theorem for Sparse Sets of Moduli, arXiv:math/0602116, classical theorem display (1.1).

Uses 1 · Used by 1

Statement usesChebyshev's function in a residue class

Used byMaximal residue-class error

DefinitionMaximal residue-class error#✓fully proved

For natural numbers \(y\) and \(q\), \(E^{\ast}(y; q)\) is the maximum of the residue-class error \(E(y; q, a)\) over the natural numbers \(a < q\) coprime to \(q\), and \(0\) if there is no such \(a\).

public noncomputable def bombieriVinogradovMaxResidueError (y q : ℕ) : ℝ :=
  (((Finset.range q).filter fun a => Nat.Coprime a q).image
    fun a => bombieriVinogradovResidueError y q a).max.unbotD 0

Sources

• S. Baier and L. Zhao, Bombieri-Vinogradov Type Theorem for Sparse Sets of Moduli, arXiv:math/0602116, inner maximum of display (1.1).

Uses 1 · Used by 1

Statement usesResidue-class error of Chebyshev's function

Used byMaximal residue-class error up to a level

DefinitionMaximal residue-class error up to a level#✓fully proved

For natural numbers \(x\) and \(q\), \(E^{\ast\ast}(x; q)\) is the maximum of the maximal residue-class error \(E^{\ast}(y; q)\) over the natural numbers \(y \le x\).

public noncomputable def bombieriVinogradovMaxUpToError (x q : ℕ) : ℝ :=
  ((Finset.range (x + 1)).image
    fun y => bombieriVinogradovMaxResidueError y q).max.unbotD 0

Sources

• S. Baier and L. Zhao, Bombieri-Vinogradov Type Theorem for Sparse Sets of Moduli, arXiv:math/0602116, maximum over y ≤ x in display (1.1).

Uses 1 · Used by 1

Statement usesMaximal residue-class error

Used byBombieri–Vinogradov sum

DefinitionBombieri–Vinogradov sum#✓fully proved

For a natural number \(x\) and a real number \(A\), the Bombieri–Vinogradov sum \(S(x, A)\) is the sum of the maximal residue-class error \(E^{\ast\ast}(x; q)\) up to \(x\) over the integers \(q\) with \(1 \le q \le x\) and \(q \le \sqrt{x} / (\log x)^{A + 5}\).

When \(A > -5\) and \(x \ge 3\), the condition \(q \le x\) follows from the other one.

public noncomputable def bombieriVinogradovSum (x : ℕ) (A : ℝ) : ℝ :=
  ∑ q ∈ Finset.range (x + 1),
    if 0 < q ∧ (q : ℝ) ≤ Real.sqrt (x : ℝ) / (Real.log (x : ℝ)) ^ (A + 5)
    then bombieriVinogradovMaxUpToError x q else 0

Sources

• S. Baier and L. Zhao, Bombieri-Vinogradov Type Theorem for Sparse Sets of Moduli, arXiv:math/0602116, outer sum of display (1.1).

Uses 1 · Used by 1

Statement usesMaximal residue-class error up to a level

Used byBombieri–Vinogradov theorem

TheoremBombieri–Vinogradov theorem#●ready to prove

Let \(\psi(y; q, a)\) denote Chebyshev's function in the residue class of \(a\) modulo \(q\), and let \(\varphi\) be Euler's totient function. For a natural number \(x\) and a real number \(A\), let \(S(x, A)\) be the sum, over the integers \(q\) with \(1 \le q \le x\) and \(q \le \sqrt{x} / (\log x)^{A + 5}\), of the maximum of \(\left|\psi(y; q, a) - y/\varphi(q)\right|\) over the natural numbers \(y \le x\) and \(a < q\) coprime to \(q\). Then for every real number \(A > 0\) there are a real number \(C > 0\) and a natural number \(x_0\) such that every natural number \(x \ge x_0\) satisfies \(S(x, A) \le C x / (\log x)^A\).

The main term \(y/\varphi(q)\) depends on the inner variable \(y\); it is not a logarithmic-integral term depending on \(x\).

public theorem_wanted bombieriVinogradov (A : ℝ) (hA : 0 < A) :
    ∃ (C : ℝ) (x₀ : ℕ), 0 < C ∧
      ∀ x : ℕ, x₀ ≤ x →
        bombieriVinogradovSum x A ≤ C * (x : ℝ) / (Real.log (x : ℝ)) ^ A

Sources

• S. Baier and L. Zhao, Bombieri-Vinogradov Type Theorem for Sparse Sets of Moduli, arXiv:math/0602116, classical theorem display (1.1), source lines 54–62.

Uses 1

Statement usesBombieri–Vinogradov sum

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.