OAI/GroupTheory/PolycyclicRecognition/Analysis/CayleyBallCover.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Disjoint word-ball packings and their enlarged covers

These are the finite counting estimates used for the averaging map in Kleiner's polynomial-growth harmonic-function argument, Section 3.2.

  1. def OAI.PolycyclicRecognition.translatedWordBall line 17
  2. theorem OAI.PolycyclicRecognition.mem_translatedWordBall line 20
  3. theorem OAI.PolycyclicRecognition.card_translatedWordBall line 29
  4. theorem OAI.PolycyclicRecognition.mem_translatedWordBall_self line 33
  5. theorem OAI.PolycyclicRecognition.translatedWordBall_symm line 37
  6. theorem OAI.PolycyclicRecognition.translatedWordBall_triangle line 43
  7. theorem OAI.PolycyclicRecognition.mem_doubled_ball_of_not_disjoint line 49
  8. theorem OAI.PolycyclicRecognition.exists_disjoint_wordBall_cover line 57
  9. theorem OAI.PolycyclicRecognition.disjoint_wordBall_packing_bound line 87
  10. theorem OAI.PolycyclicRecognition.disjoint_wordBall_overlap_bound line 103
  11. theorem OAI.PolycyclicRecognition.sum_translatedWordBall_le_overlap line 114