Shifting the Perron contour into the zero-free region

Proved

Weil.perron_contour_shift

by tabbott · Sep 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analytic-number-theorynumber-theoryperron-formulaprime-number-theorem

The contour shift. Fix a region constant $c>0$ and a bound constant $C_0>0$ . There are constants $c'>0$ and $K>0$ , depending only on $c$ and $C_0$ , such that the following holds for every modulus $q\ge1$ , every $G:\mathbb{C}\to\mathbb{C}$ , every finite set $P\subset\mathbb{C}$ of poles and every assignment $r$ of residues satisfying:

$G$ is analytic in a neighbourhood of each point of $\{s:\ \operatorname{Re}s\ge1-c/\log(q(|\operatorname{Im}s|+2)),\ \operatorname{Re}s\ge3/4\}\setminus P$ ;
every $p\in P$ satisfies $1/2\le\operatorname{Re}p\le1$ ;
$\sum_{p\in P}|r(p)|\le C_0\log(2q)$ ;
on that same region, off $P$ ,

\Bigl|G(s)-\sum_{p\in P}\frac{r(p)}{s-p}\Bigr|\;\le\;C_0\log^{2}\bigl(q(|\operatorname{Im}s|+2)\bigr).

Then for every integer $N\ge2$ and every $T_0\ge2$ there exists a height $T\in[T_0,2T_0]$ with

\Bigl|\frac{1}{2\pi i}\int_{\sigma_0-iT}^{\sigma_0+iT}G(s)\frac{N^{s}}{s}\,ds\;-\;\sum_{p\in P}r(p)\frac{N^{p}}{p}\Bigr|\;\le\;K\Bigl(N^{\,1-c'/\log(qT_0)}\log^{3}(qT_0)+\frac{N\log^{2}(qT_0)}{T_0}\Bigr),

where $\sigma_0=1+1/\log N$ .

This is the analytic heart of the de la Vallée Poussin argument. The vertical line at $\sigma_0$ is moved left to $\sigma_1=1-c'/\log(qT_0)$ , which lies inside the region for $|t|\le T$ once $c'$ is small enough in terms of $c$ ; the residues $r(p)N^{p}/p$ are what the shift releases, and the three remaining sides of the rectangle are estimated by hypothesis 4.

Two features of the statement are deliberate rather than incidental. First, the height $T$ is quantified existentially inside a dyadic window rather than prescribed: the horizontal sides of the contour must avoid the ordinates of the poles, and a suitable $T$ is produced by averaging over the window, the singularity $\log(1/|T-\operatorname{Im}p|)$ being integrable. A version of this statement holding for every $T\ge T_0$ would be false, since a pole may sit on the contour. Second, poles lying outside the shifted rectangle — to the left of $\sigma_1$ , or above height $T$ — are not released by the shift; their total contribution to $\sum_{p}r(p)N^{p}/p$ is nevertheless inside the stated error, by hypotheses 2 and 3.

Context. The theorem this lemma was introduced to decompose, Davenport.perron_of_region_bound, was proved independently — via the smoothed Perron route (Davenport.perron_smoothed_eq_integral and its siblings), which replaces the sharp cutoff by a smooth weight and so avoids the truncation error entirely. The statement here belongs to the classical sharp-cutoff route of Davenport Sections 17-18 and is left standing as a self-contained, reusable statement in its own right; it is not on the critical path of any current mission.

Preamble

import Definitions.Def_Weil_perron
import Definitions.Def_Davenport_siegelWalfisz
import Mathlib.NumberTheory.LSeries.Basic
import Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
import Mathlib.Analysis.Analytic.Order
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.SpecialFunctions.Exp
import Mathlib.Analysis.SpecialFunctions.Sqrt

set_option autoImplicit false

open Finset

Formal statement

namespace Weil
theorem perron_contour_shift (c C₀ : ℝ) (hc : 0 < c) (hC₀ : 0 < C₀) :
    ∃ c' K : ℝ, 0 < c' ∧ 0 < K ∧
      ∀ (q : ℕ) [NeZero q] (G : ℂ → ℂ) (P : Finset ℂ) (r : ℂ → ℂ),
        AnalyticOnNhd ℂ G ({s : ℂ | Davenport.InRegion c q s ∧ 3 / 4 ≤ s.re} \ ↑P) →
        (∀ p ∈ P, 1 / 2 ≤ p.re ∧ p.re ≤ 1) →
        (∑ p ∈ P, ‖r p‖) ≤ C₀ * Real.log (2 * q) →
        (∀ s : ℂ, Davenport.InRegion c q s → 3 / 4 ≤ s.re → s ∉ P →
            ‖G s - ∑ p ∈ P, r p / (s - p)‖ ≤ C₀ * Real.log ((q : ℝ) * (|s.im| + 2)) ^ 2) →
        ∀ N : ℕ, 2 ≤ N → ∀ T₀ : ℝ, 2 ≤ T₀ →
          ∃ T : ℝ, T₀ ≤ T ∧ T ≤ 2 * T₀ ∧
            ‖perronIntegral G N (1 + 1 / Real.log N) T - ∑ p ∈ P, r p * (N : ℂ) ^ p / p‖
              ≤ K * ((N : ℝ) ^ (1 - c' / Real.log ((q : ℝ) * T₀))
                        * Real.log ((q : ℝ) * T₀) ^ 3
                      + (N : ℝ) * Real.log ((q : ℝ) * T₀) ^ 2 / T₀) := by sorry
end Weil

Source

H. Davenport, Multiplicative Number Theory, 3rd ed. (rev. H. L. Montgomery), GTM 74, Springer 2000, Section 18 (pp. 111-114, the contour-shift argument for psi(x)) and Sections 19-20 (pp. 115-125, the same argument for psi(x, chi) with the exceptional-zero residue); cf. Montgomery-Vaughan, Multiplicative Number Theory I, Theorem 6.9 and Theorem 11.16

View graph