OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanControlledFolner.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Concrete controlled Følner pairs on the Cartan semidirect cover

Exponentially large nilpotent boxes are paired with good-volume Cartan balls. Right multiplication by a metric ball enlarges the box radius by a constant, and the Cartan ball radius by at most three. Both volume ratios are bounded.

  1. theorem OAI.PolycyclicRecognition.cartan_cover_controlled_pairs line 41