The $p$ -th term of the singular series is the local density

Proved

Vino.singTerm_prime

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

analytic-number-theorycircle-methodnumber-theorysingular-series

Let $p$ be prime. The $q=p$ term of the singular series of the three primes problem,

A_p(n)=\frac{\mu(p)\,c_p(n)}{\varphi(p)^3},

satisfies

1+A_p(n)=\mathfrak S_p(n)=\begin{cases}1-\dfrac{1}{(p-1)^2},& p\mid n,\\[8pt] 1+\dfrac{1}{(p-1)^3},& p\nmid n.\end{cases}

This is the step that converts the arithmetic definition of the singular series, as a sum of Ramanujan sums weighted by $\mu(q)/\varphi(q)^3$ , into the classical product of local densities.

Preamble

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

Formal statement

namespace Vino

theorem singTerm_prime {p : ℕ} (hp : p.Prime) (n : ℤ) :
    (1 : ℂ) + singTerm p n = ((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

The ppp-th term of the singular series is the local density

The $p$ -th term of the singular series is the local density