Conjugation symmetry of $\zeta'$ : $\zeta'(\overline{s}) = \overline{\zeta'(s)}$

Proved

deriv_riemannZeta_conj

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

analytic-number-theorycomplex-analysispntriemann-zeta

For every complex number $s$ , the derivative of the Riemann zeta function satisfies the conjugation symmetry

\zeta'\left(\overline{s}\right) \;=\; \overline{\zeta'(s)},

where $\overline{z}$ denotes complex conjugation.

This is the derivative-level companion of the reflection identity $\overline{\zeta(\overline{s})} = \zeta(s)$ : since conjugation is an (antiholomorphic) isometry, differentiating the reflected function transfers the symmetry from $\zeta$ to $\zeta'$ . Together the two identities say that the pair $(\zeta, \zeta')$ is completely determined by its behaviour in the upper half-plane.

In the PNT+ project this lemma allows every bound on $\zeta'$ — such as the $O((\log t)^2)$ estimates near the $1$ -line — proved for $t > 0$ to be transferred verbatim to $t < 0$ , halving the case analysis in the zero-free region and contour-integration arguments.

Preamble

import Mathlib.Analysis.Calculus.Deriv.Star
import Mathlib.Analysis.Normed.Module.Connected
import Mathlib.NumberTheory.Harmonic.ZetaAsymp

open scoped Complex ComplexConjugate

Formal statement

theorem deriv_riemannZeta_conj (s : ℂ) :
    deriv riemannZeta (conj s) = conj (deriv riemannZeta s) := by sorry

Source

https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/f55e85551ac10e96d98262a354cfcaac2825f2da/PrimeNumberTheoremAnd/ZetaConj.lean#L69-L71

View graph

Conjugation symmetry of ζ′\zeta'ζ′: ζ′(s‾)=ζ′(s)‾\zeta'(\overline{s}) = \overline{\zeta'(s)}ζ′(s)=ζ′(s)​

Conjugation symmetry of $\zeta'$ : $\zeta'(\overline{s}) = \overline{\zeta'(s)}$