Positivity of the local factors at odd primes

Proved

Vino.threePrimeFactor_pos

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

analytic-number-theorycircle-methodnumber-theorysingular-series

For every $p\ge3$ and every integer $n$ ,

\mathfrak S_p(n)>0 .

Indeed if $p\mid n$ the factor is $1-(p-1)^{-2}\ge 1-\tfrac14>0$ because $p-1\ge2$ , and if $p\nmid n$ it is $1+(p-1)^{-3}>1$ . So $p=2$ is the only prime at which the singular series of the three primes problem can vanish.

Preamble

import Definitions.Def_Vino_ramanujan
import Mathlib.Data.Nat.Totient
open Finset

Formal statement

namespace Vino

theorem threePrimeFactor_pos {p : ℕ} (hp : 3 ≤ p) (n : ℤ) : 0 < threePrimeFactor 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, Section 3.2 (the singular series of the three primes theorem); I. M. Vinogradov, Representation of an odd number as a sum of three primes, Doklady Akademii Nauk SSSR 15 (1937), 291-294.

View graph