mathlib3 documentation

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: #

Let G be the subgroup of add_circle T generated by a point u of finite order n : ℕ. Then any set I that is almost equal to a ball of radius T / 2n is a fundamental domain for the action of G on add_circle T by left addition.