OAI/GroupTheory/PolycyclicRecognition/Analysis/HarmonicVolumeDeterminant.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Polynomial growth of the combined volume and Gram determinant

Raising the ball volume to the dimension avoids fractional powers in the scale-selection quantity from Kleiner, Section 3.1.

  1. def OAI.PolycyclicRecognition.wordBallVolumeDeterminant line 17
  2. theorem OAI.PolycyclicRecognition.wordBallVolumeDeterminant_nonneg line 20
  3. theorem OAI.PolycyclicRecognition.wordBallVolumeDeterminant_monotone line 24
  4. theorem OAI.PolycyclicRecognition.wordBallVolumeDeterminant_pos line 32
  5. theorem OAI.PolycyclicRecognition.wordBallVolumeDeterminant_polynomial_bound line 37
  6. theorem OAI.PolycyclicRecognition.polynomial_sequence_exponential_bound line 67
  7. theorem OAI.PolycyclicRecognition.exists_wordBall_volume_determinant_good_scales line 81