OAI/NumberTheory/DukePrimeDegree/Dynamics/RootOrbitConcentration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Root-pair orbit concentration from strong returns

This is the arithmetic-quotient specialization of the compact-return argument in EKL (2006), Proposition 4.3. The countable ergodic action may be a dense subgroup of the neutral diagonal group. A positive-measure set with strong returns forces the component onto one root-pair orbit.

  1. theorem OAI.DukePrimeDegree.rootPair_orbit_of_strong_returns line 23