Empty von Mangoldt exponential sum

Proved

Vino.vmSum_zero_len

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

analytic-number-theorycircle-methodnumber-theoryprime-numbers

Write $\Lambda$ for the von Mangoldt function and $e(\theta)=\exp(2\pi i\theta)$ , and let

S(\alpha,N)\;=\;\sum_{n<N}\Lambda(n)\,e(\alpha n)

be the prime-side generating function of the circle method. The sum over the empty range vanishes:

S(\alpha,0)=0.

This is the base case of the recursion in $N$ that underlies every induction on the length of the sum.

Preamble

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

Formal statement

namespace Vino

theorem vmSum_zero_len (α : ℝ) : vmSum α 0 = 0 := 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