The von Mangoldt exponential sum at a rational point

Proved

Vino.vmSum_rat_char_expansion

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

analytic-number-theorycircle-methoddirichlet-charactersnumber-theory

Let $q\ge1$ and let $b$ be coprime to $q$ . Then, with $S(\alpha,N)=\sum_{n<N}\Lambda(n)e(\alpha n)$ ,

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

This is the exact major-arc identity in the form it is actually used. The first term is the main term: evaluating the Gauss sums and estimating each $\psi(N,\chi^{-1})$ by the prime number theorem in arithmetic progressions produces $\mu(q)\varphi(q)^{-1}N$ plus an error. The second term is supported on the powers of the primes dividing $q$ and is $O(\omega(q)\log N)$ , hence negligible.

No approximation has been made: the identity holds for every $N$ and every reduced fraction $b/q$ .

Preamble

import Definitions.Def_Vino_dirichlet
import Definitions.Def_Vino_primes
import Mathlib.NumberTheory.DirichletCharacter.Orthogonality
open Finset

Formal statement

namespace Vino

theorem vmSum_rat_char_expansion (q : ℕ) [NeZero q] {b : ℕ} (hb : IsUnit ((b : ℕ) : ZMod q)) (N : ℕ) :
    (Nat.totient q : ℂ) * vmSum ((b : ℝ) / (q : ℝ)) N
      = (∑ χ : DirichletCharacter ℂ q,
            χ⁻¹ ((b : ℕ) : ZMod q) * gaussE q χ * vmSumChar q χ⁻¹ N)
        + (Nat.totient q : ℂ)
            * ∑ n ∈ (Finset.range N).filter (fun n => ¬ Nat.Coprime n q),
                ((ArithmeticFunction.vonMangoldt n : ℝ) : ℂ)
                  * CircleMethod.e ((b : ℝ) / (q : ℝ) * (n : ℝ)) := by sorry

end Vino

Source

H. Davenport, Multiplicative Number Theory, 3rd ed., Springer GTM 74, 2000, Chapters 9 and 26; R. C. Vaughan, The Hardy-Littlewood Method, 2nd ed., Cambridge Tracts in Mathematics 125, Cambridge University Press, 1997, Chapter 3, Section 3.1.

View graph