OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanPivotTemplateCoding.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Continuous box selectors independent of the starting sheet

The actual generator word is retained, so its finitely many prefix sheets can be used in the independent-probe concentration argument.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_continuous_pivot_template_coding line 33

    Source documentation

    The selector is chosen before both the starting sheet and the pivot. It has uniformly bounded length and amplitudes, and every evaluation is continuous on the entire closed coordinate ball.

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

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput