Recursion in the length of the von Mangoldt exponential sum

Proved

Vino.vmSum_succ

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

analytic-number-theorycircle-methodnumber-theoryprime-numbers

For every $\alpha\in\mathbb R$ and every $N\ge0$ ,

S(\alpha,N+1)\;=\;S(\alpha,N)+\Lambda(N)\,e(\alpha N),

where $S(\alpha,N)=\sum_{n<N}\Lambda(n)e(\alpha n)$ .

Together with $S(\alpha,0)=0$ this characterises the sum recursively, which is the form induction arguments on $N$ actually consume.

Preamble

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

Formal statement

namespace Vino

theorem vmSum_succ (α : ℝ) (N : ℕ) :
    vmSum α (N + 1)
      = vmSum α N
        + ((ArithmeticFunction.vonMangoldt N : ℝ) : ℂ) * CircleMethod.e (α * (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