OAI/GroupTheory/PolycyclicRecognition/Analysis/WordChartTranslations.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_uniform_word_chart_translation_bound line 23

   Source documentation

   The coordinate displacement of left multiplication by exp (-h) is at most a common constant times the normalized coordinate size of h. The constant works for every scale.

   theorem exists_uniform_word_chart_translation_bound
       (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
       (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
       (hinj : Function.Injective Exp)
       (X : I → L) {d : ℕ} (hd : lowerCentralSeries ℝ L L d = ⊥)
       (b₀ : Basis (Fin (finrank ℝ L)) ℝ L)
       (β : WordBasisSelections X (boundedBracketWords d))
       (hβ : IsMaximizingColumnBasis (wordListCoordinates X (boundedBracketWords d) b₀)
         (fun w => bracketWordExponent (fun _ : I => 1) w) β.val)
       {c : ℕ} (a : DynkinCoefficients c 2)
       (hm : ∀ x y, Exp (e (finiteDynkinPolynomial a ![x, y])) = Exp (e x) * Exp (e y))
       (R : ℝ) :
   …

   Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.boundedBracketWords, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.bracketWordExponent, OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial