The exponential sum at the origin is $\psi(N)$

Proved

Vino.vmSum_zero_freq

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

analytic-number-theorycircle-methodnumber-theoryprime-numbers

At frequency zero the prime-side generating function degenerates to Chebyshev's function:

S(0,N)=\sum_{n<N}\Lambda(n)=\psi(N).

This identifies the value that the major arc around $0$ has to reproduce, and it is the normalisation against which every cancellation estimate is measured.

Preamble

import Definitions.Def_Vino_primes
import Mathlib.Analysis.SpecialFunctions.Log.Basic
open Finset

Formal statement

namespace Vino

theorem vmSum_zero_freq (N : ℕ) : vmSum 0 N = (psi N : ℂ) := by sorry

end Vino

Source

R. C. Vaughan, The Hardy-Littlewood Method, 2nd ed., Cambridge Tracts in Mathematics 125, Cambridge University Press, 1997, Chapter 3 (the three primes theorem).

View graph

The exponential sum at the origin is ψ(N)\psi(N)ψ(N)

The exponential sum at the origin is $\psi(N)$