Evaluation of $c_p(n)$ at a prime modulus

Proved

Vino.ramanujan_prime

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

analytic-number-theorycircle-methodnumber-theoryramanujan-sums

For a prime $p$ and any integer $n$ ,

c_p(n)=\begin{cases}p-1,& p\mid n,\\[2pt]-1,& p\nmid n.\end{cases}

Equivalently $c_p(n)=p\,[\,p\mid n\,]-1$ . This single evaluation is what turns the abstract $q$ -th term of the singular series into the classical local density: for the three primes problem it produces the factors $1-(p-1)^{-2}$ and $1+(p-1)^{-3}$ .

Preamble

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

Formal statement

namespace Vino

theorem ramanujan_prime {p : ℕ} (hp : p.Prime) (n : ℤ) :
    ramanujan p n = if (p : ℤ) ∣ n then ((p : ℂ) - 1) else -1 := by sorry

end Vino

Source

R. C. Vaughan, The Hardy-Littlewood Method, 2nd ed., Cambridge Tracts in Mathematics 125, Cambridge University Press, 1997, Section 2.6 and Chapter 3; G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers, 6th ed., Oxford University Press, 2008, Section 16.6 (Ramanujan's sum c_q(n)).

View graph

Evaluation of cp(n)c_p(n)cp​(n) at a prime modulus

Evaluation of $c_p(n)$ at a prime modulus