OAI/GroupTheory/PolycyclicRecognition/Analysis/BoxInteriorSlack.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.rescaled_box_conjugation_tendstoUniformly line 24

   Source documentation

   The actual logarithms of an enlarged suffix and an interior family satisfy the uniform conjugation conclusion. The finite word expansions needed by interior slack are constructed here from the two box bounds.

   theorem rescaled_box_conjugation_tendstoUniformly
       [Nonempty (Fin (finrank ℝ L))]
       (X : I → L) {m k₀ c₀ : ℕ}
       (hk : lowerCentralSeries ℝ L L k₀ = ⊥)
       (hnil : lowerCentralSeries ℝ L L (m + 1) = ⊥)
       (b₀ : Basis (Fin (finrank ℝ L)) ℝ L) (s : I → ℝ)
       (β : ℝ → WordBasisSelections X (boundedBracketWords k₀))
       (hβ : ∀ r, IsMaximizingColumnBasis
         (wordListCoordinates X (boundedBracketWords k₀) b₀)
         (fun w => bracketWordExponent s w) (β r).val)
       (Exp : L → G) (hinj : Function.Injective Exp)
       (hneg : ∀ x, Exp (-x) = (Exp x)⁻¹)
   …

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