OAI/GroupTheory/PolycyclicRecognition/Algebra/RescaledFixedTranslation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.rescaled_fixed_translation_tendsto line 21

   Source documentation

   The coordinate maps of every fixed right move tend to the identity in the compact-open topology. This is the part of Cartan scaling needed by the density sampling argument; it does not require a preconstructed graded Lie group or any metric scaling premise.

   theorem rescaled_fixed_translation_tendsto
       {I L G : Type*} [Fintype I] [DecidableEq I]
       [LieRing L] [LieAlgebra ℝ L] [Group G]
       (X : I → L) {k c : ℕ} (hk : lowerCentralSeries ℝ L L k = ⊥)
       (hletters : ∀ i : I, FreeMagma.of i ∈ boundedBracketWords k)
       (b₀ : Basis (Fin (finrank ℝ L)) ℝ L)
       (s : I → ℝ) (hs : ∀ i, 0 < s i)
       (β : WordBasisSelections X (boundedBracketWords k))
       (hβ : IsMaximizingColumnBasis (wordListCoordinates X (boundedBracketWords k) b₀)
         (fun w => bracketWordExponent s w) β.val)
       (Exp : L → G) (hinj : Function.Injective Exp)
       (hzero : Exp 0 = 1) (hneg : ∀ x, Exp (-x) = (Exp x)⁻¹)
   …

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