Prove2Me

Weyl–Hardy–Littlewood bound: μ(12)≤16\mu(\tfrac12)\le\tfrac16

Open
LindelofHypothesis.mu_half_le_one_sixth

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

analytic-number-theorylindelof-hypothesisriemann-zeta

The growth exponent on the critical line satisfies

μ ⁣(12)≤16,\mu\!\left(\tfrac12\right)\le\tfrac16 ,

i.e. ζ(12+it)=O(t1/6+ε)\zeta(\tfrac12+it)=O(t^{1/6+\varepsilon}) for every ε>0\varepsilon>0.

This is the bound of Hardy and Littlewood (1916, 1923), obtained from Weyl's method for exponential sums applied to the approximate functional equation; it is the first improvement on the 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_half_le_one_sixth : mu (1 / 2) ≤ ((1 / 6 : ℝ) : 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 "The upper bound of 1/4 was lowered by Hardy and Littlewood to 1/6", and second row of the table (Hardy & Littlewood 1916, 1923).
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