OAI/GroupTheory/PolycyclicRecognition/Algebra/EventualPingPong.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Large powers of contracting transformations generate a free group

Uniform control of sufficiently large positive and negative powers on the other attracting domain suffices. A common power turns these estimates into the cyclic ping-pong criterion.

  1. theorem OAI.PolycyclicRecognition.eventual_ping_pong_free_power line 18