The first term of the singular series is $1$

Proved

Vino.singTerm_one

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

analytic-number-theorycircle-methodnumber-theorysingular-series

The $q=1$ term of the singular series is

\frac{\mu(1)c_1(n)}{\varphi(1)^3}=1 .

It is the multiplicative identity of the Euler factorisation: every partial product of local densities starts from this term.

Preamble

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

Formal statement

namespace Vino

theorem singTerm_one (n : ℤ) : singTerm 1 n = 1 := 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

The first term of the singular series is 111

The first term of the singular series is $1$