Ramanujan sums over the divisors give the complete sum

Proved

Vino.sum_divisors_ramanujan

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

analytic-number-theorycircle-methodnumber-theoryramanujan-sums

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

\sum_{d\mid q}c_d(n)\;=\;\begin{cases}q,& q\mid n,\\ 0,&\text{otherwise.}\end{cases}

Every residue $k<q$ belongs to exactly one class $\gcd(q,k)=d$ , and each class contributes $c_{q/d}(n)$ ; summing over $d$ therefore recovers the complete exponential sum $\sum_{k<q}e(kn/q)$ , which orthogonality evaluates.

This is the divisor-sum relation from which Kluyver's formula for $c_q(n)$ follows by Möbius inversion. It also exhibits $c_q$ as the Möbius transform of the elementary function $q\mapsto q\,[\,q\mid n\,]$ , which is where the multiplicativity in $q$ ultimately comes from.

Preamble

import Definitions.Def_Vino_ramanujan
import Mathlib.NumberTheory.Divisors
import Mathlib.NumberTheory.ArithmeticFunction.Moebius
import Mathlib.Data.Nat.Totient
open Finset

Formal statement

namespace Vino

theorem sum_divisors_ramanujan {q : ℕ} (hq : 0 < q) (n : ℤ) :
    ∑ d ∈ q.divisors, ramanujan d n = if (q : ℤ) ∣ n then (q : ℂ) else 0 := by sorry

end Vino

Source

G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers, 6th ed., Oxford University Press, 2008, Section 16.6, Theorem 271 (Ramanujan's sum c_q(n) = sum over d | gcd(q,n) of d * mu(q/d)); J. C. Kluyver, Some formulae concerning the integers less than n and prime to n, Proc. Royal Netherlands Academy 9 (1906), 408-414.

View graph