OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanRawChainConcentration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Concentration along actual finite Cartan generator chains

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.cartan_raw_chain_concentration line 37

    Source documentation

    The actual sheet profiles concentrate along each allowed finite generator chain. Compact containment and measurable representatives are constructed from the Cartan geometry, so neither is an extra application hypothesis.

    theorem cartan_raw_chain_concentration
    [Nonempty (Fin (finrank ℝ (cartanRootIdeal H)))]
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.ExponentialLinearRealizationInput