OAI/GroupTheory/PolycyclicRecognition/Analysis/RescaledTranslatedChains.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_translated_rescaled_chain line 21

   Source documentation

   The original suffix and every translated prefix share a single vanishing envelope. Multiplication preserves all actual generator edges; the new initial logarithm is exactly the original suffix.

   theorem exists_translated_rescaled_chain
       (dynkin : NilpotentDynkinExpansionInput E G)
       (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
       (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
       (X : I → L) {c : ℕ} (hc : lowerCentralSeries ℝ L L c = ⊥)
       (b₀ : Basis (Fin (finrank ℝ L)) ℝ L)
       (s : I → ℝ) (β : WordBasisSelections X (boundedBracketWords c))
       (hβ : IsMaximizingColumnBasis (wordListCoordinates X (boundedBracketWords c) b₀)
         (fun w => bracketWordExponent s w) β.val)
       (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop) (hscale1 : ∀ n, 1 ≤ scale n)
       (ε₁ ε₂ : ℕ → ℝ) (hε₁0 : ∀ n, 0 ≤ ε₁ n) (hε₂0 : ∀ n, 0 ≤ ε₂ n)
       (hε₁ : Tendsto ε₁ atTop (𝓝 0)) (hε₂ : Tendsto ε₂ atTop (𝓝 0))
   …

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