Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

−Re⁡ L′/L(s,χ)≤clog⁡(q(∣t∣+2))−∑ρRe⁡1s−ρ-\operatorname{Re}\,L'/L(s,\chi)\le c\log(q(|t|+2))-\sum_{\rho}\operatorname{Re}\frac{1}{s-\rho}−ReL′/L(s,χ)≤clog(q(∣t∣+2))−∑ρ​Res−ρ1​ near Re⁡s=1\operatorname{Re}s=1Res=1 (Davenport §14)

Proved
Davenport.neg_logDeriv_LFunction_le_sum_zeros

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

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

The zero-sum bound for −L′/L-L'/L−L′/L near the line Re⁡s=1\operatorname{Re}s=1Res=1 (Davenport §14, from the Hadamard product of §12). There is an absolute constant c>0c>0c>0 such that for every modulus q≥1q\ge1q≥1, every non-principal Dirichlet character χ\chiχ modulo qqq, every s=σ+its=\sigma+its=σ+it with 1<σ≤21<\sigma\le21<σ≤2, and every finite multiset ZZZ of zeros of L(⋅,χ)L(\cdot,\chi)L(⋅,χ) lying in the closed disc ∣ρ−s∣≤12|\rho-s|\le\tfrac12∣ρ−s∣≤21​, each zero repeated at most as often as its multiplicity,

Re⁡(−L′L(s,χ))  ≤  clog⁡(q(∣t∣+2))−∑ρ∈ZRe⁡1s−ρ.\operatorname{Re}\Bigl(-\frac{L'}{L}(s,\chi)\Bigr)\;\le\;c\log\bigl(q(|t|+2)\bigr)-\sum_{\rho\in Z}\operatorname{Re}\frac{1}{s-\rho}.Re(−LL′​(s,χ))≤clog(q(∣t∣+2))−ρ∈Z∑​Res−ρ1​.

Davenport proves, for primitive χ\chiχ, the identity −L′/L(s,χ)=12log⁡qπ+12Γ′Γ(s+a2)−B(χ)−∑ρ(1s−ρ+1ρ)-L'/L(s,\chi)=\tfrac12\log\tfrac q\pi+\tfrac12\tfrac{\Gamma'}{\Gamma}\bigl(\tfrac{s+a}{2}\bigr)-B(\chi)-\sum_\rho\bigl(\tfrac1{s-\rho}+\tfrac1\rho\bigr)−L′/L(s,χ)=21​logπq​+21​ΓΓ′​(2s+a​)−B(χ)−∑ρ​(s−ρ1​+ρ1​) with Re⁡B(χ)=−∑ρRe⁡1ρ\operatorname{Re}B(\chi)=-\sum_\rho\operatorname{Re}\tfrac1\rhoReB(χ)=−∑ρ​Reρ1​, giving −Re⁡L′/L(s,χ)<clog⁡(q(∣t∣+2))−∑ρRe⁡1s−ρ-\operatorname{Re}L'/L(s,\chi)<c\log(q(|t|+2))-\sum_\rho\operatorname{Re}\tfrac1{s-\rho}−ReL′/L(s,χ)<clog(q(∣t∣+2))−∑ρ​Res−ρ1​ over all nontrivial zeros; since every term Re⁡1s−ρ\operatorname{Re}\tfrac1{s-\rho}Res−ρ1​ is positive for Re⁡s>1\operatorname{Re}s>1Res>1, the sum may be restricted to any sub-multiset of the zeros, in particular to those within distance 12\tfrac1221​ of sss (a local form that can also be obtained by the Borel–Carathéodory method without the Hadamard product). Imprimitive χ\chiχ reduce to the inducing primitive character, whose extra Euler factors contribute O(log⁡q)O(\log q)O(logq) and no zeros with Re⁡ρ>0\operatorname{Re}\rho>0Reρ>0. Multiplicities are expressed through Mathlib's analyticOrderAt. This is the central analytic input of both the zero-free region and the estimates for ψ(x,χ)\psi(x,\chi)ψ(x,χ).

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

open Classical in
theorem neg_logDeriv_LFunction_le_sum_zeros :
    ∃ c : ℝ, 0 < c ∧
      ∀ (q : ℕ) [NeZero q] (χ : DirichletCharacter ℂ q), χ ≠ 1 →
        ∀ s : ℂ, 1 < s.re → s.re ≤ 2 →
          ∀ Z : Multiset ℂ, (∀ ρ ∈ Z, ‖ρ - s‖ ≤ 1 / 2) →
            (∀ ρ : ℂ, (Z.count ρ : ℕ∞) ≤ analyticOrderAt (DirichletCharacter.LFunction χ) ρ) →
              (-(deriv (DirichletCharacter.LFunction χ) s / DirichletCharacter.LFunction χ s)).re
                ≤ c * Real.log ((q : ℝ) * (|s.im| + 2))
                    - (Z.map fun ρ => (1 / (s - ρ)).re).sum := 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, the inequality −Re L'/L(s,χ) < c log(q(|t|+2)) − Σ_ρ Re 1/(s−ρ) for 1 ≤ σ ≤ 2 derived from the partial-fraction formula of §12 (the Hadamard product for ξ(s,χ)); stated here for zeros in the disc |ρ−s| ≤ 1/2 with multiplicity
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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me