The terms of the singular series are multiplicative

Proved

Vino.singTerm_mul_coprime

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

analytic-number-theorycircle-methodnumber-theorysingular-series

Write $A_q(n)=\mu(q)c_q(n)/\varphi(q)^3$ for the $q$ -th term of the singular series of the three primes problem. If $(q_1,q_2)=1$ then

A_{q_1q_2}(n)=A_{q_1}(n)\,A_{q_2}(n).

Multiplicativity of $q\mapsto A_q(n)$ is inherited from that of $\mu$ , of $\varphi$ and of Ramanujan's sum; it is precisely what allows the singular series to be written as a product over primes.

Preamble

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

Formal statement

namespace Vino

theorem singTerm_mul_coprime {q₁ q₂ : ℕ} (h : Nat.Coprime q₁ q₂) (n : ℤ) :
    singTerm (q₁ * q₂) n = singTerm q₁ n * singTerm q₂ 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