Multiple recurrence for circle rotations (source code)

= Multiple recurrence for circle rotations

Every circle rotation has the <Furstenberg multiple recurrence theorem> property for normalized <Lebesgue measure>. For a rational angle, use a period. For an irrational angle, choose a positive return time with angle close to zero; <translation continuity in L1 on the circle> then makes finitely many translates of a given positive-measure set simultaneously close to that set, and the <union bound> leaves a positive-measure intersection.