The smoothed sum $\sum a(n)\widetilde{1_\varepsilon}(n/N)$ is within $O(\varepsilon N\log N)$ of $\sum_{n<N}a(n)$

Proved

Davenport.perron_smoothed_close

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

analytic-number-theorycontour-integrationmellin-transformnumber-theoryprime-number-theoremsiegel-walfisz

Throughout, $\nu$ is a fixed smoothing kernel: a $C^1$ function on $\mathbb R$ supported in $[1/2,2]$ , nonnegative on $(0,\infty)$ , with $\int_0^\infty\nu(x)\,dx/x=1$ ; $\widetilde{1_\varepsilon}=$ Smooth1 ν ε is the smoothed indicator of $(0,1]$ obtained by Mellin convolution with the delta-spike $\nu(x^{1/\varepsilon})/\varepsilon$ (it equals $1$ on $(0,1-\varepsilon\log2]$ , $0$ on $[1+2\varepsilon\log 2,\infty)$ , and lies in $[0,1]$ ), and $\mathcal M\widetilde{1_\varepsilon}(s)=\int_0^\infty\widetilde{1_\varepsilon}(x)x^{s-1}dx$ is its Mellin transform (Mathlib's mellin).

Statement. There is a constant $C>0$ (depending only on $\nu$ ) such that for all coefficients $a(n)$ with $|a(n)|\le\Lambda(n)$ , all integers $N>3$ and all $0<\varepsilon<1$ with $N\varepsilon>2$ ,

\Bigl|\sum_{n\ge1}a(n)\,\widetilde{1_\varepsilon}\Bigl(\frac nN\Bigr)-\sum_{n<N}a(n)\Bigr|\;\le\;C\,\varepsilon N\log N .

Indeed $\widetilde{1_\varepsilon}(n/N)$ differs from the sharp indicator of $n<N$ only for $n$ in a window $|n-N|\ll\varepsilon N$ (plus $n=N$ ), where $|a(n)|\le\Lambda(n)\le\log(2N)$ , and the window contains $O(\varepsilon N)$ integers. This is the price of smoothing in the contour method; with $\varepsilon=\exp(-c\sqrt{\log N})$ it is absorbed in the de la Vallée Poussin error term.

Formalization Note. The left sum is a tsum over $n\in\mathbb N$ , the right one is over Finset.range N, i.e. $0\le n<N$ .

Preamble

import Definitions.Def_MellinCalculus_defs
import Definitions.Def_ResidueCalcOnRectangles_defs
import Mathlib.NumberTheory.LSeries.Basic
import Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
import Mathlib.Analysis.MellinTransform
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Pow.Complex
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

open Set MeasureTheory

Formal statement

namespace Davenport

theorem perron_smoothed_close {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν)
    (suppν : ν.support ⊆ Icc (1 / 2) 2) (νnonneg : ∀ x > 0, 0 ≤ ν x)
    (mass_one : ∫ x in Ioi (0 : ℝ), ν x / x = 1) :
    ∃ C : ℝ, 0 < C ∧
      ∀ (a : ℕ → ℂ), (∀ n : ℕ, ‖a n‖ ≤ ArithmeticFunction.vonMangoldt n) →
        ∀ (N : ℕ), 3 < (N : ℝ) → ∀ ε : ℝ, 0 < ε → ε < 1 → 2 < N * ε →
          ‖(∑' n : ℕ, a n * (Smooth1 ν ε (n / N) : ℂ)) - ∑ n ∈ Finset.range N, a n‖
            ≤ C * ε * N * Real.log N := by sorry

end Davenport

Source

PrimeNumberTheoremAnd project (A. Kontorovich, T. Tao et al.), https://github.com/AlexKontorovich/PrimeNumberTheoremAnd, file PrimeNumberTheoremAnd/MediumPNT.lean, theorem `SmoothedChebyshevClose` (platform theorem of the same name, for a(n) = Λ(n)); the elementary input is Λ(n) ≤ log n, 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; §17 eq. (1)

View graph

The smoothed sum ∑a(n)1ε~(n/N)\sum a(n)\widetilde{1_\varepsilon}(n/N)∑a(n)1ε​​(n/N) is within O(εNlog⁡N)O(\varepsilon N\log N)O(εNlogN) of ∑n<Na(n)\sum_{n<N}a(n)∑n<N​a(n)

The smoothed sum $\sum a(n)\widetilde{1_\varepsilon}(n/N)$ is within $O(\varepsilon N\log N)$ of $\sum_{n<N}a(n)$