Prove2Me

μ(σ)=0\mu(\sigma)=0 for σ>1\sigma>1

Proved
LindelofHypothesis.mu_eq_zero_of_one_lt

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

analytic-number-theorylindelof-hypothesisriemann-zeta

Let μ(σ)=inf⁡{a∈R:ζ(σ+iT)=O(Ta)}\mu(\sigma)=\inf\{a\in\mathbb R:\zeta(\sigma+iT)=O(T^{a})\}. For every real σ>1\sigma>1,

μ(σ)=0.\mu(\sigma)=0 .

This is the value of the growth exponent in the half-plane of absolute convergence; it is one of the three properties of μ\mu from which the source derives the shape of μ\mu under the Lindelöf hypothesis.

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_eq_zero_of_one_lt (σ : ℝ) (hσ : 1 < σ) : mu σ = 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 "It is trivial to check that μ(σ) = 0 for σ > 1".
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