Quadratic Gauss sums

DefinitionQuadratic Gauss sum modulo \(5\)#✓fully proved

For an integer \(k\), the quadratic Gauss sum \(g(k; 5)\) is the complex number \(g(k; 5) = \sum_{n=0}^{4} e^{2\pi i k n^2 / 5}\).

public noncomputable def quadraticGaussSum5 (k : ℤ) : ℂ :=
  Finset.sum (Finset.range 5) (fun n =>
    Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (k : ℂ) * (n : ℂ) ^ 2 / 5))

Used by 1

Used byEvaluation of the quadratic Gauss sum modulo \(5\)

TheoremEvaluation of the quadratic Gauss sum modulo \(5\)#✓fully proved

For every integer \(k\) not divisible by \(5\), the quadratic Gauss sum \(g(k; 5) = \sum_{n=0}^{4} e^{2\pi i k n^2 / 5}\) equals \(\left(\frac{k}{5}\right)\sqrt{5}\), where \(\left(\frac{k}{5}\right)\) is the Legendre symbol.

public theorem quadraticGaussSum5_eval (k : ℤ) (hk : ¬ (5 : ℤ) ∣ k) :
    quadraticGaussSum5 k =
      ((legendreSym 5 k : ℤ) : ℂ) * ((Real.sqrt 5 : ℝ) : ℂ)

Sources

• the classical evaluation recorded in Dresden–Li, Journal of Integer Sequences 26 (2023), citing Berndt, Evans, and Williams, Theorem 1.5.2.

Uses 1

Statement usesQuadratic Gauss sum modulo \(5\)

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.