Exponential and character sums

Gauss sums, Weyl and Vinogradov sums, incomplete exponential sums, Burgess bounds, Dirichlet polynomials, trigonometric and cotangent sums.

TheoremLandsberg–Schaar relation#✓fully proved

For all positive integers \(p\) and \(q\),

\[ \frac{1}{\sqrt{p}} \sum_{n=0}^{p-1} \exp\left(\frac{2 \pi i n^2 q}{p}\right) = \frac{e^{\pi i / 4}}{\sqrt{2q}} \sum_{n=0}^{2q-1} \exp\left(-\frac{\pi i n^2 p}{2q}\right). \]
theorem landsberg_schaar (p q : ℕ) (hp : 1 ≤ p) (hq : 1 ≤ q) :
  (1 / (Real.sqrt (p : ℝ) : ℂ)) * ∑ n ∈ Finset.range p, Complex.exp
    (2 * (Real.pi : ℂ) * Complex.I * ((n : ℂ) ^ 2 * (q : ℂ) / (p : ℂ))) =
    (Complex.exp ((Real.pi : ℂ) * Complex.I / 4) / (Real.sqrt (2 * (q : ℝ)) : ℂ)) * ∑ n ∈
      Finset.range (2 * q), Complex.exp
      (-(Real.pi : ℂ) * Complex.I * ((n : ℂ) ^ 2 * (p : ℂ) / (2 * (q : ℂ))))
Sources
  • https://en.wikipedia.org/wiki/Landsberg%E2%80%93Schaar_relation.

TheoremMittou's evaluation of a quadratic sum over congruent pairs#●ready to prove

Let \(p\) be a prime and \(l\) a positive integer with \(\gcd(p, l) = 1\). Let \(F(p, l)\) be the sum of \(\left(\frac{a}{p} - \frac{1}{2}\right)\left(\frac{b}{p} - \frac{1}{2}\right)\) over all pairs of integers \(a, b\) with \(1 \le a, b \le p - 1\) and \(b \equiv a l \pmod{p}\), and let

\[s(p, l) = \frac{1}{4l} \sum_{a=1}^{l-1} \cot\left(\frac{\pi a}{l}\right) \cot\left(\frac{\pi a p}{l}\right)\]

be the Dedekind sum. Then

\[F(p, l) = \frac{p^2 - 3lp + l^2 + 1}{12 l p} - s(p, l).\]

Domain extension: the paper assumes \(p \ge 3\); the identity also holds for \(p = 2\) (then \(l\) is odd and both sides vanish), so that hypothesis is dropped. The paper's remark that \(s(p, l)\) depends only on \(p \bmod l\) is not restated.

public theorem_wanted congruentPairQuadraticSum_eq_sub_dedekindSum {p l : ℕ} (hp : p.Prime)
    (hl : 0 < l) (hpl : p.Coprime l) :
    (∑ a ∈ Finset.Icc 1 (p - 1),
        ∑ b ∈ (Finset.Icc 1 (p - 1)).filter (fun b => b ≡ a * l [MOD p]),
          ((a : ℝ) / p - 1 / 2) * ((b : ℝ) / p - 1 / 2)) =
      ((p : ℝ) ^ 2 - 3 * l * p + l ^ 2 + 1) / (12 * l * p) -
        1 / (4 * l) * ∑ a ∈ Finset.Icc 1 (l - 1),
          Real.cot (Real.pi * a / l) * Real.cot (Real.pi * a * p / l)
Sources
  • Brahim Mittou, Explicit Evaluation of a Quadratic Sum Over Congruent Pairs Modulo a Prime, INTEGERS 25 (2025), Article A85, Theorem 1.
1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.