OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanLiftMultiplicity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Volume hidden by variable Cartan lifts

For Cartan logarithms with a subexponential bound and heights o(scale), all nilpotent coordinates projecting into one fixed-radius ambient ball have subexponential Haar outer measure. The center of the ball is arbitrary.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_subexponential_lift_multiplicity line 33