OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanIdealFiberAsymptotics.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Ideal-fiber asymptotics in the constructed ray quotient

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.ideal_fiber_quotient_difference_tendsto_one line 37

    Source documentation

    A fixed displacement in the source ray ideal has asymptotically equal images in the target ray quotient. Both the connecting chains and the quotient contraction are proved from the actual Cartan models.

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

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput