OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanUniformSuffixMetric.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A fixed metric bound for every allowed suffix family

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_uniform_suffix_metric_bound line 31

    Source documentation

    The bound is fixed before the enlargement, the scale sequence, and the subexponential radius. Thus compact profiles may be chosen before the small enlargement required by the neighboring theorem.

    theorem exists_uniform_suffix_metric_bound
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput