OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanSeparatedAlternatingComparison.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Separated target tuples supply the alternating increment volume

The auxiliary Cartan volume is subexponential. Thus the finite separated count supplies the full correlated Haar lower bound needed by the product comparison; this lower bound is not assumed independently.

  1. def OAI.PolycyclicRecognition.CartanWordModel.alternatingCoordinateFamily line 39
  2. theorem OAI.PolycyclicRecognition.CartanWordModel.alternatingCoordinateFamily_left line 42
  3. theorem OAI.PolycyclicRecognition.CartanWordModel.alternatingCoordinateFamily_right line 46
  4. theorem OAI.PolycyclicRecognition.CartanWordModel.separated_alternating_product_exponent_le line 50