Prove2Me

−Re⁡ L′/L(s,χ0)≤Re⁡1s−1+clog⁡(q(∣t∣+2))-\operatorname{Re}\,L'/L(s,\chi_0)\le\operatorname{Re}\frac1{s-1}+c\log(q(|t|+2)) for 1<σ≤21<\sigma\le2 (Davenport §13–14)

Proved
Davenport.neg_logDeriv_trivChar_le_pole

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

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

The principal-character bound with the pole term (Davenport §13 for ζ\zeta, §14 for χ0\chi_0 mod qq). There is an absolute constant c>0c>0 such that for every modulus q≥1q\ge1 and every s=σ+its=\sigma+it with 1<σ≤21<\sigma\le2,

Re⁡(−L′L(s,χ0))  ≤  Re⁡1s−1+clog⁡(q(∣t∣+2)),\operatorname{Re}\Bigl(-\frac{L'}{L}(s,\chi_0)\Bigr)\;\le\;\operatorname{Re}\frac{1}{s-1}+c\log\bigl(q(|t|+2)\bigr),

χ0\chi_0 the principal character modulo qq. Since L(s,χ0)=ζ(s)∏p∣q(1−p−s)L(s,\chi_0)=\zeta(s)\prod_{p\mid q}(1-p^{-s}), one has −L′/L(s,χ0)=−ζ′/ζ(s)−∑p∣q(log⁡p)p−s1−p−s-L'/L(s,\chi_0)=-\zeta'/\zeta(s)-\sum_{p\mid q}\frac{(\log p)p^{-s}}{1-p^{-s}}, and the finite sum has real part at most ∑p∣qlog⁡p≤log⁡q\sum_{p\mid q}\log p\le\log q in absolute value; the bound −Re⁡ζ′/ζ(s)≤Re⁡1s−1+clog⁡(∣t∣+2)-\operatorname{Re}\zeta'/\zeta(s)\le\operatorname{Re}\frac1{s-1}+c\log(|t|+2) is Davenport §13's consequence of the partial-fraction formula for ζ′/ζ\zeta'/\zeta (§12), every term −Re⁡1s−ρ-\operatorname{Re}\frac1{s-\rho} over the zeros being non-positive for σ>1\sigma>1. This is the "χ2=χ0\chi^2=\chi_0" input in the 33–44–11 argument for real characters, where the third point σ+2it\sigma+2it is not on the real axis.

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.NumberTheory.LSeries.RiemannZeta

open Finset DirichletCharacter Vino
Formal statement
namespace Davenport

theorem neg_logDeriv_trivChar_le_pole :
    ∃ c : ℝ, 0 < c ∧
      ∀ (q : ℕ) [NeZero q] (s : ℂ), 1 < s.re → s.re ≤ 2 →
        (-(deriv (DirichletCharacter.LFunction (1 : DirichletCharacter ℂ q)) s
            / DirichletCharacter.LFunction (1 : DirichletCharacter ℂ q) s)).re
          ≤ (1 / (s - 1)).re + c * Real.log ((q : ℝ) * (|s.im| + 2)) := 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; §13 (A zero-free region for ζ(s)), pp. 84–87: −Re ζ'/ζ(s) < Re 1/(s−1) + c log|t| type bound from the partial-fraction formula (§12); §14, pp. 88–96: the same for L(s,χ₀) = ζ(s)∏_{p|q}(1−p^{−s})
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