OAI/GroupTheory/PolycyclicRecognition/Geometry/CanonicalHeightMetricChoice.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_canonical_height_model_with_metric_choice line 17

   Source documentation

   The triangular model and height space can be fixed before the endpoint metrics. Thus a subsequently chosen minimizing-path metric retains both the quasi-isometry comparison and the proved canonical-height Lipschitz bound.

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

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