Lagarias criterion is equivalent to RH

riemann_hypothesis_iff_lagarias_elementary_criterion

Submitter: Kim Morrison.

Notes: Lagarias' elementary divisor-sum criterion stated using Mathlib's RiemannHypothesis, harmonic numbers, and sigma notation.

Source: https://arxiv.org/abs/math/0008177

Informal solution: Prove that the Riemann hypothesis is equivalent to the inequality σ(n) ≤ H_n + exp(H_n) log(H_n) for all positive integers n.

theorem declaration uses `sorry`riemann_hypothesis_iff_lagarias_elementary_criterion :
    RiemannHypothesis ↔ LeanEval.NumberTheory.LagariasElementaryCriterion := by⊢ RiemannHypothesis ↔ LagariasElementaryCriterion
  sorryAll goals completed! 🐙

Solved by

Not yet solved.