OAI/GroupTheory/PolycyclicRecognition/Geometry/TriangularExponentialAverage.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Invertibility of the averaged real triangular exponential

This is the linear operator appearing in the differential of exponential coordinates. Its diagonal entries are integrals of positive real exponentials, so they cannot vanish. No global exponential theorem is used.

  1. def OAI.PolycyclicRecognition.triangularExpAverage line 22
  2. theorem OAI.PolycyclicRecognition.triangularExpAverage_mul line 25
  3. theorem OAI.PolycyclicRecognition.triangularExpAverage_entry line 41
  4. theorem OAI.PolycyclicRecognition.triangularExpAverage_upper line 51
  5. theorem OAI.PolycyclicRecognition.triangularExpAverage_diagonal line 61
  6. theorem OAI.PolycyclicRecognition.triangularExpAverage_diagonal_pos line 74
  7. theorem OAI.PolycyclicRecognition.triangularExpAverage_isUnit line 83