Prove2Me

Bourgain's bound: μ(12)≤1384\mu(\tfrac12)\le\tfrac{13}{84}

Open
LindelofHypothesis.mu_half_le_thirteen_div_eightyfour

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)≤1384≈0.1548,\mu\!\left(\tfrac12\right)\le\tfrac{13}{84}\approx0.1548 ,

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

This is Bourgain's 2017 bound, the last entry of the table of known bounds for μ(12)\mu(\tfrac12) in the source.

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_thirteen_div_eightyfour : mu (1 / 2) ≤ ((13 / 84 : ℝ) : 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; table of bounds for μ(1/2), last row (13/84, 0.1548, Bourgain 2017).
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