Generalized Riemann Hypothesis

Reference: Wikipedia

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