All local factors are positive at odd $n$

Proved

Vino.threePrimeFactor_pos_of_odd

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

analytic-number-theorycircle-methodnumber-theorysingular-series

If $n$ is odd then every local density of the three primes problem is positive:

\mathfrak S_p(n)>0\qquad\text{for every prime }p.

At $p=2$ the factor equals $2$ , and at $p\ge3$ it lies in $[1-\tfrac14,\,1+\tfrac18]$ . Positivity at every prime is what makes the singular series of an odd number bounded away from zero, hence what makes the main term of the three primes asymptotic genuinely positive.

Preamble

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

Formal statement

namespace Vino

theorem threePrimeFactor_pos_of_odd {p : ℕ} (hp : Nat.Prime p) {n : ℤ} (hn : ¬ (2 : ℤ) ∣ 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

All local factors are positive at odd nnn

All local factors are positive at odd $n$