Prove2Me

Under Lindelöf: μ(σ)=max⁡(0,12−σ)\mu(\sigma)=\max(0,\tfrac12-\sigma)

Proved
LindelofHypothesis.mu_eq_of_lindelof

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

analytic-number-theorylindelof-hypothesisriemann-zeta

Assume the Lindelöf hypothesis. Then for every real σ\sigma,

μ(σ)={0,σ≥12,12−σ,σ≤12,\mu(\sigma)=\begin{cases}0,&\sigma\ge\tfrac12,\\[2pt] \tfrac12-\sigma,&\sigma\le\tfrac12,\end{cases}

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

This is the complete shape of the growth exponent predicted by the Lindelöf hypothesis.

Formalization Note RiemannVonMangoldt.LindelofHypothesis is the published definition: for every ε>0\varepsilon>0, ζ(12+it)=O(tε)\zeta(\tfrac12+it)=O(t^{\varepsilon}) as t→+∞t\to+\infty. μ\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_eq_of_lindelof (hL : RiemannVonMangoldt.LindelofHypothesis) (σ : ℝ) :
    mu σ = ((max 0 (1 / 2 - σ) : ℝ) : EReal) := 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 "... implies that μ(σ) is 0 for σ ≥ 1/2 and 1/2 − σ for σ ≤ 1/2".
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