Read-back: Davenport.psi_char_of_region

Statement. The declaration asserts: for every real number $c$ with $c > 0$, there exist three real numbers $c_1, c_2, C$, all strictly positive, such that the following holds for every modulus, every Dirichlet character, every set $E$, and every $N$. The quantifier order matters: $c$ is given first; then $c_1, c_2, C$ are chosen (they are allowed to depend on $c$, and on nothing else); and only afterwards are $q$, $\chi$, $E$, $N$ quantified, so $c_1, c_2, C$ are uniform in all four of those. The three constants are required only to be positive reals — no upper bound, no lower bound, and no relation among them or to $c$ is imposed.

The inner universally quantified claim. For every natural number $q$ that is nonzero (the typeclass hypothesis NeZero q, i.e. $q \ge 1$), for every Dirichlet character $\chi$ modulo $q$ with values in $\mathbb{C}$, and for every subset $E \subseteq \mathbb{C}$, if $E$ is an exceptional set for $\chi$ at parameter $c$ (unfolded below), then for every natural number $N$ satisfying

one has

Here $\Lambda$ is the von Mangoldt function (cast from $\mathbb{R}$ into $\mathbb{C}$), the summation index runs over $n = 0, 1, \dots, N-1$ (strictly below $N$; the value $n = N$ is not included, and $\Lambda(0) = \Lambda(1) = 0$), $\chi(n \bmod q)$ is the character evaluated at the residue class of $n$ in $\mathbb{Z}/q\mathbb{Z}$ (in particular it is $0$ when $\gcd(n,q) > 1$), $\mathbf{1}$ denotes the trivial (principal) character modulo $q$ — the multiplicative unit — so the subtracted main term is exactly the complex number $N$ when $\chi$ is principal and $0$ for every non-principal $\chi$, $N^{z}$ is the complex power $\exp(z \log N)$ of the positive real $N \ge 2$, $|\cdot|$ is the complex modulus, and the right-hand side is the real number $C \cdot N \cdot e^{-c_1 \sqrt{\log N}}$ (note $\log N \ge \log 2 > 0$, so the square root is real and positive). The sum $\sum_{z \in E} N^{z}/z$ is a finite sum over the set $E$, defined to be $0$ when the summand has infinite support; it is added to, not subtracted from, the difference of the character sum and its main term.

Unfolding IsExceptionalSet c χ E. The hypothesis on $E$ is the conjunction of exactly three conditions.

1. $E$ has at most one element ($E$ is a subsingleton: any two of its elements are equal). In particular $E = \varnothing$ is permitted, and then the added sum is $0$; otherwise $E = \{\beta\}$ for a single $\beta \in \mathbb{C}$ and the added sum is $N^{\beta}/\beta$.

2. Every $z \in E$ satisfies all seven of: $\operatorname{Im} z = 0$; $\operatorname{Re} z > 0$; $\operatorname{Re} z < 1$; $z$ lies in the region (unfolded below); $L(z, \chi) = 0$, where $L(\cdot,\chi)$ is the analytically continued Dirichlet $L$-function of $\chi$; $\chi$ is quadratic (every value of $\chi$ is $0$, $1$, or $-1$); and $\chi \ne \mathbf{1}$. Consequently, if $\chi$ is the principal character (which is automatic when $q = 1$, where every character is trivial), no $z$ can satisfy clause 2, so $E$ must be empty; and whenever $E \ne \varnothing$, $\chi$ is forced to be a non-principal quadratic character and $\beta$ is a real zero of $L(\cdot,\chi)$ in the open interval $(0,1)$.

3. Zero-freeness off $E$: for every $s \in \mathbb{C}$ with $s \ne 1$, if $s$ lies in the region and $s \notin E$, then $L(s,\chi) \ne 0$. This is asserted for all such $s$ in the region, including those with $\operatorname{Re} s \ge 1$ and arbitrary imaginary part; the single point $s = 1$ is excluded from the requirement, as is the (at most one) point of $E$.

Unfolding the region. "$s$ lies in the region" is InRegion c q s, which unfolds to the inequality

a non-strict inequality, with regionBoundary $c\, q\, s$ being the left-hand side. Since $q \ge 1$, the argument of the logarithm is at least $2$, so the logarithm is at least $\log 2 > 0$ and no division by zero occurs. For $z$ real (as in clause 2) the condition reads $1 - c/\log(2q) \le z$.

Degenerate and edge cases made explicit.

• Large $c$ can make the hypothesis unsatisfiable. The parameter $c$ is an arbitrary positive real and appears only inside the region: larger $c$ pushes regionBoundary further left, enlarging the region and therefore strengthening clause 3 (zero-freeness is demanded on a bigger set) while also relaxing the membership condition in clause 2. For $c$ large enough that the region contains points where $L(\cdot,\chi)$ vanishes at more than one place — e.g. once the region reaches $\operatorname{Re} s \le 0$ for small $|\operatorname{Im} s|$, which happens when $c \ge \log(q(|\operatorname{Im} s|+2))$ — no set $E$ satisfies IsExceptionalSet c χ E, and the whole inner claim is vacuously true for that $q$ and $\chi$. The statement makes no claim that any $E$ exists; it only says what follows if one is supplied.

• $q = 1$. Permitted by NeZero q. Then $\mathbb{Z}/1\mathbb{Z}$ is trivial, the only character is $\chi = \mathbf{1}$, $\chi(n \bmod 1) = 1$ for all $n$, $E$ must be empty by clause 2, the main term is $N$, and clause 3 demands that $L(s,\mathbf{1})$ (the Riemann zeta function in this case) be nonvanishing on the whole region except at $s = 1$.

• $E = \varnothing$. Allowed by the subsingleton condition; the correction term $\sum_{z \in E} N^{z}/z$ is then $0$ and the conclusion is the plain bound $\big|\sum_{n<N}\Lambda(n)\chi(n) - [\chi = \mathbf{1}]\,N\big| \le C N e^{-c_1\sqrt{\log N}}$.

• $s = 1$. Explicitly exempted from clause 3, so nothing is asserted about $L(1,\chi)$ (where the principal character's $L$-function has a pole). Note also that $s = 1$ can never lie in $E$, since elements of $E$ must have real part strictly less than $1$; and $z = 0$ can never lie in $E$ either (real part strictly positive), so the division by $z$ in the correction term is never by zero.

• The range hypothesis. For any fixed $q$, the condition $q \le \exp(c_2\sqrt{\log N})$ fails for small $N$ and holds for all sufficiently large $N$; conversely, for fixed $N \ge 2$ it restricts the conclusion to moduli $q$ up to $\exp(c_2\sqrt{\log N})$. Nothing is asserted for pairs $(q, N)$ outside this range, nor for $N \in \{0, 1\}$.

• No modulus, primitivity, or conductor conditions are imposed on $\chi$ beyond what clause 2 forces when $E$ is nonempty; $\chi$ may be any Dirichlet character modulo $q$ with complex values, including imprimitive ones, and $N$ need not be related to $q$ except through the displayed inequality.

• The proof is omitted (sorry); the file asserts the statement without establishing it.