OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanTuplePerturbation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Box bounds survive thickening of an endpoint tuple

Each successive increment keeps its own template. In particular, this applies to alternating reflected templates, without replacing them by their union before the polynomial multiplication argument.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_subexponential_tuple_perturbation line 30