$c_q(0)=\varphi(q)$

Proved

Vino.ramanujan_arg_zero

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

analytic-number-theorycircle-methodnumber-theoryramanujan-sums

At $n=0$ every summand of Ramanujan's sum is $1$ , so

c_q(0)=\varphi(q).

This is the maximal possible value of $|c_q(n)|$ , and it is the value that appears when the singular series of the three primes problem is evaluated at the trivial local condition.

Preamble

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

Formal statement

namespace Vino

theorem ramanujan_arg_zero (q : ℕ) : ramanujan q 0 = (Nat.totient 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

cq(0)=φ(q)c_q(0)=\varphi(q)cq​(0)=φ(q)

$c_q(0)=\varphi(q)$