OAI/GroupTheory/PolycyclicRecognition/Geometry/UniversalAllScaleCartanProfiles.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A compact profile family for every nonnegative real scale

  1. structure OAI.PolycyclicRecognition.AllScaleProfileData line 17

    Source documentation

    Only the metric data used to form a normalized chart profile.

    structure AllScaleProfileData (G W : Type*) [Group G] [PseudoMetricSpace G]
    [NormedAddCommGroup W] (K : ℝ≥0) (B : ℝ) where
…
  2. theorem OAI.PolycyclicRecognition.equicontinuous_all_cartan_profiles line 38

    Source documentation

    All nonnegative scales share one modulus of continuity.

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

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput

  3. theorem OAI.PolycyclicRecognition.exists_universal_compact_cartan_profiles_all_scales line 88

    Source documentation

    The compact family is chosen before the real scale, the map, the center, and the suffix. This makes subsequent enlargement thresholds independent of any selected sequence.

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

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput