A character-twisted von Mangoldt sum is supported on reduced residues

Proved

Vino.vmSumChar_eq_sum_coprime

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

analytic-number-theorycircle-methoddirichlet-charactersnumber-theory

For a Dirichlet character $\chi$ modulo $q$ ,

\psi(N,\chi)\;=\;\sum_{n<N}\Lambda(n)\chi(n)\;=\;\sum_{\substack{n<N\\ (n,q)=1}}\Lambda(n)\chi(n).

A Dirichlet character vanishes on residues that are not units, so the twisted sum automatically discards the $n$ sharing a factor with $q$ . The identity is what lets one pass freely between the twisted sum and the sum restricted to reduced residues in the major-arc expansion.

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 vmSumChar_eq_sum_coprime (q : ℕ) (χ : DirichletCharacter ℂ q) (N : ℕ) :
    vmSumChar q χ N
      = ∑ n ∈ (Finset.range N).filter (fun n => Nat.Coprime n q),
          ((ArithmeticFunction.vonMangoldt n : ℝ) : ℂ) * χ ((n : ℕ) : ZMod q) := 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