RiemannHypothesis — Mathlib

English

If Φ is periodic modulo N, then the L-series converges for 1 < Re(s).

Русский

Если функция Φ периодична по модулю N, то L-функция сходится для 1 < Re(s).

LaTeX

$$$\\\\text{LSeriesSummable}_{\\\\mathbb{Z}/N\\\\mathbb{Z}}(\\\\Phi, s) \\,\\text{ holds for } 1 < \\Re s$$$

Lean4

/-- A formal statement of the **Riemann hypothesis** – constructing a term of this type is worth a
million dollars. -/
def RiemannHypothesis : Prop :=
  ∀ (s : ℂ) (_ : riemannZeta s = 0) (_ : ¬∃ n : ℕ, s = -2 * (n + 1)) (_ : s ≠ 1), s.re = 1 / 2

Похожие утверждения