Counting the powers of a fixed prime below $N$

Proved

Vino.card_primePow_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$ , the number of powers of $p$ below $N$ is at most $\lfloor\log_p N\rfloor$ :

\#\{n<N: n=p^{k}\ \text{for some }k\ge1\}\;\le\;\log_p N.

Combined with $\Lambda(p^{k})=\log p$ this gives $\sum_{p^{k}<N}\Lambda(p^{k})\le\log N$ — the statement that each individual prime contributes at most $\log N$ to Chebyshev's function, uniformly in $p$ .

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 card_primePow_minFac_le {p N : ℕ} (hp : p.Prime) (hN : N ≠ 0) :
    ((Finset.range N).filter (fun n => IsPrimePow n ∧ n.minFac = p)).card
      ≤ Nat.log p 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

Counting the powers of a fixed prime below NNN

Counting the powers of a fixed prime below $N$