OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanPerturbedBox.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Subexponential corrections to endpoint-tuple increments

For a template containing zero, its scaled box contains the corresponding unscaled box. Left and right corrections with subexponential logarithms therefore preserve the template and change only its subexponential radius.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.norm_boxBasis_le_unscaled_of_zero_mem line 28
  2. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_subexponential_perturbed_groupBox line 59