Imprimitive-to-primitive reduction: $|\psi(N,\chi)-\psi(N,\chi^*)|\le\omega(q)\log N$

Proved

Davenport.vmSumChar_sub_primitive_le

by alya · Sep 3, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analytic-number-theorydirichlet-l-functionnumber-theorysiegel-walfisz

Reduction of $\psi(N,\chi)$ to the primitive character (Davenport §19). Let $\chi$ be a Dirichlet character modulo $q\ge1$ and let $\chi^*$ be the primitive character modulo the conductor $q^*\mid q$ that induces it (Mathlib's primitiveCharacter). With $\psi(N,\chi)=\sum_{n<N}\Lambda(n)\chi(n)$ ,

\bigl|\psi(N,\chi)-\psi(N,\chi^*)\bigr|\;\le\;\omega(q)\,\log N,

where $\omega(q)$ is the number of distinct prime factors of $q$ . Indeed $\chi(n)=\chi^*(n)$ unless $\gcd(n,q)>1$ , in which case $\chi(n)=0$ ; the terms that differ are the prime powers $p^k<N$ with $p\mid q$ , and for each such $p$ they contribute at most $\sum_{k:\,p^k<N}\log p\le\log N$ . This is the elementary step that lets the explicit formula and the zero-free region, which are stated for primitive characters, be applied to arbitrary characters in the §20 estimate; note $\omega(q)\log N\le(\log q)(\log N)/\log 2$ .

Preamble

import Definitions.Def_Davenport_siegelWalfisz
import Mathlib.NumberTheory.LSeries.DirichletContinuation
import Mathlib.NumberTheory.DirichletCharacter.Basic
import Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
import Mathlib.NumberTheory.Chebyshev
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Pow.Complex
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.SpecialFunctions.Exp
import Mathlib.Analysis.SpecialFunctions.Sqrt
import Mathlib.Algebra.BigOperators.Finprod
import Mathlib.Data.Nat.Totient
import Mathlib.NumberTheory.EulerProduct.DirichletLSeries

open Finset DirichletCharacter Vino

Formal statement

namespace Davenport

theorem vmSumChar_sub_primitive_le (q : ℕ) [NeZero q] (χ : DirichletCharacter ℂ q) (N : ℕ) :
    ‖vmSumChar q χ N - vmSumChar χ.conductor χ.primitiveCharacter N‖
      ≤ (q.primeFactors.card : ℝ) * Real.log N := by sorry

end Davenport

Source

H. Davenport, Multiplicative Number Theory, 3rd ed. (revised by H. L. Montgomery), GTM 74, Springer, 2000, https://doi.org/10.1007/978-1-4757-5927-3; §19 (The explicit formula for ψ(x,χ)), pp. 115–120: the remark ψ(x,χ) = ψ(x,χ*) + O((log q)(log x)) for an imprimitive character χ induced by χ*

Human review

Endorsed by Shuze Chen · Sep 3, 2026
Endorsed by alya · Sep 3, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Imprimitive-to-primitive reduction: ∣ψ(N,χ)−ψ(N,χ∗)∣≤ω(q)log⁡N|\psi(N,\chi)-\psi(N,\chi^*)|\le\omega(q)\log N∣ψ(N,χ)−ψ(N,χ∗)∣≤ω(q)logN

Imprimitive-to-primitive reduction: $|\psi(N,\chi)-\psi(N,\chi^*)|\le\omega(q)\log N$