OAI/GroupTheory/PolycyclicRecognition/Analysis/CompactWordCost.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Weighted costs attached to a compact generating neighborhood

Inside the generating neighborhood use the original metric; outside it use word length. This preserves the local topology while controlling word length.

  1. def OAI.PolycyclicRecognition.metricGroupNorm line 21
  2. def OAI.PolycyclicRecognition.compactWordGenerators line 35
  3. def OAI.PolycyclicRecognition.compactWordLength line 37
  4. theorem OAI.PolycyclicRecognition.compactWordLength_le_one line 40
  5. theorem OAI.PolycyclicRecognition.compactWordLength_one line 45
  6. theorem OAI.PolycyclicRecognition.compactWordLength_inv line 49
  7. def OAI.PolycyclicRecognition.compactWordCost line 53
  8. theorem OAI.PolycyclicRecognition.compactWordCost_mem line 58
  9. theorem OAI.PolycyclicRecognition.wordLength_le_cost line 62
  10. theorem OAI.PolycyclicRecognition.metric_le_compactWordCost line 76
  11. theorem OAI.PolycyclicRecognition.compactWordCost_inv line 88
  12. def OAI.PolycyclicRecognition.compactWeightedNorm line 96
  13. theorem OAI.PolycyclicRecognition.wordLength_le_weightedNorm_add line 100