OAI/GroupTheory/PolycyclicRecognition/Algebra/CocycleCombing.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Sublinear cocycles from a nilpotent subgroup and bounded combing

The geometric premise is an explicit product of a bounded number of compact factors and subgroup factors, with a linear bound on their total subgroup length. No cohomological conclusion is included in this premise.

  1. def OAI.PolycyclicRecognition.HasBoundedSubgroupCombing line 21
  2. theorem OAI.PolycyclicRecognition.IsUnitaryCocycle.norm_mul_le line 31
  3. theorem OAI.PolycyclicRecognition.IsUnitaryCocycle.norm_paired_word_le line 36
  4. theorem OAI.PolycyclicRecognition.IsUnitaryCocycle.sublinear_of_bounded_combing line 55
  5. theorem OAI.PolycyclicRecognition.IsUnitaryCocycle.sublinear_of_approximation line 85
  6. theorem OAI.PolycyclicRecognition.IsUnitaryCocycle.sublinear_of_nilpotent_combing line 98