The truncated Perron integral $\frac{1}{2\pi i}\int_{\sigma-iT}^{\sigma+iT}G(s)\,x^{s}\,\frac{ds}{s}$

Definition

Weil_perron

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

analytic-number-theorynumber-theoryperron-formula

The vertical contour integral at the heart of Perron's formula. For a function $G$ on $\mathbb{C}$ , a real $x>0$ , an abscissa $\sigma$ and a height $T>0$ ,

\operatorname{perronIntegral}(G,x,\sigma,T)\;=\;\frac{1}{2\pi i}\int_{\sigma-iT}^{\sigma+iT}G(s)\,\frac{x^{s}}{s}\,ds.

It is written here as an integral in the real variable $t$ along the line $s=\sigma+it$ : with $ds=i\,dt$ the factor $i$ cancels against the $i$ in $1/2\pi i$ , leaving

\frac{1}{2\pi}\int_{-T}^{T}G(\sigma+it)\,\frac{x^{\sigma+it}}{\sigma+it}\,dt.

No hypotheses are imposed on $G$ or on the parameters. Where the integrand fails to be interval integrable the Bochner integral is $0$ by convention, so any statement about this quantity carries its own analyticity or integrability hypotheses.

Perron's formula says that for $\sigma$ to the right of the abscissa of absolute convergence this integral approximates the partial sum $\sum_{n<x}a(n)$ of the Dirichlet series $G(s)=\sum_{n\ge1}a(n)n^{-s}$ , with an error that decreases in $T$ . Moving the line of integration to the left of $\sigma=1$ and collecting the residues released by the shift is what converts a zero-free region for $G$ into an asymptotic formula for that partial sum.

Definition code

/-
# The truncated Perron integral

The vertical contour integral that carries the analytic content of the Perron formula,
`(1 / 2πi) ∫_{σ - iT}^{σ + iT} G(s) x^s / s ds`, parametrised by the real variable
`t` with `s = σ + it`, so that `ds = i dt` and the factor `i` cancels the `i` in `1/2πi`.
-/
import Mathlib.Analysis.SpecialFunctions.Pow.Complex
import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

namespace Weil

/-- `perronIntegral G x σ T` is the truncated Perron integral
`(1 / 2πi) ∫_{σ - iT}^{σ + iT} G(s) · x ^ s / s ds`,
written as an integral in the real variable `t` along `s = σ + it`. -/
noncomputable def perronIntegral (G : ℂ → ℂ) (x σ T : ℝ) : ℂ :=
  (1 / (2 * Real.pi)) *
    ∫ t in (-T)..T,
      G ((σ : ℂ) + (t : ℂ) * Complex.I) * (x : ℂ) ^ ((σ : ℂ) + (t : ℂ) * Complex.I)
        / ((σ : ℂ) + (t : ℂ) * Complex.I)

end Weil

Source

H. Davenport, Multiplicative Number Theory, 3rd ed. (rev. H. L. Montgomery), GTM 74, Springer 2000, Section 17 (The truncated Perron formula, pp. 105-110); cf. Montgomery-Vaughan, Multiplicative Number Theory I, Theorem 5.2

View graph

The truncated Perron integral 12πi∫σ−iTσ+iTG(s) xs dss\frac{1}{2\pi i}\int_{\sigma-iT}^{\sigma+iT}G(s)\,x^{s}\,\frac{ds}{s}2πi1​∫σ−iTσ+iT​G(s)xssds​

The truncated Perron integral $\frac{1}{2\pi i}\int_{\sigma-iT}^{\sigma+iT}G(s)\,x^{s}\,\frac{ds}{s}$