Each prime contributes at most $\log N$ to $\psi$

Proved

Vino.sum_vonMangoldt_minFac_le

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

analytic-number-theorycircle-methodnumber-theoryprime-numbers

For a prime $p$ and $N\ge1$ ,

\sum_{\substack{n<N\\ n\ \text{a power of }p}}\Lambda(n)\;\le\;\log N,

uniformly in $p$ . Indeed the sum is $(\#\{k\ge1:p^{k}<N\})\log p\le\log_p N\cdot\log p=\log\!\left(p^{\lfloor\log_p N\rfloor}\right)\le\log N$ .

This is the per-prime input to the bound on the non-coprime part of the major-arc split: summing over the $\omega(q)$ primes dividing $q$ gives $O(\omega(q)\log N)$ .

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_minFac_le {p N : ℕ} (hp : p.Prime) (hN : N ≠ 0) :
    ∑ n ∈ (Finset.range N).filter (fun n => IsPrimePow n ∧ n.minFac = p),
        (ArithmeticFunction.vonMangoldt n : ℝ) ≤ 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

Each prime contributes at most log⁡N\log NlogN to ψ\psiψ

Each prime contributes at most $\log N$ to $\psi$