OAI/GroupTheory/PolycyclicRecognition/Algebra/ControlledReiterCocycles.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Controlled scalar averages turn sublinear cocycles into coboundaries

The geometric data are compactly supported probability densities with translation error of order inverse scale and support of order scale. They contain no representation or cohomology hypotheses.

  1. structure OAI.PolycyclicRecognition.ControlledReiterFamily line 21
  2. theorem OAI.PolycyclicRecognition.ControlledReiterFamily.almost_coboundary line 39