OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanMetricChartShift.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual small-distance lifts preserve a common Cartan chart domain

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_small_metric_chart_shift line 43

    Source documentation

    A sufficiently small fraction of the ambient scale admits a factor lift whose inverse Cartan translation carries one fixed coordinate ball into the required larger ball, uniformly in both nearby scales.

    theorem exists_small_metric_chart_shift
    (hExp : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput