Continuity of the additive character
ProvedVino.continuous_eanalytic-number-theorycircle-methodnumber-theory
The character is a continuous function .
Continuity is the hypothesis behind every integrability claim in the circle method: the generating functions are finite sums of continuous functions, so all the integrals over that define Fourier coefficients exist.
Preamble
import Definitions.Def_CircleMethod_char open Finset
Formal statement
namespace Vino theorem continuous_e : Continuous CircleMethod.e := 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.