Conjugation symmetry of the von Mangoldt exponential sum

Proved

Vino.vmSum_neg

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

analytic-number-theorycircle-methodnumber-theoryprime-numbers

Since the weights $\Lambda(n)$ are real,

S(-\alpha,N)=\overline{S(\alpha,N)}.

In particular $|S(\alpha,N)|$ is even in $\alpha$ , so arcs may be treated in symmetric pairs, and the singular integral of the three primes problem inherits the same symmetry.

Preamble

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

Formal statement

namespace Vino

theorem vmSum_neg (α : ℝ) (N : ℕ) : vmSum (-α) N = (starRingEnd ℂ) (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