The von Mangoldt exponential sum is $1$ -periodic in $\alpha$

Proved

Vino.vmSum_add_one

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

analytic-number-theorycircle-methodnumber-theoryprime-numbers

The generating function $S(\alpha,N)=\sum_{n<N}\Lambda(n)e(\alpha n)$ is a function on the circle: for all $\alpha$ and all $N$ ,

S(\alpha+1,N)=S(\alpha,N).

This is why the circle method integrates over a single period $[0,1]$ , and why the major and minor arcs may be described modulo $1$ .

Preamble

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

Formal statement

namespace Vino

theorem vmSum_add_one (α : ℝ) (N : ℕ) : vmSum (α + 1) N = vmSum α 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 von Mangoldt exponential sum is 111-periodic in α\alphaα

The von Mangoldt exponential sum is $1$ -periodic in $\alpha$