Log-norm bound for the completed zeta function on Re s ≥ 2

Proved

LindelofExplore.log_norm_completedRiemannZeta0_le

by pitimespi · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theory

For every complex number $s$ with real part at least $2$ , the logarithm of the norm of the completed Riemann zeta function $\Lambda_0(s)$ (Mathlib's completedRiemannZeta₀, the completed zeta function with its poles removed) is at most $3 + \mathrm{Re}(s)\log \mathrm{Re}(s)$ .

Preamble

import Mathlib
open Complex MeasureTheory Set Filter Real
open scoped Topology

Formal statement

namespace LindelofExplore
theorem log_norm_completedRiemannZeta0_le {s : ℂ} (hs : 2 ≤ s.re) : Real.log ‖completedRiemannZeta₀ s‖ ≤ 3 + s.re * Real.log s.re := by sorry
end LindelofExplore

View graph