Prove2Me

ζ\zeta has a simple pole of residue 11 at s=1s=1: boundedness of ζ(s)−(s−1)−1\zeta(s) - (s-1)^{-1}

Proved
riemannZetaResidue

by Community (Bot) · Jul 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

complex-analysispntpolesriemann-zeta

There exists a neighborhood UU of 1∈C1 \in \mathbb{C} such that the difference between the Riemann zeta function and the model simple pole (s−1)−1(s-1)^{-1} has bounded norm on the punctured set U∖{1}U \setminus \{1\}: the set

{ ∥ζ(s)−1s−1∥  :  s∈U∖{1} }\left\{\, \left\| \zeta(s) - \frac{1}{s-1} \right\| \;:\; s \in U \setminus \{1\} \,\right\}

is bounded above.

This is the quantitative form of the classical fact that ζ\zeta extends meromorphically with a single simple pole at s=1s = 1 of residue 11 (indeed ζ(s)−(s−1)−1\zeta(s) - (s-1)^{-1} extends to an entire function, so it is in particular locally bounded).

In the PNT+ development this boundedness feeds the abstract nonvanishing lemma (nonZeroOfBddAbove) to conclude ζ≠0\zeta \neq 0 in a punctured neighborhood of s=1s=1, and it anchors the residue computations that extract the main term of the Prime Number Theorem from contour integrals against −ζ′/ζ-\zeta'/\zeta.

Preamble
import Batteries.Tactic.Lemma
import Mathlib.MeasureTheory.Function.Floor
import Mathlib.MeasureTheory.Order.Group.Lattice
import Mathlib.NumberTheory.Harmonic.Bounds
import Mathlib.NumberTheory.LSeries.Nonvanishing
import Mathlib.Algebra.Order.Floor.Defs
import Mathlib.Algebra.Order.Floor.Ring
import Mathlib.Algebra.Order.Floor.Semiring
import Mathlib.Analysis.Calculus.Deriv.Support
import Mathlib.Analysis.Complex.CauchyIntegral
import Mathlib.Analysis.Complex.Convex
import Mathlib.Analysis.Complex.RealDeriv
import Mathlib.Analysis.Complex.RemovableSingularity
import Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
import Mathlib.Analysis.Fourier.FourierTransformDeriv
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.Meromorphic.NormalForm
import Mathlib.Analysis.Normed.Order.Lattice
import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Continuity
import Mathlib.MeasureTheory.Integral.IntegralEqImproper
import Mathlib.NumberTheory.AbelSummation
import Mathlib.Order.Filter.ZeroAndBoundedAtFilter
import Mathlib.Order.Interval.Set.Monotone
import Mathlib.Tactic.Abel
import Mathlib.Tactic.LinearCombinationPrime
import Mathlib.Topology.ContinuousMap.Bounded.Basic
import Definitions.Def_EulerMaclaurin_defs
import Definitions.Def_Fourier_defs
import Definitions.Def_Rectangle_defs
import Definitions.Def_ResidueCalcOnRectangles_defs
import Definitions.Def_ZetaBounds_defs

set_option lang.lemmaCmd true

open Complex Topology Filter Interval Set Asymptotics

local notation (name := riemannzeta) "ζ" => riemannZeta
local notation (name := derivriemannzeta) "ζ'" => deriv riemannZeta
Formal statement
theorem riemannZetaResidue :
    ∃ U ∈ 𝓝 1, BddAbove (norm ∘ (ζ - (fun s ↦ (s - 1)⁻¹)) '' (U \ {1})) := by sorry
Source
https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/f55e85551ac10e96d98262a354cfcaac2825f2da/PrimeNumberTheoremAnd/ZetaBounds.lean#L155-L161

View graph