OAI/GroupTheory/PolycyclicRecognition/Analysis/WordBallGram.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Gram matrices of word-ball evaluations

The determinant is the volume quantity used in Kleiner's scale selection. Its positivity comes from separation by a finite ball, and its polynomial upper bound comes directly from polynomial growth of the functions.

  1. def OAI.PolycyclicRecognition.wordBallEvaluationMatrix line 20
  2. def OAI.PolycyclicRecognition.wordBallGram line 23
  3. theorem OAI.PolycyclicRecognition.wordBallGram_apply line 27
  4. theorem OAI.PolycyclicRecognition.wordBallGram_posDef_of_separates line 33
  5. theorem OAI.PolycyclicRecognition.exists_wordBallGram_posDef line 48
  6. theorem OAI.PolycyclicRecognition.finite_family_polynomial_word_bound line 66
  7. theorem OAI.PolycyclicRecognition.wordBallGram_entry_bound line 75
  8. theorem OAI.PolycyclicRecognition.wordBallGram_det_bound line 93