OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanCocycleWordGrowth.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Sublinear cocycles on compact words in the ambient Cartan group

The actual compact factor lifts control both factors of the same word. The nilpotent factor lies in a polynomially enlarged root box; the Cartan factor remains a word in one compact set, where nilpotent reduced cohomology applies.

  1. theorem OAI.PolycyclicRecognition.cartan_cocycle_compact_words line 48
  2. theorem OAI.PolycyclicRecognition.cartan_cocycle_sublinear line 134