Estermann's lemma: $f(1) \ge \tfrac14(1-\sigma)M^{-3(1-\sigma)}$ when $\zeta f$ has nonnegative coefficients

Proved

Davenport.estermann_lemma

by alya · Sep 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

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

Estermann's lemma (Montgomery–Vaughan, Lemma 11.13). Suppose that $f(s)$ is analytic for $|s-2| \le 3/2$ and that $|f(s)| \le M$ for $s$ in this disc, where $M \ge 1$ . Suppose also that

F(s) = \zeta(s)f(s) = \sum_{n=1}^{\infty} r(n)\,n^{-s} \qquad (\sigma > 1),

the Dirichlet series being absolutely convergent for $\sigma > 1$ , that $r(1) = 1$ , and that $r(n) \ge 0$ for all $n$ . If there is a $\sigma \in [19/20, 1)$ such that $f(\sigma) \ge 0$ , then

f(1) \;\ge\; \tfrac14\,(1-\sigma)\,M^{-3(1-\sigma)} .

This is the analytic heart of Siegel's theorem. Applied with $f(s) = L(s,\chi)$ (when no real character has a real zero near $1$ ) or with $f(s) = L(s,\chi)L(s,\chi_1)L(s,\chi\chi_1)$ evaluated at a real zero $\beta_1$ of $L(s,\chi_1)$ , it produces the lower bound $L(1,\chi) \gg_\varepsilon q^{-\varepsilon}$ ; the ineffectivity of Siegel's constant comes entirely from the choice of $\chi_1$ , not from this lemma.

Formalization Note. The conditions " $f(\sigma) \ge 0$ " and the conclusion are stated for the real part of $f$ (in the applications $f$ is real on the real axis). The normalization $M \ge 1$ is harmless (replace $M$ by $\max(M,1)$ ) and is made explicit here; the Dirichlet series is Mathlib's LSeries, so its absolute convergence for $\operatorname{Re} s > 1$ is listed as a hypothesis, and $M^{-3(1-\sigma)}$ is the real power.

Preamble

import Mathlib.NumberTheory.LSeries.DirichletContinuation
import Mathlib.NumberTheory.LSeries.Nonvanishing
import Mathlib.NumberTheory.LSeries.Positivity
import Mathlib.NumberTheory.LSeries.Convolution
import Mathlib.NumberTheory.DirichletCharacter.Basic
import Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Pow.Complex
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.SpecialFunctions.Exp

open Finset DirichletCharacter

Formal statement

namespace Davenport

theorem estermann_lemma (f : ℂ → ℂ) (M : ℝ) (r : ℕ → ℝ) (hM : 1 ≤ M)
    (hf : DifferentiableOn ℂ f (Metric.closedBall (2 : ℂ) (3 / 2)))
    (hfM : ∀ s ∈ Metric.closedBall (2 : ℂ) (3 / 2), ‖f s‖ ≤ M)
    (hsum : ∀ s : ℂ, 1 < s.re → LSeriesSummable (fun n => (r n : ℂ)) s)
    (hF : ∀ s : ℂ, 1 < s.re → riemannZeta s * f s = LSeries (fun n => (r n : ℂ)) s)
    (hr₁ : r 1 = 1) (hr : ∀ n, 0 ≤ r n)
    (σ : ℝ) (hσ : 19 / 20 ≤ σ) (hσ₁ : σ < 1) (hfσ : 0 ≤ (f σ).re) :
    (1 / 4) * (1 - σ) * M ^ (-(3 * (1 - σ))) ≤ (f 1).re := by sorry

end Davenport

Source

H. L. Montgomery and R. C. Vaughan, Multiplicative Number Theory I: Classical Theory, Cambridge Studies in Advanced Mathematics 97, CUP 2007, Lemma 11.13 (Estermann), pp. 370–371, stated verbatim with the additional normalization M ≥ 1; cf. T. Estermann, On Dirichlet's L functions, J. London Math. Soc. 23 (1948), 275–279; 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, §21, pp. 126–131

View graph

Estermann's lemma: f(1)≥14(1−σ)M−3(1−σ)f(1) \ge \tfrac14(1-\sigma)M^{-3(1-\sigma)}f(1)≥41​(1−σ)M−3(1−σ) when ζf\zeta fζf has nonnegative coefficients

Estermann's lemma: $f(1) \ge \tfrac14(1-\sigma)M^{-3(1-\sigma)}$ when $\zeta f$ has nonnegative coefficients