OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanBoundaryFamilyShadow.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A common compact shadow for a family with fixed linear height label

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_boundary_family_with_compact_shadow line 34

    Source documentation

    The common centered sublinear estimate supplies one compact boundary shadow for the entire fixed-label family, uniformly over its basepoints.

    theorem exists_boundary_family_with_compact_shadow
    [SimplyConnectedSpace G]
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput