OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanFixedProbeBridge.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The bridge at the prescribed inward contact pivot

  1. theorem OAI.PolycyclicRecognition.exists_fixed_contact_pivot_probe_bridge line 25

    Source documentation

    The bridge estimate applies to the exact dilation already used by the three sampler chains. Agreement on nilpotent exponentials identifies it with the action constructed in the bridge theorem.

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

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput