OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanPublishedRawChain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite-chain concentration from the precisely published inputs

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_uniform_published_raw_chain_concentration line 54

    Source documentation

    The compact profile family is constructed before the enlargement threshold, uniformly in all maps and centers. The conclusion concerns the original raw profiles and assumes no compactness or convergence for their laws.

    theorem exists_uniform_published_raw_chain_concentration
    (hExp : IsGroupExponential Exp) (hinj : Function.Injective Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput