mathlib documentation

measure_theory.group.add_circle

Measure-theoretic results about the additive circle #

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.