OAI/NumberTheory/DukePrimeDegree/Dynamics/CentralOrbitCover.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Time-independent covers of compact neutral displacements

Compact sets of displacements commuting with the diagonal flow admit a fixed finite orbit cover, valid for every time and every base point. Thus their geometric covering cost does not grow with orbit length.

  1. theorem OAI.DukePrimeDegree.quotientLogDistance_commuting_displacements line 20
  2. theorem OAI.DukePrimeDegree.compact_neutral_orbit_cover line 32