OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanNeighborBoxAffinity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.cartan_neighbor_profiles_affine_of_boxes line 36

   Source documentation

   Affinity on both neighboring sheets follows from the original enlarged box bounds. Logarithmic suffixes and their common vanishing error envelope are constructed by the box product estimate.

   theorem cartan_neighbor_profiles_affine_of_boxes
       [IsTopologicalGroup F.N.carrier]
       [Nonempty (Fin (finrank ℝ (cartanRootIdeal H)))]
       (hExp : IsGroupExponential Exp)
       (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
   …

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