OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanRayBoundaryHaar.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Positive Haar characters on the concrete boundary rays

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.RayBoundaryModel.exists_positive_haar_height_multiplier line 29

    Source documentation

    A retained generator makes the Haar character strictly positive on the selected ray. No volume or trace comparison is assumed.

    theorem RayBoundaryModel.exists_positive_haar_height_multiplier
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput