$e(b/q)$ depends only on $b$ modulo $q$

Proved

Vino.e_natCast_mod

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

analytic-number-theorycircle-methodnumber-theory

For $q\ge1$ and any natural number $b$ ,

e\!\left(\frac{b\bmod q}{q}\right)=e\!\left(\frac{b}{q}\right).

Replacing a numerator by its least nonnegative residue is the step that connects a sum indexed by $\{0,\dots,q-1\}$ with an arbitrary rational point $b/q$ of the circle.

Preamble

import Definitions.Def_CircleMethod_char
open Finset

Formal statement

namespace Vino

theorem e_natCast_mod (q : ℕ) (hq : 0 < q) (b : ℕ) :
    CircleMethod.e (((b % q : ℕ) : ℝ) / (q : ℝ)) = CircleMethod.e ((b : ℝ) / (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 1.1.

View graph

e(b/q)e(b/q)e(b/q) depends only on bbb modulo qqq

$e(b/q)$ depends only on $b$ modulo $q$