Choosing the height in the de la Vallée Poussin argument

Proved

Weil.perron_parameter_choice

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

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

The parameter choice. Let $K_1,K_2,c'>0$ . There are constants $c_1,c_2,C>0$ , depending only on $K_1$ , $K_2$ and $c'$ , such that for every $q\ge1$ and every integer $N\ge2$ with $q\le\exp(c_2\sqrt{\log N})$ there is a height $T_0\ge2$ satisfying

K_1\Bigl(\frac{N\log^{2}N}{T_0}+\log N\Bigr)+K_2\Bigl(N^{\,1-c'/\log(qT_0)}\log^{3}(qT_0)+\frac{N\log^{2}(qT_0)}{T_0}\Bigr)\;\le\;C\,N\exp\bigl(-c_1\sqrt{\log N}\bigr).

This is the calculus step of the argument, isolated from the complex analysis. Given the two error terms produced by the truncated Perron formula and by the contour shift, it exhibits a height at which their sum is small, and shows that the resulting saving over the trivial bound is $\exp(-c_1\sqrt{\log N})$ .

The choice is $T_0=\exp(\sqrt{\log N})$ . With it $\log(qT_0)\le(1+c_2)\sqrt{\log N}$ , so the shifted abscissa gives

N^{\,1-c'/\log(qT_0)}\;\le\;N\exp\Bigl(-\frac{c'}{1+c_2}\sqrt{\log N}\Bigr),

and the terms carrying $1/T_0$ contribute $N\log^{2}N\,e^{-\sqrt{\log N}}$ ; the polynomial factors $\log^{3}(qT_0)$ and $\log^{2}N$ are absorbed by shrinking $c_1$ .

The hypothesis $q\le\exp(c_2\sqrt{\log N})$ is exactly what prevents the modulus from eating the saving, and it is the reason the Siegel-Walfisz theorem is uniform only for moduli up to a fixed power of $\log N$ .

No complex analysis enters: this is a statement about real functions of $N$ and $q$ .

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_parameter_choice (K₁ K₂ c' : ℝ) (hK₁ : 0 < K₁) (hK₂ : 0 < K₂) (hc' : 0 < c') :
    ∃ c₁ c₂ C : ℝ, 0 < c₁ ∧ 0 < c₂ ∧ 0 < C ∧
      ∀ (q N : ℕ), 1 ≤ q → 2 ≤ N → (q : ℝ) ≤ Real.exp (c₂ * Real.sqrt (Real.log N)) →
        ∃ T₀ : ℝ, 2 ≤ T₀ ∧
          K₁ * ((N : ℝ) * Real.log N ^ 2 / T₀ + Real.log N)
            + K₂ * ((N : ℝ) ^ (1 - c' / Real.log ((q : ℝ) * T₀))
                        * Real.log ((q : ℝ) * T₀) ^ 3
                      + (N : ℝ) * Real.log ((q : ℝ) * T₀) ^ 2 / T₀)
            ≤ C * N * Real.exp (-c₁ * Real.sqrt (Real.log N)) := 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