OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanSmallWordFactors.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_ambient_word_small_cartan_bound line 39

   Source documentation

   Keep the total size of the Cartan increments, in the same lift that provides the nilpotent box bound. This is the small-chart estimate needed when comparing nearby basepoints.

   theorem exists_ambient_word_small_cartan_bound
       (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (γ : M.Bases) {K : Set G} (hK : IsCompact K)
       (hφ : ∀ d, F.action d = M.adjointGroupAutomorphism T F.N.equiv F.ExpN F.isExpN
         (by rw [← show chartN = F.ExpN from funext hchartN]; exact chartN.bijective) dynkinN
         (cartanLog H F.D.equiv F.ExpD
           (by rw [← show chartD = F.ExpD from funext hchartD]; exact chartD.bijective) d))
       (X : I → H) {d : ℕ} (hDnil : lowerCentralSeries ℝ H H d = ⊥)
       (bD₀ : Basis (Fin (finrank ℝ H)) ℝ H)
       (βD : WordBasisSelections X (boundedBracketWords d))
       (hβD : IsMaximizingColumnBasis (wordListCoordinates X (boundedBracketWords d) bD₀)
         (fun w => bracketWordExponent (fun _ : I => 1) w) βD.val) :
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.cartanLog, OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.boundedBracketWords, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.bracketWordExponent