Kluyver's formula for Ramanujan's sum

Proved

Vino.ramanujan_eq_kluyver

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

analytic-number-theorycircle-methodnumber-theoryramanujan-sums

Kluyver's closed formula: for $q\ge1$ and any integer $n$ ,

c_q(n)\;=\;\sum_{\substack{d\mid q\\ d\mid n}}d\,\mu\!\left(\frac{q}{d}\right) \;=\;\sum_{d\mid\gcd(q,n)}d\,\mu\!\left(\frac{q}{d}\right).

The statement is written as a sum over all divisors $d$ of $q$ , with the summand set to $0$ unless $d\mid n$ , which is the same thing.

This is the single most useful fact about Ramanujan sums. It shows at once that $c_q(n)$ is an integer, that it depends on $n$ only through $\gcd(q,n)$ , that $c_q(-n)=c_q(n)$ , and — since it exhibits $c_q(n)$ as a Möbius-type convolution — that $q\mapsto c_q(n)$ is multiplicative. It also gives the bound $|c_q(n)|\le\sigma(\gcd(q,n))$ used to control the tail of the singular series.

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 ramanujan_eq_kluyver {q : ℕ} (hq : 0 < q) (n : ℤ) :
    ramanujan q n
      = ∑ d ∈ q.divisors,
          (if (d : ℤ) ∣ n then (d : ℂ) else 0)
            * ((ArithmeticFunction.moebius (q / d) : ℤ) : ℂ) := 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