$\zeta'/\zeta(s)+1/(s-1)\ll\log^2 q(|t|+2)$ in a zero-free region of $\zeta$ (Davenport §§13, 18)

The logarithmic derivative of $\zeta$ in a zero-free region, with the pole removed. Fix a region constant $c>0$. There is a constant $C>0$, depending only on $c$, such that the following holds for every integer $q\ge1$ (a parameter only entering through the shape of the region). Suppose that

Then for every $s=\sigma+it\ne1$ with

one has

This is the estimate for $\zeta'/\zeta$ on the shifted contour in de la Vallée Poussin's proof of the prime number theorem with error term $x\exp(-c\sqrt{\log x})$ (Davenport §18), stated with the modulus-dependent region $1-c/\log(q(|t|+2))$ so that it serves the principal character in the Siegel–Walfisz theorem: since $L(s,\chi_0)=\zeta(s)\prod_{p\mid q}(1-p^{-s})$, the hypothesis is exactly the zero-freeness of $L(\cdot,\chi_0)$ in the region of IsExceptionalSet, and the conclusion is the $\chi_0$ case of Davenport.logDeriv_LFunction_region_bound up to the $O(\log q)$ contribution of the finite Euler product. For $q=1$ it is the classical statement. It follows from Landau's local partial-fraction expansion of the logarithmic derivative of the entire function $(s-1)\zeta(s)$ on discs $|s-(2+it)|\le 3/2$ (the platform theorem Zeta23.WeilEF.logDeriv_partial_fraction_disk, with the growth bound $\zeta(s)\ll|t|$ for $\sigma\ge\delta$), because in the region every zero $\rho$ of $\zeta$ in such a disc satisfies $\operatorname{Re}s-\operatorname{Re}\rho\gg1/\log(q(|t|+2))$ and there are $O(\log(q(|t|+2)))$ of them; for $\sigma$ large the Dirichlet series gives a trivial bound.

Formalization Note. InRegion c q s unfolds to $1-c/\log(q(|\operatorname{Im}s|+2))\le\operatorname{Re}s$; deriv riemannZeta s / riemannZeta s is $\zeta'/\zeta(s)$ (Mathlib's riemannZeta, whose value at $s=1$ is irrelevant since $s\ne1$ is assumed). The hypothesis may be unsatisfiable for large $c$ (e.g. if the region contains $s=-2$), in which case the statement is vacuous, not false.