Conjugation symmetry of Ramanujan sums

Proved

Vino.ramanujan_neg

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

analytic-number-theorycircle-methodnumber-theoryramanujan-sums

For all $q$ and $n$ ,

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

Together with the fact that $c_q$ is real valued this gives the evenness $c_q(-n)=c_q(n)$ ; on its own it is the statement that the local factors of the singular series respect the symmetry $n\mapsto-n$ of the underlying additive problem.

Preamble

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

Formal statement

namespace Vino

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