OAI/GroupTheory/PolycyclicRecognition/Algebra/ControlledProductPairs.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Controlled Følner pairs from compact product coordinates

The required estimate is an explicit right-product containment in a larger rectangle, together with a bounded ratio of the two coordinate volumes.

  1. theorem OAI.PolycyclicRecognition.productCoordinateMeasure_rectangle line 30
  2. def OAI.PolycyclicRecognition.controlledMetricFolnerPairs_of_product_sets line 39