Major-arc expansion of the von Mangoldt exponential sum

Proved

Vino.vmSum_coprime_char_expansion

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

analytic-number-theorycircle-methoddirichlet-charactersnumber-theory

Let $q\ge1$ , let $b$ be coprime to $q$ , and let $N\ge0$ . Then

\varphi(q)\sum_{\substack{n<N\\ (n,q)=1}}\Lambda(n)\,e\!\left(\frac{bn}{q}\right)\;=\;\sum_{\chi\bmod q}\chi^{-1}(b)\,\tau(\chi)\,\psi(N,\chi^{-1}),

where $\tau(\chi)=\sum_{m<q}\chi(m)e(m/q)$ is the Gauss sum and $\psi(N,\chi)=\sum_{n<N}\Lambda(n)\chi(n)$ is the von Mangoldt sum twisted by $\chi$ .

This is the identity that governs the major arcs in the three primes theorem. It is exact — no approximation has been made — and it converts the behaviour of the prime-side generating function at a rational point $b/q$ into a weighted average of character sums. Estimating each $\psi(N,\chi)$ by the prime number theorem in arithmetic progressions, and evaluating the Gauss sums, is what produces the main term $\varphi(q)^{-1}\mu(q)N$ together with the singular series.

Preamble

import Definitions.Def_Vino_dirichlet
import Definitions.Def_Vino_primes
import Mathlib.NumberTheory.DirichletCharacter.Orthogonality
import Mathlib.Data.ZMod.Units
open Finset

Formal statement

namespace Vino

theorem vmSum_coprime_char_expansion (q : ℕ) [NeZero q] {b : ℕ} (hb : IsUnit ((b : ℕ) : ZMod q)) (N : ℕ) :
    (Nat.totient q : ℂ) * ∑ n ∈ (Finset.range N).filter (fun n => Nat.Coprime n q),
        ((ArithmeticFunction.vonMangoldt n : ℝ) : ℂ)
          * CircleMethod.e ((b : ℝ) / (q : ℝ) * (n : ℝ))
      = ∑ χ : DirichletCharacter ℂ q,
          χ⁻¹ ((b : ℕ) : ZMod q) * gaussE q χ * vmSumChar q χ⁻¹ 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, Section 3.1 (major arcs for the three primes theorem, expansion of the von Mangoldt exponential sum in Dirichlet characters); H. Davenport, Multiplicative Number Theory, 3rd ed., Springer GTM 74, 2000, Chapter 26.

View graph