Ramanujan sums

DefinitionRamanujan sum#✓fully proved

For a positive integer \(n\) and an integer \(t\), the Ramanujan sum of modulus \(n\) at \(t\) is the complex number

\[c_n(t) = \sum_{a \in (\mathbb{Z}/n\mathbb{Z})^\times} e^{2\pi i a t / n},\]

the sum over the units \(a\) modulo \(n\) of the standard additive character of \(\mathbb{Z}/n\mathbb{Z}\) evaluated at \(a t\).

noncomputable def ramanujanSum (n : ℕ) [NeZero n] (t : ℤ) : ℂ :=
  ∑ a : (ZMod n)ˣ, ZMod.stdAddChar ((a : ZMod n) * (t : ZMod n))

Used by 3

Used byPeriodicity of Ramanujan sums · Ramanujan sums of modulus one · Ramanujan sum at zero

TheoremRamanujan sum at zero#✓fully proved

For every positive integer \(n\), the Ramanujan sum \(c_n(0)\) equals Euler's totient \(\varphi(n)\).

@[simp]
theorem ramanujanSum_zero (n : ℕ) [NeZero n] :
    ramanujanSum n 0 = Nat.totient n

Uses 1

Statement usesRamanujan sum

TheoremRamanujan sums of modulus one#✓fully proved

For every integer \(t\), the Ramanujan sum \(c_1(t)\) equals \(1\).

@[simp]
theorem ramanujanSum_modulus_one (t : ℤ) : ramanujanSum 1 t = 1

Uses 1

Statement usesRamanujan sum

TheoremPeriodicity of Ramanujan sums#✓fully proved

For every positive integer \(n\) and all integers \(t\) and \(k\), the Ramanujan sum \(c_n\) of modulus \(n\) satisfies \(c_n(t + kn) = c_n(t)\).

@[simp]
theorem ramanujanSum_add_mul_modulus (n : ℕ) [NeZero n] (t k : ℤ) :
    ramanujanSum n (t + k * n) = ramanujanSum n t

Uses 1

Statement usesRamanujan sum

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.