OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanDiagonalNeighborLabels.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One geometric diagonal for shrinking neighboring sheets

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.diagonal_root_neighbor_labels_eq line 39

    Source documentation

    Supported affine labels along shrinking enlargements agree. The proof selects the actual Haar cells, their subexponential mass and all geometric bounds on one diagonal before applying the reflection comparison.

    theorem diagonal_root_neighbor_labels_eq
    (hExpG : IsGroupExponential ExpG) (hinjG : Function.Injective ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput