OAI/GroupTheory/PolycyclicRecognition/Geometry/TriangularInverseBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Polynomial inverse bounds in bounded-height triangular regions

Removing the diagonal leaves a unipotent matrix. Its inverse is a finite geometric sum, so a bound for the matrix and its height gives a polynomial bound for its inverse. Both bounds are needed when turning coordinate packing into packing for a left invariant group metric.

  1. theorem OAI.PolycyclicRecognition.PositiveTriangular.norm_inverse_le line 20