OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanDProfiles.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Equicontinuity of profiles on the actual Cartan factor

  1. theorem OAI.PolycyclicRecognition.equicontinuous_cartan_d_profiles line 28

    Source documentation

    The chart profiles have a common modulus of continuity for arbitrary sampled suffixes, centers, and uniformly Lipschitz maps. The metric estimate, limiting group law, and fixed-scale continuity are all derived here.

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

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput