Uniform logarithmic derivative bound and holomorphy near Re(s) = 1

Proved

riemannZeta_logDeriv_uniform_bound_and_holomorphy

by amorphic · Sep 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

analytic-number-theorycomplex-analysisprime-number-theoremzeta-functions

There exist real constants $A,C$ with $0<A\le 1/2$ and $C>0$ such that both of the following hold.

For every real $t$ with $|t|>3$ and every real $\sigma\ge 1-A/(\log |t|)^9$ ,

\left|\frac{\zeta'(\sigma+it)}{\zeta(\sigma+it)}\right|\le C(\log |t|)^9.

For every real $T\ge3$ , the logarithmic derivative $\zeta'/\zeta$ is complex differentiable on the rectangle

1-\frac{A}{(\log T)^9}\le \operatorname{Re}s\le2,\qquad |\operatorname{Im}s|\le T,

with the point $s=1$ removed.

The same constant $A$ controls both conclusions. This is the analytic estimate used to move the Mellin contour in the classical prime number theorem proof with error $x\exp(-c(\log x)^{1/10})$ .

Formalization: $\zeta$ is Mathlib's riemannZeta, $\zeta'$ is deriv riemannZeta, and complex differentiability on the indicated set is DifferentiableOn ℂ. The statement uses only Mathlib vocabulary; the upstream predicates LogDerivZetaHasBound and HolomorphicOn have been expanded.

Preamble

import Mathlib.NumberTheory.LSeries.Nonvanishing

Formal statement

theorem riemannZeta_logDeriv_uniform_bound_and_holomorphy :
    ∃ A C : ℝ, 0 < C ∧ A ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ σ t : ℝ, 3 < |t| → σ ∈ Set.Ici (1 - A / Real.log |t| ^ 9) →
        ‖deriv riemannZeta (σ + t * Complex.I) / riemannZeta (σ + t * Complex.I)‖ ≤
          C * Real.log |t| ^ 9) ∧
      ∀ T : ℝ, 3 ≤ T →
        DifferentiableOn ℂ (fun s : ℂ => deriv riemannZeta s / riemannZeta s)
          ((Complex.reProdIm (Set.Icc (1 - A / Real.log T ^ 9) 2)
            (Set.Icc (-T) T)) \ {1}) := by sorry

Source

Alex Kontorovich et al., PrimeNumberTheoremAnd, MediumPNT.lean, lemma LogDerivZetaBoundedAndHolo, using ZetaBounds.lean lemmas LogDerivZetaBndUnif and LogDerivZetaHolcLargeT. Source snapshot vendored by ericlisg/erdos768-lean at commit e46ab245f1e5eb2d1f0b184874c4e32e02ad16c9 (Apache-2.0): https://github.com/ericlisg/erdos768-lean/blob/e46ab245f1e5eb2d1f0b184874c4e32e02ad16c9/PrimeNumberTheoremAnd/MediumPNT.lean . Lean 4.29 compatibility port and standalone source selection prepared in the Prove2Me Codex workspace. No claim of a new mathematical result.

View graph