OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanRayBoundaryComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Boundary volume data constructed on the actual ray quotients

  1. abbrev OAI.PolycyclicRecognition.CartanWordModel.RayBoundaryComparison line 31

    Source documentation

    Volume data for the actual source and target ray actions.

    abbrev RayBoundaryComparison :=
…
  2. theorem OAI.PolycyclicRecognition.CartanWordModel.nonempty_rayBoundaryComparison_of_shadows line 38

    Source documentation

    The two actual Haar characters and the compact-shadow sandwich produce all volume data required in the leaf and averaging steps.

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

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput