Chebyshev's bias

DefinitionThe set where primes \(\equiv 3 \pmod 4\) lead#✓fully proved

This is the set of natural numbers \(n\) for which the number of primes \(p \le n\) with \(p \equiv 3 \pmod 4\) is strictly greater than the number of primes \(p \le n\) with \(p \equiv 1 \pmod 4\).

def chebyshevLead : Set ℕ :=
  {n : ℕ | Nat.primeCountingMod n 4 1 < Nat.primeCountingMod n 4 3}

Uses 1 · Used by 1

Statement usesPrime counting in a residue class

Used byHardy–Littlewood sign changes in the prime race modulo 4

TheoremHardy–Littlewood sign changes in the prime race modulo 4#●ready to prove

There are infinitely many natural numbers \(n\) for which the primes \(p \le n\) with \(p \equiv 3 \pmod 4\) strictly outnumber the primes \(p \le n\) with \(p \equiv 1 \pmod 4\), and infinitely many natural numbers \(n\) for which the primes \(p \le n\) with \(p \equiv 1 \pmod 4\) strictly outnumber the primes \(p \le n\) with \(p \equiv 3 \pmod 4\).

public theorem_wanted chebyshev_sign_change :
    chebyshevLead.Infinite ∧
    {n : ℕ | Nat.primeCountingMod n 4 3 < Nat.primeCountingMod n 4 1}.Infinite

Sources

• G.H. Hardy and J.E. Littlewood, 'Contributions to the theory of the Riemann zeta-function and the theory of the distribution of primes', Acta Math. 41 (1916) 119–196 (announced 1914). Chebyshev's original observation: P. Chebyshev, letter to M. Fuss, 1853, in Œuvres de P.L. Tchebychef, vol. I (Saint Petersburg, 1899). Listed as §106 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem chebyshev_sign_change of the lean-eval benchmark.

Uses 2

Statement usesThe set where primes \(\equiv 3 \pmod 4\) lead · Prime counting in a residue class

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.