The $3$ - $4$ - $1$ inequality for $-L'/L$ (Davenport §14)

Proved

Davenport.logDeriv_three_four_one

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

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

The 3–4–1 inequality for logarithmic derivatives (Davenport §14, the device of §13 applied to $L$ -functions). For every modulus $q\ge1$ , every Dirichlet character $\chi$ modulo $q$ , every real $\sigma>1$ and every real $t$ ,

3\,\operatorname{Re}\Bigl(-\frac{L'}{L}(\sigma,\chi_0)\Bigr)+4\,\operatorname{Re}\Bigl(-\frac{L'}{L}(\sigma+it,\chi)\Bigr)+\operatorname{Re}\Bigl(-\frac{L'}{L}(\sigma+2it,\chi^2)\Bigr)\;\ge\;0,

where $\chi_0$ is the principal character modulo $q$ . Since $-L'/L(s,\psi)=\sum_n\Lambda(n)\psi(n)n^{-s}$ for $\operatorname{Re}s>1$ , the left side equals $\sum_n\Lambda(n)n^{-\sigma}\bigl(3+4\cos\theta_n+\cos2\theta_n\bigr)$ over $n$ coprime to $q$ , with $\chi(n)n^{-it}=e^{i\theta_n}$ , and $3+4\cos\theta+\cos2\theta=2(1+\cos\theta)^2\ge0$ . This is the starting point of the zero-free region for $L(s,\chi)$ .

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 logDeriv_three_four_one (q : ℕ) [NeZero q] (χ : DirichletCharacter ℂ q) (σ t : ℝ)
    (hσ : 1 < σ) :
    0 ≤ 3 * (-(deriv (DirichletCharacter.LFunction (1 : DirichletCharacter ℂ q)) (σ : ℂ)
              / DirichletCharacter.LFunction (1 : DirichletCharacter ℂ q) (σ : ℂ))).re
        + 4 * (-(deriv (DirichletCharacter.LFunction χ) (σ + t * Complex.I)
              / DirichletCharacter.LFunction χ (σ + t * Complex.I))).re
        + (-(deriv (DirichletCharacter.LFunction (χ ^ 2)) (σ + 2 * t * Complex.I)
              / DirichletCharacter.LFunction (χ ^ 2) (σ + 2 * t * Complex.I))).re := 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 3(−L'/L)(σ,χ₀) + 4 Re(−L'/L)(σ+it,χ) + Re(−L'/L)(σ+2it,χ²) ≥ 0 for σ > 1, from 3 + 4 cos θ + cos 2θ ≥ 0 (cf. §13 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

The 333-444-111 inequality for −L′/L-L'/L−L′/L (Davenport §14)

The $3$ - $4$ - $1$ inequality for $-L'/L$ (Davenport §14)