Ramanujan sums as a sum over the unit group

Proved

Vino.ramanujan_eq_sum_units

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

analytic-number-theorycircle-methodnumber-theoryramanujan-sums

For $q\ge1$ ,

c_q(n)=\sum_{u\in(\mathbb Z/q\mathbb Z)^{\times}}e\!\left(\frac{\tilde u\,n}{q}\right),

where $\tilde u$ denotes the representative in $\{0,\dots,q-1\}$ of the unit $u$ .

This is the working form of Ramanujan's sum: the index set is now a finite abelian group, so translation by a unit and the Chinese remainder decomposition become available as reindexings.

Preamble

import Definitions.Def_Vino_ramanujan
import Mathlib.Data.ZMod.Units
open Finset

Formal statement

namespace Vino

theorem ramanujan_eq_sum_units (q : ℕ) [NeZero q] (n : ℤ) :
    ramanujan q n
      = ∑ u : (ZMod q)ˣ,
          CircleMethod.e (((((u : ZMod q).val : ℤ) * n : ℤ) : ℝ) / (q : ℝ)) := 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