Character sums away from a centered slab

Jordan's inequality bounds a nontrivial root of unity away from one in terms of its centered residue. The finite geometric-series identity then bounds every partial character sum independently of its length.

theorem EGZ.Expansion.zmodAddEquiv_one {p : ℕ} [NeZero p] (r : ZMod p) : (AddChar.zmodAddEquiv r) 1 = Complex.exp (Complex.I * (2 * ↑Real.pi * ↑↑r.valMinAbs / ↑p))

theorem EGZ.Expansion.norm_zmodAddEquiv_one_sub_one_ge {p : ℕ} [NeZero p] (r : ZMod p) : 4 * |↑r.valMinAbs| / ↑p ≤ ‖(AddChar.zmodAddEquiv r) 1 - 1‖

A centered residue controls the distance of its character value from one. This estimate does not require primality.

theorem EGZ.Expansion.character_partial_sum_le {p K : ℕ} [NeZero p] (hK : 0 < K) (r : ZMod p) (hr : ¬HasBoundedRepresentative p K r) (m : ℕ) : ‖∑ j ∈ Finset.range m, (AddChar.zmodAddEquiv r) ↑j‖ ≤ 2 * ↑p / ↑K