Splitting the von Mangoldt exponential sum at a modulus

Proved

Vino.vmSum_split_coprime

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

analytic-number-theorycircle-methoddirichlet-charactersnumber-theory

For every modulus $q$ , every $\alpha$ and every $N$ ,

S(\alpha,N)=\sum_{\substack{n<N\\ (n,q)=1}}\Lambda(n)e(\alpha n)\;+\;\sum_{\substack{n<N\\ (n,q)>1}}\Lambda(n)e(\alpha n).

On a major arc around $b/q$ only the first sum is expanded in Dirichlet characters; the second is an error term supported on the powers of the primes dividing $q$ , and is negligible. Recording the split explicitly keeps the character expansion an exact identity rather than an approximation.

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_split_coprime (q : ℕ) (α : ℝ) (N : ℕ) :
    vmSum α N
      = (∑ n ∈ (Finset.range N).filter (fun n => Nat.Coprime n q),
            ((ArithmeticFunction.vonMangoldt n : ℝ) : ℂ) * CircleMethod.e (α * (n : ℝ)))
        + ∑ n ∈ (Finset.range N).filter (fun n => ¬ Nat.Coprime n q),
            ((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, 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