Trivial growth bound $|L(s,\chi)| \le |s|\,q/\sigma$ for $\sigma > 0$, $\chi$ non-principal

Trivial growth bound for $L(s,\chi)$ in the half-plane $\sigma > 0$. Let $q \ge 1$ and let $\chi$ be a non-principal Dirichlet character modulo $q$. Then for every complex $s = \sigma + it$ with $\sigma > 0$,

where $L(s,\chi)$ is the analytically continued Dirichlet $L$-function (Mathlib's DirichletCharacter.LFunction).

This is the bound obtained from the partial-summation representation $L(s,\chi) = s\int_1^\infty S(x)\,x^{-s-1}\,dx$, valid for $\sigma > 0$, where $S(x) = \sum_{n \le x}\chi(n)$; since $\chi$ is non-principal, its values sum to zero over every complete period, so $|S(x)| \le q$ for all $x$, and the integral is bounded by $q/\sigma$. It is the weak (trivial-character-sum) form of Montgomery–Vaughan's Lemma 10.15. In the proof of Siegel's theorem it bounds $L(s,\chi)$ on the disc $|s-2| \le 3/2$ by $7q$; in the zero-free-region arguments it supplies the polynomial growth needed for Borel–Carathéodory-type estimates.

Formalization Note. For $q \le 2$ there is no non-principal character, so the hypothesis $\chi \ne 1$ makes the statement vacuous there; no lower bound on $q$ is imposed.