Documentation

FormalConjectures.Millenium.RiemannHypothesis

Riemann Hypothesis and its generalizations #

The Riemann Hypothesis asserts that all non-trivial zeros of the Riemann zeta function $\zeta(s)$ have real part $\frac{1}{2}$. The trivial zeros are the negative even integers $-2, -4, -6, \ldots$. The hypothesis is one of the seven Millennium Prize Problems posed by the Clay Mathematics Institute.

The Generalized Riemann Hypothesis extends this to Dirichlet $L$-functions of primitive Dirichlet characters.

The Extended Riemann Hypothesis is a closely related conjecture for Dedekind zeta functions of number fields.

Note: in Mathlib, NumberField.dedekindZeta is currently defined as the naive Dirichlet series (LSeries), not as a meromorphic continuation. The statements here follow Mathlib's naming.

References:

source
theorem riemannHypothesis :
RiemannHypothesis

The Riemann Hypothesis: all non-trivial zeros of the Riemann zeta function have real part $\frac{1}{2}$. That is, if $\zeta(s) = 0$, $s \neq 1$, and $s$ is not a trivial zero $-2(n+1)$ for some $n \in \mathbb{N}$, then $\operatorname{Re}(s) = \frac{1}{2}$.

This is the official Millennium Prize Problem as posed by the Clay Mathematics Institute.

This uses the RiemannHypothesis type from Mathlib, which is defined as ∀ (s : ℂ), riemannZeta s = 0 → (¬∃ n : ℕ, s = -2 * (n + 1)) → s ≠ 1 → s.re = 1 / 2.

source
def GRH.trivialZeros {q : ℕ} (χ : DirichletCharacter ℂ q) :
Set ℤ

Let $\chi$ be a Dirichlet character, trivialZeros is the set of trivial zeros of the Dirichlet $L$-function of $\chi$ which is always a set of non-positive integers.

  • $\chi = 1$ then the Dirichlet $L$-function is the Riemann zeta function, having trivial zeroes at all negative even integers (exclude $0$).
  • $\chi$ is odd, then the trivial zeroes are the negative odd integers.
  • $\chi \neq 1$ is even, then the trivial zeroes are the non-positive even integers.
Equations
Instances For
    source
    theorem GRH.generalized_riemann_hypothesis (q : ℕ) [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ.IsPrimitive) (s : ℂ) (hs : DirichletCharacter.LFunction χ s = 0) (hs_nontrivial : s ∉ Int.cast '' trivialZeros χ) :
    s.re = 1 / 2

    The Generalized Riemann Hypothesis asserts that all the non-trivial zeros of the Dirichlet $L$-function $L(\chi, s)$ of a primitive Dirichlet character $\chi$ have real part $\frac{1}{2}$.

    source
    theorem GRH.implies_riemannHypothesis :
    (DirichletCharacter.IsPrimitive 1 → ∀ (s : ℂ), DirichletCharacter.LFunction 1 s = 0 → s ∉ Int.cast '' trivialZeros 1 → s.re = 1 / 2) ↔ RiemannHypothesis

    GRH for $\chi = 1$ is RiemannHypothesis.

    source
    def ExtendedRiemannHypothesis.IsInCriticalStrip (s : ℂ) :
    Prop

    The (open) critical strip $\{ s \in \mathbb{C} \mid 0 < \Re(s) < 1 \}$.

    Equations
    Instances For
      source
      def ExtendedRiemannHypothesis.trivialZeros (K : Type u_1) [Field K] [NumberField K] :
      Set ℤ

      A convenient (over-)approximation to the set of trivial zeros of a Dedekind zeta function.

      When $K$ is totally real, the only poles in the completed zeta function come from $\Gamma(s/2)$, so the trivial zeros occur at non-positive even integers; otherwise $\Gamma(s)$ also appears, giving trivial zeros at all non-positive integers.

      Informally, the trivial zeros come from the poles of the $\Gamma$-factors in the functional equation for the completed zeta function. In particular, they occur at non-positive integers, with the exact pattern depending on the signature of $K$.

      Equations
      Instances For
        source
        theorem ExtendedRiemannHypothesis.extended_riemann_hypothesis_dedekindZeta (K : Type u_1) [Field K] [NumberField K] (s : ℂ) (hs : NumberField.dedekindZeta K s = 0) (hs_nontrivial : s ∉ Int.cast '' trivialZeros K) (hs_ne_one : s ≠ 1) :
        s.re = 1 / 2

        The Extended Riemann Hypothesis (ERH) for Dedekind zeta functions asserts that if $K$ is a number field and $\zeta_K(s)$ is its Dedekind zeta function, then every zero of $\zeta_K(s)$ is either a trivial zero (at a non-positive integer) or lies on the critical line $\Re(s) = \tfrac12$.

        In the formal statement below, hs_nontrivial excludes the chosen set of trivial zeros, and hs_ne_one excludes the (simple) pole at $s = 1$.

        source
        theorem ExtendedRiemannHypothesis.extended_riemann_hypothesis_dedekindZeta_of_isInCriticalStrip (K : Type u_1) [Field K] [NumberField K] (s : ℂ) (hs_strip : IsInCriticalStrip s) (hs : NumberField.dedekindZeta K s = 0) :
        s.re = 1 / 2

        A common formulation of ERH: every zero of $\zeta_K$ in the critical strip lies on the critical line.