OAI/GroupTheory/PolycyclicRecognition/Analysis/HarmonicGoodScaleFactors.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Separate volume and determinant bounds from a good scale

  1. theorem OAI.PolycyclicRecognition.positive_product_power_first_factor line 9
  2. theorem OAI.PolycyclicRecognition.positive_product_power_second_factor line 20
  3. theorem OAI.PolycyclicRecognition.wordBall_good_scale_volume_bound line 32
  4. theorem OAI.PolycyclicRecognition.wordBall_good_scale_determinant_bound line 42
  5. def OAI.PolycyclicRecognition.harmonicScaleConstant line 52
  6. theorem OAI.PolycyclicRecognition.harmonicScaleConstant_gt_one line 54
  7. theorem OAI.PolycyclicRecognition.harmonic_good_scale_factor_bound line 59