Prove2Me

A prime power meeting qq has its prime among those of qq

Proved
Vino.minFac_mem_primeFactors

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

analytic-number-theorycircle-methodnumber-theoryprime-numbers

Let q≥1q\ge1 and let n=pkn=p^{k} be a prime power that is not coprime to qq. Then

p=minFac(n) is a prime factor of q.p=\mathrm{minFac}(n)\ \text{is a prime factor of }q.

The von Mangoldt function is supported on prime powers, so this says that the only n<Nn<N contributing to ∑(n,q)>1Λ(n)\sum_{(n,q)>1}\Lambda(n) are the powers of the finitely many primes dividing qq. That observation is what makes the non-coprime part of the major-arc split negligible.

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 minFac_mem_primeFactors {q n : ℕ} (hq : 0 < q) (hn : IsPrimePow n) (h : ¬ Nat.Coprime n q) :
    n.minFac ∈ q.primeFactors := 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