Prove2Me

Linear Weyl-sum bound ∥∑n<Ne(αn)∥≤min⁡(N,(2∥α∥)−1)\|\sum_{n<N}e(\alpha n)\| \le \min(N, (2\|\alpha\|)^{-1})

Proved
CircleMethod.geom_sum_bound

by jjosh · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

circle-methodexponential-sumsnumber-theory

The linear exponential sum satisfies the standard two-part bound

∣∑n<Ne(αn)∣≤min⁡(N, 12∥α∥),\Bigl|\sum_{n<N} e(\alpha n)\Bigr| \le \min\Bigl(N,\ \frac{1}{2\|\alpha\|}\Bigr),

where ∥α∥\|\alpha\| is the distance to the nearest integer and the second term is only asserted when ∥α∥>0\|\alpha\|>0. The trivial bound is the triangle inequality with ∣e∣=1|e|=1; the nontrivial bound uses the geometric series ∑e(αn)=(e(αN)−1)/(e(α)−1)\sum e(\alpha n) = (e(\alpha N)-1)/(e(\alpha)-1) together with ∣e(α)−1∣=2∣sin⁡πα∣≥4∥α∥|e(\alpha)-1| = 2|\sin\pi\alpha| \ge 4\|\alpha\| (Jordan's inequality sin⁡x≥2x/π\sin x \ge 2x/\pi). This is the basic cancellation bound behind every minor-arc estimate in the circle method.

Preamble
import Mathlib
import Definitions.Def_CircleMethod_char
Formal statement
namespace CircleMethod

theorem geom_sum_bound (N : ℕ) (α : ℝ) :
    ‖∑ n ∈ Finset.range N, e (α * (n : ℝ))‖ ≤ (N : ℝ)
      ∧ (0 < nrm α →
        ‖∑ n ∈ Finset.range N, e (α * (n : ℝ))‖ ≤ (2 * nrm α)⁻¹) := by
  sorry

end CircleMethod
Source
standard; e.g. Davenport, Multiplicative Number Theory, Ch. 25

View graph