Ramanujan sums are periodic in $n$ modulo $q$

Proved

Vino.ramanujan_periodic

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

analytic-number-theorycircle-methodnumber-theoryramanujan-sums

For $q\ge1$ and every integer $n$ ,

c_q(n+q)=c_q(n).

Ramanujan's sum is therefore a function of the residue class of $n$ modulo $q$ — it is the local object attached to the congruence condition modulo $q$ , which is exactly the role it plays in the singular series.

Preamble

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

Formal statement

namespace Vino

theorem ramanujan_periodic {q : ℕ} (hq : 0 < q) (n : ℤ) : ramanujan q (n + (q : ℤ)) = ramanujan 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, 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

Ramanujan sums are periodic in nnn modulo qqq

Ramanujan sums are periodic in $n$ modulo $q$