Prove2Me

Convexity bound: 0≤μ(12)≤140\le\mu(\tfrac12)\le\tfrac14 (Lindelöf 1908)

Proved
LindelofHypothesis.mu_half_convexity_bound

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

analytic-number-theorylindelof-hypothesisriemann-zeta

The growth exponent on the critical line satisfies

0≤μ ⁣(12)≤14,0\le\mu\!\left(\tfrac12\right)\le\tfrac14 ,

where μ(σ)=inf⁡{a∈R:ζ(σ+iT)=O(Ta)}\mu(\sigma)=\inf\{a\in\mathbb R:\zeta(\sigma+iT)=O(T^{a})\}. In particular ζ(12+it)=O(t1/4+ε)\zeta(\tfrac12+it)=O(t^{1/4+\varepsilon}) for every ε>0\varepsilon>0.

This is Lindelöf's convexity bound (1908), the first entry of the table of known bounds for μ(12)\mu(\tfrac12).

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_half_convexity_bound : 0 ≤ mu (1 / 2) ∧ mu (1 / 2) ≤ ((1 / 4 : ℝ) : 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 0 ≤ μ(1/2) ≤ 1/4", and first row of the table (Lindelöf 1908, convexity bound).
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