The singular series term at a squarefree modulus

Proved

Vino.singTerm_prod_primes

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 and $Q=\prod_{p\in s}p$ . Then

A_Q(n)=\prod_{p\in s}A_p(n),\qquad A_q(n)=\frac{\mu(q)c_q(n)}{\varphi(q)^3}.

Distinct primes are coprime, so the multiplicativity of $A$ propagates through the whole squarefree modulus. This is the form in which multiplicativity is consumed by the Euler product.

Preamble

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

Formal statement

namespace Vino

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