The truncated singular series factors over the primes

Proved

Vino.singSeriesDvd_eq_prod

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

analytic-number-theorycircle-methodnumber-theorysingular-series

For a squarefree modulus $Q$ and every integer $n$ ,

\mathfrak S_Q(n)\;:=\;\sum_{q\mid Q}\frac{\mu(q)\,c_q(n)}{\varphi(q)^3}\;=\;\prod_{p\mid Q}\mathfrak S_p(n),

with $\mathfrak S_p(n)=1-(p-1)^{-2}$ if $p\mid n$ and $1+(p-1)^{-3}$ otherwise.

This is the Euler product of the three primes singular series in the form actually used on the major arcs: the sum over moduli up to a truncation point is replaced by a product of explicit local densities, whose size and sign can then be read off directly.

Preamble

import Definitions.Def_Vino_ramanujan
import Mathlib.Data.Nat.Totient
import Mathlib.Algebra.BigOperators.Ring.Finset
open Finset

Formal statement

namespace Vino

theorem singSeriesDvd_eq_prod {Q : ℕ} (hQ : Squarefree Q) (n : ℤ) :
    singSeriesDvd Q n = ∏ p ∈ Q.primeFactors, ((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