$|c_q(n)|\le\varphi(q)$

Proved

Vino.norm_ramanujan_le

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

analytic-number-theorycircle-methodnumber-theoryramanujan-sums

The trivial bound for Ramanujan's sum:

|c_q(n)|\le\varphi(q)\qquad\text{for all }q\ge0,\ n\in\mathbb Z.

Combined with $\mu(q)^2\le1$ it gives $|\mu(q)c_q(n)/\varphi(q)^3|\le\varphi(q)^{-2}$ , which is the crude estimate behind the absolute convergence of the singular series of the three primes problem.

Preamble

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

Formal statement

namespace Vino

theorem norm_ramanujan_le (q : ℕ) (n : ℤ) : ‖ramanujan q n‖ ≤ (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(n)∣≤φ(q)|c_q(n)|\le\varphi(q)∣cq​(n)∣≤φ(q)

$|c_q(n)|\le\varphi(q)$