Local partial-fraction expansion of $L'/L(s,\chi)$ with error $O(\log q(|t|+2))$ (Davenport §16)

Proved

Davenport.logDeriv_LFunction_partial_fraction

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

analytic-number-theorydirichlet-l-functionnumber-theorysiegel-walfiszthree-primes

Partial fractions for the logarithmic derivative of $L(s,\chi)$ , locally near the line $\sigma=2$ . There is an absolute constant $C>0$ such that for every modulus $q\ge1$ , every non-principal Dirichlet character $\chi$ modulo $q$ and every real height $t$ , writing $s_0=2+it$ , there is a finite set $Z$ of complex numbers such that:

$Z$ is exactly the set of zeros of $L(s,\chi)$ in the closed disc $|s-s_0|\le 3/2$ ;
counted with multiplicity, these zeros are few:

\sum_{\rho\in Z} m_\rho\;\le\;C\log\bigl(q(|t|+2)\bigr),

where $m_\rho$ is the order of the zero $\rho$ ;

on the smaller closed disc $|s-s_0|\le 7/5$ , at every point where $L(s,\chi)\ne0$ ,

\Bigl|\frac{L'}{L}(s,\chi)-\sum_{\rho\in Z}\frac{m_\rho}{s-\rho}\Bigr|\;\le\;C\log\bigl(q(|t|+2)\bigr).

This is the $L$ -function analogue of Landau's local form of the Hadamard-product expansion of $\zeta'/\zeta$ (the platform theorem Zeta23.WeilEF.zeta_logDeriv_partial_fraction), and is the form in which Davenport's §16 formula $\frac{L'}{L}(s,\chi)=\sum_{|\gamma-t|<1}\frac1{s-\rho}+O(\log q(|t|+2))$ is used in §§14, 19, 20: since the disc $|s-s_0|\le7/5$ covers the whole strip $3/5\le\sigma\le2$ at height $\approx t$ , it gives at once (a) the zero-free-region inequality $-\operatorname{Re}\frac{L'}{L}(s,\chi)\le C\log q(|t|+2)-\sum_\rho\operatorname{Re}\frac1{s-\rho}$ for $1<\sigma\le2$ (Davenport.neg_logDeriv_LFunction_le_sum_zeros), and (b) the bound $\frac{L'}{L}(s,\chi)\ll\log^2 q(|t|+2)$ inside a zero-free region, which drives the explicit-formula and contour estimates for $\psi(x,\chi)$ . It follows from the Borel–Carathéodory / Jensen argument applied to $L(\cdot,\chi)$ on the disc $|s-s_0|\le 75/44$ , using the growth bound $|L(s,\chi)|\ll q|s|$ for $\sigma\ge 1/3$ (partial summation) and the lower bound $|L(2+it,\chi)|\ge\zeta(4)/\zeta(2)$ (Euler product); for imprimitive $\chi$ the finitely many Euler factors $1-\chi^*(p)p^{-s}$ contribute $O(\log q)$ to $L'/L$ and have no zeros in the disc.

Formalization Note. logDeriv f s is Mathlib's deriv f s / f s; analyticOrderNatAt (LFunction χ) ρ is the order of the zero at $\rho$ ; $Z$ is a Finset ℂ whose underlying set is specified exactly (clause 1), so the sum in clause 3 ranges over all zeros in the disc of radius $3/2$ , with the correct multiplicities.

Preamble

import Definitions.Def_Davenport_siegelWalfisz
import Mathlib.NumberTheory.LSeries.DirichletContinuation
import Mathlib.NumberTheory.LSeries.Basic
import Mathlib.NumberTheory.DirichletCharacter.Basic
import Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
import Mathlib.NumberTheory.Chebyshev
import Mathlib.Analysis.Analytic.Order
import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
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

open Finset DirichletCharacter Vino

Formal statement

namespace Davenport

theorem logDeriv_LFunction_partial_fraction :
    ∃ C : ℝ, 0 < C ∧
      ∀ (q : ℕ) [NeZero q] (χ : DirichletCharacter ℂ q), χ ≠ 1 → ∀ t : ℝ,
        ∃ Z : Finset ℂ,
          (↑Z = {ρ ∈ Metric.closedBall (2 + t * Complex.I) (3 / 2) |
                  DirichletCharacter.LFunction χ ρ = 0}) ∧
          (∑ ρ ∈ Z, (analyticOrderNatAt (DirichletCharacter.LFunction χ) ρ : ℝ))
              ≤ C * Real.log ((q : ℝ) * (|t| + 2)) ∧
          ∀ s ∈ Metric.closedBall (2 + t * Complex.I) (7 / 5),
            DirichletCharacter.LFunction χ s ≠ 0 →
              ‖logDeriv (DirichletCharacter.LFunction χ) s
                  - ∑ ρ ∈ Z, (analyticOrderNatAt (DirichletCharacter.LFunction χ) ρ : ℂ) / (s - ρ)‖
                ≤ C * Real.log ((q : ℝ) * (|t| + 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; §16 (The number of zeros of L(s,χ)), pp. 101–104, eq. (4) and the displayed bound L′/L(s,χ) = Σ_{|γ−t|<1} 1/(s−ρ) + O(log q(|t|+2)) (p. 102, valid for −1 ≤ σ ≤ 2 and stated there for primitive χ), and the zero-count N(t+1,χ)−N(t−1,χ) ≪ log q(|t|+2) of eq. (2); cf. Montgomery–Vaughan, Multiplicative Number Theory I, Lemma 6.4 / Theorem 6.7 (Borel–Carathéodory route)

View graph

Local partial-fraction expansion of L′/L(s,χ)L'/L(s,\chi)L′/L(s,χ) with error O(log⁡q(∣t∣+2))O(\log q(|t|+2))O(logq(∣t∣+2)) (Davenport §16)

Local partial-fraction expansion of $L'/L(s,\chi)$ with error $O(\log q(|t|+2))$ (Davenport §16)