OAI/GroupTheory/PolycyclicRecognition/Analysis/ControlledMetricFolner.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compact Følner pairs supply controlled averaging densities

Only a bounded volume ratio between a compact set and its thickening is needed. Normalized inverse-coordinate tents produce continuous probability densities with the required support and translation estimates.

  1. structure OAI.PolycyclicRecognition.ControlledMetricFolnerPairs line 21
  2. def OAI.PolycyclicRecognition.ControlledMetricFolnerPairs.toReiter line 39