OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanSublinearRayComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Constructing one boundary comparison from the published inputs and sublinear height

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_published_boundary_comparison_of_sublinear line 49

    Source documentation

    All ray models, actions, boundary maps, and volume comparisons are constructed here. Only the previously established sublinear estimates and precisely stated published Lie inputs enter the construction.

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

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput