Exponential twisting preserves bounded partial sums with an explicit variation loss

Proved

CircleMethod.norm_sum_twist_le

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

analytic-number-theorycircle-methodexponential-sumspartial-summation

Let $a_0,a_1,\ldots$ be complex numbers, let $N$ be a nonnegative integer, and let $E\ge0$ . Suppose every initial partial sum through length $N$ satisfies

\left|\sum_{n<K}a_n\right|\le E\qquad(0\le K\le N).

For every real $\beta$ , writing $e(t)=\exp(2\pi i t)$ , one then has

\left|\sum_{n<N}a_ne(\beta n)\right|\le (1+2\pi N|\beta|)E.

This is a finite Abel-summation estimate for transporting cancellation to a nearby frequency. It includes the empty sum and imposes no rationality or nonvanishing condition on $\beta$ .

Preamble

import Mathlib
import Definitions.Def_CircleMethod_char

Formal statement

theorem CircleMethod.norm_sum_twist_le (a : ℕ → ℂ) (N : ℕ) (β E : ℝ)
    (hE : 0 ≤ E)
    (hpartial : ∀ K : ℕ, K ≤ N → ‖∑ n ∈ Finset.range K, a n‖ ≤ E) :
    ‖∑ n ∈ Finset.range N, a n * CircleMethod.e (β * (n : ℝ))‖
      ≤ (1 + 2 * Real.pi * (N : ℝ) * |β|) * E := by sorry

Source

Finite Abel summation: Mathlib, Mathlib/Algebra/BigOperators/Module.lean, Finset.sum_range_by_parts; phase variation from Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean, Real.norm_exp_I_mul_ofReal_sub_one_le. This explicit finite corollary is proved in the submitted solution. Related analytic use: H. A. Helfgott, The ternary Goldbach conjecture is true, arXiv:1312.7748, Section 6.1 (summation by parts).

View graph