Write and . A convenient form of the quadratic Weyl inequality is the following: if , and , then
The implied constant is absolute. In particular the familiar square-root saving is . We prove all estimates used in this statement.
First, the finite geometric series identity gives
where denotes distance to the nearest integer and the second bound is interpreted as infinite when that distance is zero. Indeed the sum is , and . This proves the exponential geometric sum bound.
Expand the squared quadratic exponential sum by the difference between its indices. Since , the diagonal and the paired off-diagonals give
For , partition the into consecutive blocks of length at most . Within one block, two distinct indices have difference . Since the denominator of after reduction is at least , . Therefore
Thus the points in a block are separated on the circle by at least .
For any such separated set, at most an absolute number of points lie in each pair of arcs whose distances from zero are between and . The closest few contribute to the capped reciprocal sum; the remaining arcs contribute for . Summing the harmonic series, using , proves a block bound . This is the required separated reciprocal-distance sum estimate, with its proof supplied here. There are blocks, so
For , the trivial bound already implies this estimate after increasing the absolute constant. This completes the proof, including the small denominators and the possible common factor of and .
Write and use for distance to the nearest integer. The Dirichlet approximation theorem, in its pigeonhole form, says that for every real and integer there are coprime integers with and . Indeed put the fractional parts of into equal intervals; two lie in the same interval. Their difference gives , and reducing the fraction preserves the claimed bound. This includes rational .
For , the finite geometric series has length . When ,
The last inequality uses the concavity of sine on . The triangle inequality also gives . At integer the sum has absolute value , interpreting the reciprocal as infinity. Thus the precise exponential geometric sum bound is
The interval must be nonempty; for its sum is zero and its length should be defined as , rather than using a potentially negative bound.
For the separated points, assume and . An arc of length contains at most of the points, by ordering them along the arc. Points with contribute . In the dyadic annulus , each summand is and there are at most points. There are nonempty annuli, giving the stronger separated reciprocal-distance sum
If there is only one point the bound is immediate; otherwise . The printed requires a lower bound away from ; avoids that endpoint defect.
A useful version of the quadratic Weyl inequality is the following, with , and :
For , expand the square of this quadratic exponential sum by :
The exponential geometric sum bound therefore gives . For , partition these into blocks of length at most . Two different points in one block have difference with . The reduced denominator of is at least , so , while
Thus the rotations are separated by at least in each block. The separated reciprocal-distance sum bounds each block by . There are blocks, and hence
For or , the trivial bound supplies the same assertion with an absolute constant. The same proof applies to , whose difference sums also have interval endpoints.
We finally prove a polynomial rate of quantitative quadratic recurrence, without using the optional finite-group assumption. For , use the periodic triangular bump . It is times the periodic convolution of two interval indicators, and therefore has the nonnegative Fourier coefficients
Its Fourier series is absolutely convergent, , and the coefficient tail is . Suppose that for every . Then . Choose with a sufficiently large absolute , so that the contribution of frequencies has absolute value at most . The zero frequency contributes . Since all coefficients are nonnegative and their sum is one, some must satisfy
Apply the Dirichlet approximation theorem to with , obtaining a reduced , . The quadratic Weyl inequality then implies
Set . For sufficiently large , the term is absorbed on the left, giving . The integer consequently satisfies
Moreover the approximating integer is , and
This contradicts the assumed avoidance. Increasing the absolute constant handles the finitely many smaller , uniformly for every real . Thus