Reflection symmetry of :
ProvedriemannZeta_conjcomplex-analysispntriemann-zetaspecial-functions
For every complex number , the Riemann zeta function commutes with complex conjugation:
This is the Schwarz reflection property of , valid on all of (with the completed meromorphic continuation): it holds because is real on the real axis where its Dirichlet series converges, and the identity propagates to the full plane by analytic continuation.
The reflection identity halves the work in zero-free-region and growth estimates: any bound on or on established for transfers immediately to , and zeros of come in conjugate pairs. The PNT+ development uses it to reduce vertical-strip estimates to the upper half-plane.
Preamble
import Mathlib.NumberTheory.LSeries.RiemannZeta open scoped Complex ComplexConjugate
Formal statement
theorem riemannZeta_conj (s : ℂ) : riemannZeta (conj s) = conj (riemannZeta s) := by sorry
Source