RH is equivalent to holomorphic continuation of the Moebius Dirichlet series

Proved

riemann_hypothesis_iff_moebius_holomorphic_extension

by ryanshin · Sep 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theorydirichlet-seriesformalizationriemann-hypothesis

Let $D(s)=\sum_{n\ge1}\mu(n)n^{-s}$ on $\operatorname{Re}s>1$ , where $\mu$ is the arithmetic Moebius function. Then

\mathrm{RH}\quad\Longleftrightarrow\quad \exists F\text{ holomorphic on }\operatorname{Re}s>\tfrac12\text{ with }F(s)=D(s)\text{ for }\operatorname{Re}s>1.

This is a proved equivalence, not a proof that either equivalent assertion holds. It provides a precise analytic-continuation formulation of the unresolved Riemann Hypothesis. Only continuation is required; no claim of absolute summability in the critical strip is made.

Preamble

import Mathlib.NumberTheory.LSeries.Dirichlet
import Mathlib.NumberTheory.LSeries.Nonvanishing
import Mathlib.Analysis.Analytic.Uniqueness
import Mathlib.Analysis.Complex.Convex
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Ring
open MeasureTheory
open scoped Topology

Formal statement

theorem riemann_hypothesis_iff_moebius_holomorphic_extension :
    RiemannHypothesis ↔
      ∃ F : ℂ → ℂ,
        DifferentiableOn ℂ F {s : ℂ | 1 / 2 < s.re} ∧
        ∀ s : ℂ, 1 < s.re →
          F s = LSeries (fun n : ℕ => (ArithmeticFunction.moebius n : ℂ)) s := by sorry

Source

E. C. Titchmarsh, The Theory of the Riemann Zeta-function, second edition revised by D. R. Heath-Brown (1986), Section 14.25(A), p. 369, and the analytic-continuation paragraph preceding 14.25(B), p. 370. https://sites.math.rutgers.edu/~zeilberg/EM18/TitchmarshZeta.pdf. This is the derived holomorphic-continuation criterion discussed there, not a claim that the continuation exists unconditionally.

View graph