OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanSelectedProfilePaths.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual controlled paths from the selected affine profiles

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_selected_profile_paths line 29

    Source documentation

    One compact set of Cartan coordinates suffices for all the selected finite chains. Good affine profiles on that set produce actual paths with linear length, logarithmic jumps, and the prescribed convex height image.

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

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput