Measure-theoretic results about the additive circle #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
The file is a place to collect measure-theoretic results about the additive circle.
Main definitions: #
G be the subgroup of
add_circle T generated by a point
u of finite order
n : ℕ. Then
I that is almost equal to a ball of radius
T / 2n is a fundamental domain for the action
add_circle T by left addition.