Euler product for the three primes singular series

Proved

Vino.singSeries_euler_product

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

analytic-number-theorycircle-methodnumber-theorysingular-series

Let $s$ be a finite set of primes. Then

\sum_{T\subseteq s}A_{\prod_{p\in T}p}(n)\;=\;\prod_{p\in s}\mathfrak S_p(n),

where $A_q(n)=\mu(q)c_q(n)/\varphi(q)^3$ and $\mathfrak S_p(n)$ is the local density $1-(p-1)^{-2}$ for $p\mid n$ and $1+(p-1)^{-3}$ otherwise.

The left-hand side is the singular series of the three primes problem restricted to the moduli built from $s$ ; the right-hand side is the product of local densities. The statement is the finite, unconditional core of the Euler factorisation $\mathfrak S(n)=\prod_p\mathfrak S_p(n)$ , with no convergence issue to address.

Preamble

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

Formal statement

namespace Vino

theorem singSeries_euler_product {s : Finset ℕ} (hs : ∀ p ∈ s, Nat.Prime p) (n : ℤ) :
    ∑ T ∈ s.powerset, singTerm (∏ p ∈ T, p) n
      = ∏ p ∈ s, ((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