OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanOverlapCoordinates.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic coordinates of the Cartan overlap

Injectivity of the ambient exponential identifies the two logarithms of an overlap element. A fixed linear retraction compares their coordinate norms; this controls the entire overlap rather than its center.

  1. theorem OAI.PolycyclicRecognition.CartanFactorModel.overlap_log_eq line 25
  2. theorem OAI.PolycyclicRecognition.CartanFactorModel.exists_overlap_coordinate_bound line 41