Prove2Me

μ(1)=0\mu(1)=0

Proved
LindelofHypothesis.mu_one_eq_zero

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theorylindelof-hypothesisriemann-zeta

On the line Re⁡s=1\operatorname{Re}s=1 the growth exponent vanishes:

μ(1)=0,\mu(1)=0,

where μ(σ)=inf⁡{a∈R:ζ(σ+iT)=O(Ta)}\mu(\sigma)=\inf\{a\in\mathbb R:\zeta(\sigma+iT)=O(T^{a})\}.

This is one of the two boundary values used in Lindelöf's convexity bound.

Formalization Note μ\mu is LindelofHypothesis.mu, valued in the extended reals.

Preamble
import Mathlib
import Definitions.Def_RiemannVonMangoldt_ZeroCounts
import Definitions.Def_LindelofHypothesis_GrowthAndZeroCounts

open Complex Filter Asymptotics
open scoped ENNReal
Formal statement
namespace LindelofHypothesis

theorem mu_one_eq_zero : mu 1 = 0 := by sorry

end LindelofHypothesis
Source
Wikipedia, "Lindelöf hypothesis" (snapshot supplied as Lindelöf_hypothesis.pdf, printed 12 Oct 2026), https://en.wikipedia.org/wiki/Lindel%C3%B6f_hypothesis; section "The μ function", sentence "Lindelöf's convexity result together with μ(1) = 0 and μ(0) = 1/2 implies that 0 ≤ μ(1/2) ≤ 1/4".
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 13, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph