The non-coprime part of $\psi$ is $O(\omega(q)\log N)$

Proved

Vino.sum_vonMangoldt_not_coprime_le

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

analytic-number-theorycircle-methodnumber-theoryprime-numbers

Let $q\ge1$ and $N\ge1$ . Then

\sum_{\substack{n<N\\ (n,q)>1}}\Lambda(n)\;\le\;\omega(q)\log N,

where $\omega(q)$ is the number of distinct prime factors of $q$ .

This is the estimate that disposes of the error term in the major-arc identity. Only prime powers contribute to a von Mangoldt sum, and a prime power sharing a factor with $q$ must be a power of one of the $\omega(q)$ primes dividing $q$ ; each such prime contributes at most $\log N$ . Since $\omega(q)\ll\log q/\log\log q$ , the whole term is $O(\log q\log N)$ — negligible against the main term $\varphi(q)^{-1}N$ on any reasonable major arc.

Preamble

import Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
import Mathlib.Data.Nat.Factorization.PrimePow
import Mathlib.Data.Nat.Log
import Mathlib.Analysis.SpecialFunctions.Log.Basic
open Finset

Formal statement

namespace Vino

theorem sum_vonMangoldt_not_coprime_le {q : ℕ} (hq : 0 < q) {N : ℕ} (hN : N ≠ 0) :
    ∑ n ∈ (Finset.range N).filter (fun n => ¬ Nat.Coprime n q),
        (ArithmeticFunction.vonMangoldt n : ℝ)
      ≤ (q.primeFactors.card : ℝ) * Real.log 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, Sections 3.1-3.2 (the three primes theorem).

View graph

The non-coprime part of ψ\psiψ is O(ω(q)log⁡N)O(\omega(q)\log N)O(ω(q)logN)

The non-coprime part of $\psi$ is $O(\omega(q)\log N)$