GlobalGeneratorWords.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Passing from uniformly rescaled words to global bounded word width

theorem OAI.PolycyclicRecognition.global_generator_words_of_uniform_rescaling line 18

Source documentation

Positive coordinate widths exhaust the whole Lie algebra. Uniform rescaled word length therefore gives bounded global word length after absorbing the rescaling into the unrestricted generator amplitudes.

theorem global_generator_words_of_uniform_rescaling
    {L G I J : Type*} [LieRing L] [LieAlgebra ℝ L] [Group G] [Fintype J]
    (X : I → L) (Exp : L → G) (b : Basis J ℝ L) (cost : J → ℝ)
    (hcost : ∀ j, 0 < cost j) (N : ℕ)
    (hwords : ∀ r : ℝ, 0 ≤ r → ∀ v : L,
      ‖(exponentialRescaleBasis b cost r).equivFun v‖ ≤ 1 →
      ∃ u : List (I × ℝ), u.length ≤ N ∧
        generatorGroupWord (fun i => Real.exp r • X i) Exp u = Exp v) :
    ∀ v : L, ∃ u : List (I × ℝ), u.length ≤ N ∧ generatorGroupWord X Exp u = Exp v := by
…

Mentions: OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.generatorGroupWord

theorem OAI.PolycyclicRecognition.global_generator_words_of_all_rescalings line 48

Source documentation

The uniform word theorem over all generator weights already implies bounded word width on the entire exponential group.

theorem global_generator_words_of_all_rescalings
    {L G I : Type*} [LieRing L] [LieAlgebra ℝ L] [FiniteDimensional ℝ L]
    [Group G] [Fintype I] [DecidableEq I]
    (X : I → L) (Exp : L → G) (S : Finset (FreeMagma I))
    [Nonempty (WordBasisSelections X S)]
    (b₀ : Basis (Fin (finrank ℝ L)) ℝ L)
    (hwords : ∃ (N : ℕ) (C : ℝ), 1 ≤ C ∧
      ∀ (s : I → ℝ) (β : WordBasisSelections X S),
      IsMaximizingColumnBasis (wordListCoordinates X S b₀)
        (fun w : S => bracketWordExponent s w.val) β.val →
      ∀ r : ℝ, 0 ≤ r → ∀ v : L,
      ‖(exponentialRescaleBasis (WordBasisSelections.basis X S β)
…

Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.bracketWordExponent, OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.WordBasisSelections.basis