OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanDMetric.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_cartan_d_chart_metric_bound line 32

   Source documentation

   Bounded normalized coordinates in the Cartan factor have ambient distance at most a constant times the dilation scale. This follows from the actual finite generator words, not a metric-scaling hypothesis.

   theorem exists_cartan_d_chart_metric_bound
       (hExpG : IsGroupExponential ExpG)
       (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
   …

   Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput

2. theorem OAI.PolycyclicRecognition.cartan_d_metric_sublinear_of_coordinates line 78

   Source documentation

   Small normalized Cartan coordinates give sublinear ambient distance. This is the equicontinuity estimate needed after taking a limit of the finite-dimensional coordinate group laws.

   theorem cartan_d_metric_sublinear_of_coordinates
       (hExpG : IsGroupExponential ExpG)
       (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
   …

   Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput