OAI/GroupTheory/PolycyclicRecognition/Geometry/CanonicalHeightMinimizingModel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_canonical_height_model_with_minimizing_metric line 16

   Source documentation

   Choose the published minimizing metric only after the triangular Lie model is fixed. Its chain structure is derived by sampling those paths.

   theorem exists_canonical_height_model_with_minimizing_metric
       (ct : CornulierTesseraModelInput) (metric : GeodesicMetricExistenceInput)
       (minimizing : LieMinimizingMetricInput)
       (differential : MatrixLieDifferentialInput)
       (dixmier : ∀ (R : SimplyConnectedSolvableLieModel) (d : ProperChainMetric R.carrier),
         letI := d.compatibleMetric
   …

   Mentions: OAI.PolycyclicRecognition.CornulierTesseraModelInput, OAI.PolycyclicRecognition.GeodesicMetricExistenceInput, OAI.PolycyclicRecognition.LieMinimizingMetricInput, OAI.PolycyclicRecognition.MatrixLieDifferentialInput, OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel, OAI.PolycyclicRecognition.ProperChainMetric