OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanProfileChainConcentration.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_generator_chain_concentration line 35

    Source documentation

    Actual interior generator switches retain the starting profile on each compact part of the open height domain, in probability. The generator may vary with the scale and the edge of the finite chain.

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

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