OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanGradedGeometry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual graded Cartan group's geometric data

  1. theorem OAI.PolycyclicRecognition.cartan_graded_conjugation line 29

    Source documentation

    The conjugation identity for the actual graded Cartan law is derived from the published faithful realization and the original exponential.

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

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput

  2. theorem OAI.PolycyclicRecognition.lipschitz_supported_cartan_profiles line 63

    Source documentation

    Supported actual Cartan profiles have one horizontal Lipschitz bound for each direction, uniform in the starting point and supported profile.

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

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput