OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanNormalizedPolarSamplers.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The original neighboring step supplies the polar tiling flow

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_normalized_polar_samplers line 41

    Source documentation

    The original neighboring amplitude gives the actual normalized tiling flow. Its rate and conjugation identity are proved, and the quotient section is fixed before the scale, neighboring step and tail are chosen.

    theorem exists_normalized_polar_samplers
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput