OAI/GroupTheory/PolycyclicRecognition/Geometry/CanonicalHeightContractionModel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_canonical_height_model_with_controlled_contraction line 19

   Source documentation

   Choose the Riemannian metric after fixing the triangular model, and construct its controlled exponential contraction from the two precisely stated published regularity inputs.

   theorem exists_canonical_height_model_with_controlled_contraction
       (ct : CornulierTesseraModelInput) (metric : GeodesicMetricExistenceInput)
       (riemannian : LieRiemannianMetricInput)
       (regular : ∀ R : SimplyConnectedSolvableLieModel,
         DixmierExponentialDiffeomorphismInput (E := R.modelSpace) (G := R.carrier))
   …

   Mentions: OAI.PolycyclicRecognition.CornulierTesseraModelInput, OAI.PolycyclicRecognition.GeodesicMetricExistenceInput, OAI.PolycyclicRecognition.LieRiemannianMetricInput, OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel, OAI.PolycyclicRecognition.DixmierExponentialDiffeomorphismInput