OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanInteriorSwitch.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   Above a generator's support height, every switch with the prescribed subexponential amplitude has vanishing normalized distance. The chart position and its polynomial bound are constructed from the word basis.

   theorem exists_word_pivot_interior_switch_bound
       (Exp : GroupLieAlgebra (𝓘(ℝ, EG)) G → G) (hExp : IsGroupExponential Exp)
       (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
   …

   Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput

2. theorem OAI.PolycyclicRecognition.CartanWordModel.word_pivot_interior_switch_sublinear line 82

   Source documentation

   The preceding uniform switch bound vanishes after dividing by the physical scale, for arbitrary translated sheets.

   theorem word_pivot_interior_switch_sublinear
       (Exp : GroupLieAlgebra (𝓘(ℝ, EG)) G → G) (hExp : IsGroupExponential Exp)
       (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
   …

   Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput