OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanBoxIncrementConcentration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.cartan_box_increment_concentration line 38

   Source documentation

   Every bounded box increment supported strictly inside the height domain preserves the starting sheet profile in probability. Generation, prefix bounds, compactness, and measurable profile construction are proved here.

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

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