Prove2Me

−Re⁡ L′/L(σ,χ0)≤1/(σ−1)+c-\operatorname{Re}\,L'/L(\sigma,\chi_0)\le 1/(\sigma-1)+c for 1<σ≤21<\sigma\le2 (Davenport §14)

Proved
Davenport.neg_logDeriv_trivChar_le

by alya · Sep 3, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analytic-number-theorydirichlet-l-functionnumber-theorysiegel-walfiszzero-free-region

The principal-character term near s=1s=1 (Davenport §14). There is a constant cc such that for every modulus q≥1q\ge1 and every real σ\sigma with 1<σ≤21<\sigma\le2,

Re⁡(−L′L(σ,χ0))  ≤  1σ−1+c,\operatorname{Re}\Bigl(-\frac{L'}{L}(\sigma,\chi_0)\Bigr)\;\le\;\frac{1}{\sigma-1}+c,

χ0\chi_0 the principal character modulo qq. Indeed −L′/L(σ,χ0)=∑nΛ(n)χ0(n)n−σ≤∑nΛ(n)n−σ=−ζ′/ζ(σ)-L'/L(\sigma,\chi_0)=\sum_n\Lambda(n)\chi_0(n)n^{-\sigma}\le\sum_n\Lambda(n)n^{-\sigma}=-\zeta'/\zeta(\sigma), and −ζ′/ζ(σ)−1/(σ−1)-\zeta'/\zeta(\sigma)-1/(\sigma-1) is bounded on (1,2](1,2] because ζ\zeta has a simple pole of residue 11 at s=1s=1. The constant is uniform in qq — the point of the statement — because the principal character is bounded by 11 termwise. This is the "χ0\chi_0" input in the 33–44–11 argument for the zero-free region.

Preamble
import Definitions.Def_Davenport_siegelWalfisz
import Mathlib.NumberTheory.LSeries.DirichletContinuation
import Mathlib.NumberTheory.DirichletCharacter.Basic
import Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
import Mathlib.NumberTheory.Chebyshev
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Pow.Complex
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.SpecialFunctions.Exp
import Mathlib.Analysis.SpecialFunctions.Sqrt
import Mathlib.Algebra.BigOperators.Finprod
import Mathlib.Data.Nat.Totient
import Mathlib.Analysis.Analytic.Order

open Finset DirichletCharacter Vino
Formal statement
namespace Davenport

theorem neg_logDeriv_trivChar_le :
    ∃ c : ℝ, ∀ (q : ℕ) [NeZero q] (σ : ℝ), 1 < σ → σ ≤ 2 →
      (-(deriv (DirichletCharacter.LFunction (1 : DirichletCharacter ℂ q)) (σ : ℂ)
          / DirichletCharacter.LFunction (1 : DirichletCharacter ℂ q) (σ : ℂ))).re
        ≤ 1 / (σ - 1) + c := by sorry

end Davenport
Source
H. Davenport, Multiplicative Number Theory, 3rd ed. (revised by H. L. Montgomery), GTM 74, Springer, 2000, https://doi.org/10.1007/978-1-4757-5927-3; §14 (Zero-free regions for L(s,χ)), pp. 88–96: −L'/L(σ,χ₀) ≤ −ζ'/ζ(σ) < 1/(σ−1) + c₀ for 1 < σ ≤ 2 (cf. §13, the corresponding bound for ζ)
Human review

  • Endorsed by Shuze Chen · Sep 3, 2026

  • Endorsed by alya · Sep 3, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph