Ramanujan sums are real

Proved

Vino.ramanujan_conj

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

analytic-number-theorycircle-methodnumber-theoryramanujan-sums

Ramanujan's sum is fixed by complex conjugation:

\overline{c_q(n)}=c_q(n).

So $c_q(n)$ is real — in fact an integer. This matters when the singular series is shown to be positive: each local factor $1+\mu(q)c_q(n)/\varphi(q)^3$ is a real number, and inequalities between real numbers are what the argument needs.

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_conj (q : ℕ) (n : ℤ) : (starRingEnd ℂ) (ramanujan q n) = ramanujan q n := 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