Completed Dirichlet $L$ -functions are bounded on vertical strips

Proved

QRHLittlewood.completedLFunction_bounded_strip

by @bwdaugherty · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theorynumber-theory

Let $\chi$ be a nontrivial Dirichlet character modulo $N\ge2$ , and let $\Lambda(s,\chi)$ be its completed $L$ -function (Gamma factor times $L(s,\chi)$ ). For all real $a\le b$ there is a constant $C$ such that

|\Lambda(s,\chi)|\le C\qquad\text{whenever } a\le\Re s\le b.

The completed function is entire for nontrivial $\chi$ ; this states that it is bounded on every closed vertical strip. This is the standard a priori growth input for Phragmén–Lindelöf arguments.

Formalization Note $\Lambda$ is Mathlib's DirichletCharacter.completedLFunction.

Preamble

import Mathlib.NumberTheory.LSeries.DirichletContinuation
import Mathlib.NumberTheory.DirichletCharacter.GaussSum
import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

open Complex

Formal statement

namespace QRHLittlewood

theorem completedLFunction_bounded_strip {N : ℕ} [NeZero N] (hN : 2 ≤ N) {χ : DirichletCharacter ℂ N}
    (hχ : χ ≠ 1) (a b : ℝ) :
    ∃ C : ℝ, ∀ s : ℂ, a ≤ s.re → s.re ≤ b → ‖DirichletCharacter.completedLFunction χ s‖ ≤ C := by sorry

end QRHLittlewood

Source

B. W. Daugherty, S. Ryan, G. Ward, Certified harmonic-measure barriers and explicit Littlewood bounds from zero-free regions, https://doi.org/10.5281/zenodo.23400116, Section 6 (Dirichlet inputs)

View graph

Completed Dirichlet LLL-functions are bounded on vertical strips

Completed Dirichlet $L$ -functions are bounded on vertical strips