Interval integrability of linear phases

Proved

Vino.intervalIntegrable_e

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

analytic-number-theorycircle-methodnumber-theory

For every real $m$ and all $a<b$ , the function $\alpha\mapsto e(m\alpha)$ is interval integrable on $[a,b]$ .

Every integrand appearing in the circle method is, after expanding the generating function, a finite linear combination of such pure phases; this lemma is what allows the integral to be exchanged with those finite sums.

Preamble

import Definitions.Def_CircleMethod_char
import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
open Finset

Formal statement

namespace Vino

theorem intervalIntegrable_e (m : ℝ) (a b : ℝ) :
    IntervalIntegrable (fun α : ℝ => CircleMethod.e (m * α)) MeasureTheory.volume a b := 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