OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanUniformContactBridge.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform contact-bridge constants before the source choices

  1. theorem OAI.PolycyclicRecognition.exists_uniform_sampled_contact_bridge line 25

    Source documentation

    The constants precede the section, the scale and the subexponential radius. Only the eventual threshold depends on those choices. The estimate uses the original center, sampled root and actual neighboring-letter rate.

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

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput