OAI/NumberTheory/DukePrimeDegree/Geometry/DiagonalPeriodicity.lean

Periodicity of one diagonal map under full diagonal ergodicity

The chosen map need not itself be ergodic. Its period-n fixed sets are invariant under every diagonal translation, hence each has measure zero or one. There is either a common positive period almost everywhere or almost every point has no positive period.