OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanNeighborRateBridge.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Contact bridges at the original neighboring-letter rate

  1. theorem OAI.PolycyclicRecognition.exists_sampled_contact_bridge_at_neighbor_rate line 24

    Source documentation

    The original neighboring-sheet amplitude has exponent q + B * δ. At a positive contact support this gives the same small bridge as the normalized exponent, after a proved change of the enlargement parameter.

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

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput