OAI/GroupTheory/PolycyclicRecognition/Algebra/WordPivotCoordinates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_compact_word_pivot_coordinates line 16

   Source documentation

   The pivot coordinate moves with the weighted chart. It stays in one compact part of the height domain and has exactly the original height.

   theorem exists_compact_word_pivot_coordinates
       {L W I : Type*} [LieRing L] [LieAlgebra ℝ L]
       [NormedAddCommGroup W] [NormedSpace ℝ W]
       [Fintype I] [DecidableEq I]
       (X : I → L) (S : Finset (FreeMagma I)) (β : WordBasisSelections X S)
       (h : L →ₗ[ℝ] W) (hh : ∀ x y : L, h ⁅x, y⁆ = 0)
       (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop) (hs0 : ∀ n, 0 < scale n)
       (pivot : L) (V : Set W) (hV : IsOpen V) (hp : h pivot ∈ V) :
       let b := WordBasisSelections.basis X S β
   …

   Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.WordBasisSelections.basis