OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanMeasuredConeRealization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.nonempty_measuredCone_of_published_realization line 27

   Source documentation

   The precise published linear realization supplies the faithful root representation required by the measured cone construction. The choice of height and every metric estimate remain separate from this input.

   theorem nonempty_measuredCone_of_published_realization
       [SimplyConnectedSpace G] {a : ℕ}
       (T : TriangularAdjoint (GroupLieAlgebra (𝓘(ℝ, EG)) G) a)
       (hExpG : IsGroupExponential ExpG)
       (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
   …

   Mentions: OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.ExponentialLinearRealizationInput