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.

Note: the Extended Riemann Hypothesis (ERH) for Dedekind zeta functions is intentionally not stated here. Mathlib's NumberField.dedekindZeta is the naive Dirichlet series (LSeries), not a meromorphic continuation; outside the region of absolute convergence tsum returns junk 0, producing spurious zeros that make the naive foramlisation of the conjecture provably false. The ERH should be added once Mathlib provides a meromorphic continuation of the Dedekind zeta function.

References:

• The Clay Institute
• Wikipedia: Riemann hypothesis
• Wikipedia: Generalized Riemann hypothesis
• Wikipedia: Dedekind zeta function
• J. Neukirch, Algebraic Number Theory, Springer (Grundlehren 322), 1999, Chapter VII, §5.
• D. A. Marcus, Number Fields, Springer (GTM 81), 1977, Chapter VII.

theorem RiemannHypothesis.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.

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

• GRH.trivialZeros χ = if q = 1 then {x : ℤ | ∃ (n : ℕ), -2 * (↑n + 1) = x} else if χ.Odd then {x : ℤ | ∃ (n : ℕ), -2 * ↑n - 1 = x} else {x : ℤ | ∃ (n : ℕ), -2 * ↑n = x}

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}$.

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.