Recursion for the character-twisted von Mangoldt sum

Proved

Vino.vmSumChar_succ

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

analytic-number-theorycircle-methoddirichlet-charactersnumber-theory

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

\psi(N+1,\chi)=\psi(N,\chi)+\Lambda(N)\chi(N),

where $\psi(N,\chi)=\sum_{n<N}\Lambda(n)\chi(n)$ . Together with $\psi(0,\chi)=0$ this characterises the twisted sum recursively, which is the form partial summation and induction arguments consume.

Preamble

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

Formal statement

namespace Vino

theorem vmSumChar_succ (q : ℕ) (χ : DirichletCharacter ℂ q) (N : ℕ) :
    vmSumChar q χ (N + 1)
      = vmSumChar q χ N
        + ((ArithmeticFunction.vonMangoldt N : ℝ) : ℂ) * χ ((N : ℕ) : ZMod q) := 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