$\psi(N,\chi)=-N^{\beta_1}/\beta_1+O(N e^{-c_1\sqrt{\log N}})$ for non-principal $\chi$, given the zero-free region

The prime number theorem for a non-principal character, given the zero-free region (Davenport §20, non-principal case). Fix a region constant $c>0$. There are constants $c_1,c_2,C>0$, depending only on $c$, such that for every modulus $q\ge1$, every non-principal Dirichlet character $\chi$ modulo $q$, every exceptional set $E$ for $\chi$ with respect to $c$ (IsExceptionalSet c χ E: at most one real zero $\beta_1\in(0,1)$ of $L(\cdot,\chi)$ in the region $\operatorname{Re}s\ge1-c/\log(q(|\operatorname{Im}s|+2))$, only for quadratic $\chi$, and no other zero $s\ne1$ in the region) whose elements are simple zeros ($L'(\beta_1,\chi)\ne0$), and every integer $N\ge2$ with

one has

where $\psi(N,\chi)=\sum_{n<N}\Lambda(n)\chi(n)$. That is, $\psi(N,\chi)=-N^{\beta_1}/\beta_1+O\bigl(N\exp(-c_1\sqrt{\log N})\bigr)$, the term being present exactly when $\chi$ has an exceptional zero $\beta_1$.

This is the non-principal case of Davenport's §20 estimate (the principal character reduces to the prime number theorem with de la Vallée Poussin error term). It is proved by the contour-integral (Perron) method: $\psi(N,\chi)$ is expressed through $-L'/L(s,\chi)$ on a vertical line, the contour is moved to the left edge $\operatorname{Re}s=1-c'/\log(q(T+2))$ of the zero-free region, the exceptional zero contributes the residue $-N^{\beta_1}/\beta_1$, and the bound $L'/L\ll\log^2(q(|t|+2))$ on the contour together with the choice $T=\exp(\sqrt{\log N})$ gives the error term.

Formalization Note The statement is Davenport.psi_char_of_region restricted to $\chi\ne1$, with the additional hypothesis that the elements of $E$ are simple zeros, as in Davenport's formulation ($\beta_1$ is simple by §14). The sum over $E$ is a finite sum (finsum) over the at most one element of $E$; $N^{\beta}$ is the complex power (N : ℂ) ^ β.